The Stack

One system,
ten levels of abstraction.

Legal Engine is the application at the top of a vertically integrated stack: from mathematical foundations through agent orchestration and compositional safety to legal reasoning and recursive benchmarking. The glue is a single Lean 4 type vocabulary shared by every layer.

Start with AI Grounding → LegalLean deep-dive
Ten systems

A stack, not a pile of tools.

They are one system expressed at ten levels of abstraction, connected through EconLib4's shared type structures.

Layer 0 — Formal Foundations

EconLib4

The mathematical substrate every layer predicates on.

Lean 4 · 12,500 lines · 253 theorems

Layer 1 — Agent Orchestration

Elan

Fault-tolerant runtime; agents as supervised BEAM processes.

Elixir / OTP
CSC

Compiles English into typed, capability-bounded pipelines.

Lean 4 + Elixir
TokenGov

Incentive-compatible budget allocation across agents.

Lean 4 · 7 invariants + Elixir

Layer 2 — Safety Verification

Spectral

Compositional safety proofs for agent coalitions.

Lean 4 + EconLib4

Layer 3 — Legal & Compliance

LegalLean →

Legal rules as machine-checked propositions.

Lean 4 · 80+ theorems
OpenCompliance

Typed, machine-readable evidence chains.

Standards library, 7 repos

Layer 4 — Protocol & Application

CCAP

Wire protocol for agent attestation and execution traces.

TypeScript (reference)
LegalEngine

The production application this stack powers.

AI voice agents for law firms

Cross-cutting — Temporal Envelope

Recursa

Recursive benchmarking that proves each version is better.

Elixir + Lean 4
Verified by construction

Three proofs at every handoff.

When the compiler joins one skill to the next, three properties are machine-checked before the edge is allowed to exist.

  • Type safety — the output type of the source is a subtype of the target's input.
  • Capability safety — the target's capability envelope is within what the source permits.
  • Budget safety — combined budget never exceeds what remains.
-- A pipeline edge only exists if it type-checks. def composes (A : Sol α) (B : α → Sol β) : Sol β -- Three-layer handoff contract output(src) ≼ input(tgt) -- type capability(tgt) ⊆ allowed(src) -- capability budget(src)+budget(tgt) ≤ remaining -- budget ✓ groundtrace inhabited ⇒ pipeline safe

See it on your own work.

Speak to us → Explore solutions