Prismatic Lean

Overview

Prismatic Lean provides a bridge between the Elixir platform and the Lean 4 theorem prover, enabling formal mathematical verification of critical platform properties. It translates Elixir specifications into Lean 4 propositions, executes proof obligations, and integrates verification results into the platform's epistemic framework. This module serves as the formal necessity layer -- the third gate of the Trinity Gate -- ensuring that critical claims are not merely consistent or logical but mathematically proven.

The verification bridge addresses a fundamental challenge in complex systems: how to guarantee that security rating algorithms are monotonic, that compliance scoring never produces contradictory results, and that epistemic axioms hold under all conditions. While property-based testing can demonstrate that properties hold for many random inputs, formal verification proves they hold for all possible inputs -- a qualitative difference in assurance level that matters for safety-critical decisions.

Prismatic Lean operates as part of the platform's QEVE (Quantitative Epistemic Verification Engine) alongside Prismatic Monte Carlo for probabilistic analysis. Where Monte Carlo quantifies uncertainty through simulation, Lean provides certainty through mathematical proof.

Architecture

The module runs as a supervised OTP application with process-isolated Lean 4 toolchain management.

PrismaticLean.Application
└── PrismaticLean.Supervisor (:one_for_one)
    ├── PrismaticLean.SpecTranslator (GenServer)
    │   └── Elixir AST → Lean 4 definition translation
    ├── PrismaticLean.ProofScheduler (GenServer)
    │   └── Proof obligation queue with priority ordering
    ├── PrismaticLean.EnginePool (PoolSupervisor)
    │   ├── Lean4.Worker (Port process)
    │   ├── Lean4.Worker ...
    │   └── Lean4.Worker ...
    ├── PrismaticLean.ProofCache (GenServer)
    │   └── ETS: :lean_proof_cache (property, version → proof result)
    └── PrismaticLean.ResultParser (GenServer)
        └── Lean 4 output → Elixir {:ok, proof} | {:error, counterexample}

Elixir @spec/@type → Spec Translator → Lean 4 Definitions
         ↓                  ↓                   ↓
  Behavioral Contracts   AST Transform    Lean 4 Propositions
  Invariant Specs        Type Mapping     Proof Obligations
         ↓                                      ↓
  Property Generators ←→ Lean 4 Proof Engine → Verification Result
                                ↓                    ↓
                          Proof Artifacts    Trinity Gate Layer 3
                          Counterexamples    Confidence Score

The translator parses Elixir type specifications and behavioral contracts through AST analysis, mapping Elixir types to their Lean 4 equivalents. Proof execution is managed through a supervised port process that communicates with the Lean 4 toolchain, with result caching for incremental verification.

Key Modules

Configuration

config :prismatic_lean,
  # Lean 4 engine
  lean4_binary: System.get_env("LEAN4_PATH", "/usr/local/bin/lean"),
  pool_size: 4,
  proof_timeout_ms: 30_000,

  # Caching
  cache_enabled: true,
  cache_ttl_seconds: 86_400,

  # Trinity Gate
  trinity_gate_enabled: true,
  min_proof_coverage: 0.80

API Reference

# Verify a property formally through Lean 4
{:ok, proof} = PrismaticLean.verify(
  property: :monotonic_security_score,
  spec: PrismaticPerimeter.SecurityRating
)
# => %{status: :proven, proof_hash: "abc123...", time_ms: 2340}

# Generate proof obligations for a module
{:ok, obligations} = PrismaticLean.obligations(PrismaticNabla.Axioms)
# => [%{property: :signal_plurality, status: :pending}, ...]

# Verify all properties for a module
{:ok, report} = PrismaticLean.verify_all(module: PrismaticAlgorithms)
# => %{total: 12, proven: 10, failed: 1, timeout: 1}

# Extract counterexample from failed proof
{:ok, counter} = PrismaticLean.counterexample(failed_obligation)

# Check proof cache status
{:ok, stats} = PrismaticLean.cache_stats()
# => %{entries: 142, hit_rate: 0.87, total_proofs: 163}

Testing

# Run all Lean verification tests
cd apps/prismatic_lean && mix test

# Run with coverage
mix test --cover

# Run proof engine integration tests (requires Lean 4 installation)
mix test test/prismatic_lean/engine_pool_test.exs

# Run spec translator unit tests
mix test test/prismatic_lean/spec_translator_test.exs

Tests cover specification translation accuracy, proof caching with invalidation, engine pool process management, and Trinity Gate integration. Integration tests require a Lean 4 installation and verify end-to-end proof execution with real theorem proving.

Integration Points

NABLA Compliance

Prismatic Lean is the primary implementer of NABLA's formal verification requirements.

Trinity Gate Layer 3 passage requires at least one formal proof for each critical property claim. Lean provides the definitive answer: proven or disproven with machine-checked evidence.

Performance

Related Resources

• Prismatic Lean4 -- Low-level Lean 4 toolchain integration and process management
• Prismatic Monte Carlo -- Probabilistic verification complementing formal proofs
• Prismatic Testing -- Property-based testing as a complement to formal proofs
• Prismatic Transcendence -- Consciousness axiom verification through formal methods
• Evidence Enforcement Agent -- Enforces evidence-based verification standards
• Trinity Gate -- Prismatic Lean serves as the Layer 3 formal necessity provider
• NABLA Axioms -- Formal verification of the 7 epistemic axioms

Connect & Contribute

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

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