White Team

Overview

The White Team provides the formal verification and constructive proof capability within the Prismatic Platform's six-team color-team security architecture. While Red Team finds vulnerabilities through adversarial simulation and Blue Team builds defenses through monitoring and detection, White Team proves that systems hold through progressive formal methods — from property-based testing through contract validation to full Lean4 theorem proving. White provides mathematical certainty where simulation and observation alone cannot.

The theoretical foundation of White Team operations draws from formal methods in software engineering, type theory, constructive logic, and the Curry-Howard correspondence that links proofs and programs. The Prismatic Platform implements a six-level verification hierarchy (L0-L5) that allows verification effort to be calibrated to the criticality of the system under examination. Low-criticality modules receive L0-L1 verification (unit and property tests), while safety-critical paths receive L4-L5 verification (theorem proving and full formalization).

White Team's role within the color-team architecture is uniquely constructive — while other teams find problems (Red), detect changes (Blue), explore boundaries (Gray), model threats (Black), and synthesize findings (Purple), White Team proves that solutions work. White verification evidence feeds into Purple Team closure decisions, providing the formal proof that a defense implementation actually satisfies its security properties. This constructive role makes White Team essential for the platform's Trinity Gate — the three-layer verification gate that every belief must pass.

Mission and Doctrine

The White Team mission is to provide progressive formal verification of platform systems, producing mathematical evidence that implementations satisfy their specifications. This evidence supports Purple Team closure decisions, Trinity Gate passage, and long-term platform reliability.

Mission Principles

The NO MERCY, NO DOUBTS doctrine governs White operations with emphasis on NO DOUBTS: every verification claim must be backed by reproducible proof artifacts, and no system is declared "verified" without evidence at the appropriate level. NO MERCY manifests in the insistence on genuine verification — proofs that actually prove the property in question, not superficially similar properties that are easier to verify.

Team Composition

The White Team comprises three agents organized around the verification lifecycle: campaign orchestration, contract validation, and invariant proving.

white-verifier-commander

The Verifier Commander orchestrates verification campaigns, assigning verification levels to target systems based on criticality assessment, available specifications, and resource constraints. The commander also constructs composite proofs — combining evidence from multiple verification methods into unified proof packages that satisfy Trinity Gate requirements. Campaign planning considers the priority signals from Purple Team about which findings require formal verification for closure.

white-contract-validator

The Contract Validator specializes in three contract types: behavior contracts (function input/output relationships verified against @spec annotations), protocol contracts (Elixir protocol compliance verification), and API contracts (OpenAPI specification validation for external interfaces). This agent produces test suites that continuously verify contract compliance, serving as the L1-L2 verification layer.

white-invariant-prover

The Invariant Prover conducts the deepest verification work — property-based testing with StreamData, model checking, and formal theorem proving with Lean4. This agent handles L3-L5 verification, producing mathematical proofs of system invariants. The prover also conducts fault injection analysis, verifying that systems maintain their properties under controlled failure conditions.

Verification Hierarchy

Progressive Methodology (L0-L5)

Verification Pipeline

flowchart TD
    Spec["Specification Extraction"]
    Prop["Property Identification"]
    Level["Level Assignment<br/>(L0-L5 based on criticality)"]
    Gen["Test / Proof Generation"]
    Exec["Execution &amp; Verification"]
    Evid["Evidence Artifact Production"]
    Purple["Purple Team / Trinity Gate Submission"]

    Spec --> Prop --> Level --> Gen --> Exec --> Evid --> Purple

    classDef stage fill:#0f172a,stroke:#e2e8f0,color:#fff
    classDef gate fill:#1e293b,stroke:#a855f7,color:#fff
    class Spec,Prop,Level,Gen,Exec,Evid stage
    class Purple gate

Level Assignment Criteria

Contract Validation

Three Contract Types

Contract Testing Implementation

defmodule PrismaticDark.WhiteTeam.ContractValidator do
  @moduledoc """
  Three-type contract validation for behavior, protocol, and API contracts.
  Produces continuous verification evidence for Purple Team closure support.
  """

  @type contract_type :: :behavior | :protocol | :api
  @type verification_result :: %{
    contract_type: contract_type(),
    target: module(),
    properties_verified: non_neg_integer(),
    properties_failed: non_neg_integer(),
    confidence: float(),
    evidence: [map()]
  }

  @spec validate_behavior_contract(module(), atom(), non_neg_integer()) :: verification_result()
  def validate_behavior_contract(module, function, arity) do
    spec = fetch_spec(module, function, arity)
    properties = extract_properties_from_spec(spec)

    results =
      properties
      |> Enum.map(&verify_property(module, function, &1))

    %{
      contract_type: :behavior,
      target: module,
      properties_verified: Enum.count(results, &(&1.status == :verified)),
      properties_failed: Enum.count(results, &(&1.status == :failed)),
      confidence: calculate_confidence(results),
      evidence: results
    }
  end

  @spec validate_protocol_contract(module(), module()) :: verification_result()
  def validate_protocol_contract(protocol, implementation) do
    required_functions = protocol.__protocol__(:functions)

    results =
      required_functions
      |> Enum.map(fn {name, arity} ->
        verify_protocol_function(implementation, name, arity)
      end)

    %{
      contract_type: :protocol,
      target: implementation,
      properties_verified: Enum.count(results, &(&1.status == :verified)),
      properties_failed: Enum.count(results, &(&1.status == :failed)),
      confidence: calculate_confidence(results),
      evidence: results
    }
  end
end

Invariant Proving

Property-Based Testing

defmodule PrismaticDark.WhiteTeam.InvariantProver do
  @moduledoc """
  Property-based testing and formal proof generation.
  Handles L1-L5 verification with progressive methodology.
  """
  use ExUnit.Case
  use ExUnitProperties

  property "NABLA signal plurality: minimum 2 independent signals for belief" do
    check all signals <- list_of(signal_generator(), min_length: 1, max_length: 20) do
      belief = PrismaticNabla.form_belief(signals)

      case belief do
        {:ok, %{confidence: c}} when c > 0.5 ->
          independent_sources = signals |> Enum.map(& &1.source) |> Enum.uniq()
          assert length(independent_sources) >= 2

        {:error, :insufficient_plurality} ->
          independent_sources = signals |> Enum.map(& &1.source) |> Enum.uniq()
          assert length(independent_sources) < 2

        _ ->
          :ok
      end
    end
  end

  property "account balance invariant: balance >= 0 after any operation sequence" do
    check all operations <- list_of(operation_generator()) do
      account = Account.new()
      final = Enum.reduce(operations, account, &apply_operation/2)
      assert final.balance >= 0
    end
  end
end

Lean4 Formal Proofs

-- Proof that Trinity Gate is sound: if all three gates pass, the belief is valid
theorem trinity_gate_sound (belief : Belief) :
  trinity_passes belief →
  structural_consistent belief ∧
  logical_consistent belief ∧
  formally_necessary belief := by
  intro h
  constructor
  · exact h.structural
  constructor
  · exact h.logical
  · exact h.formal

-- Proof that NABLA signal plurality prevents single-source beliefs
theorem nabla_plurality_prevents_single_source :
  ∀ (signals : List Signal),
    (signals.length ≥ 2 ∧ sources_independent signals) →
    ¬ (single_source_dominant signals) := by
  intro signals ⟨h_len, h_indep⟩
  intro h_single
  have : sources_independent signals := h_indep
  exact absurd h_single (independent_not_single h_len this)

Fault Injection Analysis

White Team validates system resilience through controlled fault injection, verifying that systems maintain their verified properties under failure conditions.

Technical Architecture

System Architecture

White Verifier Commander (L3)
├── Campaign Planner
│   ├── Criticality Assessor (assigns L0-L5)
│   ├── Specification Extractor
│   └── Resource Scheduler
├── Contract Validator (L4)
│   ├── Behavior Contract Engine
│   ├── Protocol Contract Engine
│   ├── API Contract Engine
│   └── Evidence Collector
├── Invariant Prover (L4)
│   ├── Property Test Generator (StreamData)
│   ├── Model Checker (TLA+)
│   ├── Theorem Prover (Lean4)
│   └── Fault Injector
└── Evidence Pipeline
    ├── Proof Artifact Storage
    ├── Confidence Calculator
    ├── Trinity Gate Submitter
    └── Purple Team Evidence Emitter

Telemetry Events

NABLA Compliance

White Team provides the formal verification layer that supports NABLA axiom enforcement across the platform.

Trinity Gate Support

White Team provides the Formal Necessity component of the Trinity Gate:

Performance Metrics

Integration Points

Signal Flow

Red Findings ──→ Proof Targets ──→ White Team ──→ Proof Artifacts
                                       ↑                ↓
Blue Defenses ──→ Verification ────────┘          Purple Team
                    Targets                       (closure evidence)
                                                       ↓
Gray Edge Cases ──→ Property ──────────────────→ Trinity Gate
                    Test Seeds                   (formal necessity)

Outputs

Related Resources

• Purple Team — Primary consumer of White verification evidence for closure
• Red Team — Produces findings that require formal verification
• Blue Team — Produces defenses that White formally verifies
• Gray Team — Edge case discoveries that seed property-based tests
• Black Team — Theoretical models verified against formal specifications
• Trinity Gate — Three-layer verification gate supported by White proofs
• Quality Gates — Quality enforcement incorporating verification status

Connect & Contribute

Created by Tomáš Korcak (korczis) | Open Source under GHL

• GitHub | GitLab | LinkedIn | Contact
• Developer Portal | Architecture | Meet the Creator