Prismatic Lean4

Overview

Prismatic Lean4 is the verification component of the Prismatic Platform's umbrella architecture. It implements the Lean4 formal proof engine specifically designed for Trinity Gate verification, providing mathematical guarantees of structural, logical, and modal consistency for platform decisions. It bridges Elixir with formal verification systems, enabling mathematical proofs of system properties through theorem prover integration and formal specification languages.

Where other platform components provide probabilistic confidence through statistical methods and heuristic analysis, Prismatic Lean4 provides mathematical certainty. When the Trinity Gate requires formal necessity verification (Layer 3), Lean4 proofs supply the definitive answer -- a property either holds or it does not, with machine-checked proof either way.

Architecture

The core of Prismatic Lean4 is its proof construction pipeline, which translates platform verification requests into Lean4 proof obligations, executes them, and returns formally verified results.

PrismaticLean4.Application
└── PrismaticLean4.Supervisor (:one_for_one)
    ├── PrismaticLean4.SpecGenerator (GenServer)
    │   └── Elixir module + property → Lean4 type signature
    ├── PrismaticLean4.ProofEngine (GenServer)
    │   └── Lean4 tactic engine (simp, omega, decide)
    ├── PrismaticLean4.ProcessPool (PoolSupervisor)
    │   ├── Lean4.OSProcess (Port)
    │   └── ... (configurable pool_size: 4)
    ├── PrismaticLean4.ProofCache (GenServer)
    │   └── ETS: {module, property, source_hash} → {status, proof_term, timestamp}
    └── PrismaticLean4.ResultTranslator (GenServer)
        └── Lean4 output → Elixir {:ok, proof} | {:error, counterexample}

Pipeline Architecture

Verification Request --> Specification --> Proof Obligation --> Lean4 Engine --> Verified Result
        |                     |                  |                  |                |
  Elixir Module         Formal Spec         Tactic Script      Type Check       {:ok, proof}
  Property Claim        Generation           Generation         + Verify         or {:error, counterexample}

Pipeline Stages

Proof Types

Key Modules

Configuration

config :prismatic_lean4,
  # Lean4 binary path
  lean4_path: System.get_env("LEAN4_PATH", "/usr/local/bin/lean"),

  # Process pool
  pool_size: 4,
  max_proof_timeout_ms: 60_000,

  # Proof caching
  cache_enabled: true,
  cache_invalidation: :source_hash,

  # QEVE integration
  qeve_enabled: true,
  trinity_gate_layer: 3

API Reference

QEVE Integration

The Quantitative Epistemic Verification Engine (QEVE) combines Lean4 formal proofs with Monte Carlo simulation and NABLA epistemic analysis:

# Combined QEVE verification
{:ok, report} = PrismaticQeve.verify(%{
  property: "security_rating_consistency",
  formal: %{
    lean4_spec: "theorem rating_monotone : ...",
    required: true
  },
  probabilistic: %{
    monte_carlo_runs: 10_000,
    confidence_target: 0.99
  },
  epistemic: %{
    nabla_axioms: [:signal_plurality, :provenance_mandatory],
    min_confidence: 0.95
  }
})

# Direct proof verification with caching
{:ok, result} = PrismaticLean4.verify(property, cache: true)

# Force re-verification (bypass cache)
{:ok, result} = PrismaticLean4.verify(property, cache: false)

Trinity Gate Layer 3

-- Lean4 proof: NABLA Signal Plurality axiom holds for all belief updates
theorem signal_plurality_preserved
  (b : Belief) (update : BeliefUpdate)
  (h_valid : b.sources.length >= 2) :
  (apply_update b update).sources.length >= 2 := by
  cases update with
  | add_source s => simp [apply_update]; omega
  | remove_source s => simp [apply_update]; exact h_valid
  | modify_confidence c => simp [apply_update]; exact h_valid

-- Lean4 proof: Trinity Gate structural consistency
theorem trinity_structural_consistency
  (g : BeliefGraph) (h_dag : is_dag g) :
  is_dag (add_verified_belief g belief proof) := by
  apply dag_preserved_by_leaf_addition
  exact h_dag

Testing

# Run all Lean4 tests
cd apps/prismatic_lean4 && mix test

# Run with coverage
mix test --cover

# Run without starting the application (unit tests only)
mix test --no-start

# Run proof cache tests
mix test test/prismatic_lean4/proof_cache_test.exs

Testing validates specification generation, proof caching with source-hash invalidation, process pool lifecycle management, and QEVE integration. Unit tests run without Lean4 installation by mocking the proof engine; integration tests require the full Lean4 toolchain.

Integration Points

NABLA Compliance

Prismatic Lean4 is the definitive NABLA compliance enforcement mechanism for formal properties.

All seven NABLA axioms have corresponding Lean4 theorems. The proofs verify that axiom properties are preserved under all possible belief graph operations, providing mathematical certainty beyond what empirical testing can achieve.

Performance

Proof Caching Strategy

Related Resources

• Prismatic Nabla -- NABLA Infinity epistemic framework
• Prismatic Monte Carlo -- Probabilistic verification engine
• Prismatic Deduction -- Logical deduction framework
• Prismatic Lean -- Higher-level formal verification bridge
• Evidence Enforcement Agent -- Ensures formal proofs are correctly applied
• Trinity Gate -- Lean4 implements Layer 3 (Formal Necessity)
• NABLA Axioms -- Formal proofs of axiom preservation
• Quality Gates -- Proof verification in quality gate pipeline

Connect & Contribute

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

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