Unified Architecture

The Stack

A formally verified, economically grounded, legally reasoned system for AI agent orchestration, compliance, and governance.

10 systems · 1 formal substrate · 253 theorems · Eduardo Aguilar Peláez

Temporal Envelope Recursa
Application LegalEngine
Protocol & Compliance CCAP · OpenCompliance · LegalLean
Safety Verification Spectral
Orchestration Elan · CSC · TokenGov
Formal Foundations EconLib4

Overview

This document maps ten systems into a single coherent architecture. Each system occupies a distinct layer but shares formal vocabulary, type structures, and proof infrastructure with the others.

The glue is EconLib4 — a Lean 4 library that provides the mathematical substrate upon which every other system predicates.

The systems are not independent projects that happen to be written by the same person. They are a vertically integrated stack spanning from mathematical foundations through agent orchestration to domain application and cross-cutting infrastructure.

12,500+ Lines of Lean 4
253 Formal Theorems
4 Languages
10 Integrated Systems

The Ten Systems

Layer 0 Formal Foundations

EconLib4

Lean 4 · 12,500 lines · 253 theorems · 349 definitions

GitHub →

The mathematical substrate. Formalises economics, game theory, mechanism design, trust, cryptography, information theory, and semantic compression in Lean 4. Every system in the stack implicitly assumes game-theoretic, information-theoretic, or mechanism-design properties. EconLib4 makes those assumptions explicit, compositional, and machine-checkable.

ModuleKey TheoremsGrounds
MechanismDesignvcg_is_dsic, revelation_principleTokenGov allocation, OpenCompliance audit
GameTheorynash_exists, shapley_uniquenessCSC budget partitioning, Elan coordination
SemanticCompressiongroundtrace_soundCSC wind tunnel, LegalLean simplification
Trustreputation_effect, staking_cooperationTokenGov reputation, CCAP trust model
Learningmw_regret_boundTokenGov adaptive allocation, Elan skill selection
Cryptospecial_soundness, fiat_shamirCCAP attestation, OpenCompliance evidence
SocialChoicearrow_impossibilityLegalLean rule aggregation
ContractTheorymonotone_implementableTokenGov screening, LegalLean compliance
Financeput_call_parityTokenGov cross-account optimisation
Informationdata_processing_inequalityTokenGov efficiency, CSC chaos monkey
Layer 1 Agent Orchestration

Elan

Elixir/OTP · 436 Elan tests · 1,119 CompanyAsCode suite

Website →

The runtime. Models an entire organisation as communicating BEAM processes — each agent is a GenServer with typed state, capability bounds, and supervision. Provides process topology, fault tolerance, skill dispatch, state introspection, and Monte Carlo simulation.

ContractTheory.AdverseSelection GameTheory.Bayesian Learning.Regret Finance.Arbitrage

Composable Skill Compiler

Lean 4 + Elixir · 10,000+ lines · 583 tests, 0 failures

GitHub →

English → Verified Agent Pipelines. Compiles natural language prompts into typed, capability-bounded, budget-constrained SkillDAGs with machine-checked Lean 4 proofs at every handoff point. Three-layer verification: type safety, capability safety, budget safety.

English Prompt SemanticIR SkillDAG HandoffProofs Execution
Shapley Value Groundtrace NoisyChannel Nash ZeroKnowledge

TokenGov

Lean 4 + Elixir · 8,200+ lines · 7 invariants

GitHub →

Mechanism design for token budget allocation. Closes the feedback loop between AI agent token consumption and real-world economic outcomes across four accounts. VCG-based allocation, reputation ledger, yoneme cross-account deduplication, bounded punishment, ROI oracle.

Budget Conservation Reputation Boundedness Budget Floor Monotone Allocation Bounded Punishment Yoneme Uniqueness Circuit Breaker
Layer 2 Safety Verification
λ

Spectral

Lean 4 (planned) · EconLib4 primitives · ZK coalition proofs

Docs →

Compositional safety proofs. Addresses Spera (2026, Thm 9.2): safety is non-compositional under conjunctive capability dependencies — two individually safe agents can compose into an unsafe coalition. Spectral formalises the full capability space as a directed hypergraph, computes closure under conjunctive dependencies, and proves the closure does not intersect the forbidden set — all via ZK proofs that preserve agent privacy.

Capability Sets Hypergraph Closure π_safe / π_delta Speculum
ZeroKnowledge Commitment Safety.Compositional Reputation
Layer 3 Legal & Compliance
§

LegalLean

Lean 4 · 87 theorems · JURIX/ICAIL track

GitHub →

Formal legal reasoning. Formalises legal rules as machine-checkable propositions in Lean 4 — rule formalisation, compliance checking, legal simplification with proved semantic preservation, and wind tunnel testing for paraphrase robustness.

ExtensiveForm MoralHazard Arrow Groundtrace

OpenCompliance

7 repos · Schema + controls · Foundation

GitHub →

Standards-grade compliance infrastructure. Replaces compliance theatre with typed, machine-readable evidence chains. Covers SOC 2, ISO 27001, GDPR, NICE digital health, CE marking, ICH E6(R3), MHRA, SRA. The key insight: compliance is a mechanism-design problem.

DirectMechanism Revelation GibbardSatterthwaite Commitment ZeroKnowledge
Layer 4 Protocol & Application

CCAP

TypeScript · Reference impl · Wire protocol

Website →

Agent communication protocol. Defines how agents communicate, attest capabilities, and verify execution. Execution traces, witnesshood, capability attestation, and graded reputation with transitivity conditions.

Commitment ZeroKnowledge Reputation

LegalEngine

Production · AI voice agents · UK Top 100 law firms

Website →

The commercially deployed application at the top of the stack. AI voice agents for law firms with HubSpot, Slack, and email integration via Elan's CompanyAsCode model. Both a customer of the stack and a proving ground — its sales cycles generate the data that trains TokenGov's reputation model.

Cross-Cutting Temporal Envelope

Recursa

Elixir + Lean 4 (planned) · Trace capture · Differential oracle

Docs →

Recursive benchmarking and self-improvement harness. Not a layer — a temporal envelope wrapping Layers 0–4. Feeds synthetic scenarios end-to-end, captures full execution traces across all nine other systems, compares outputs against prior versions, and proves that system evolution preserves or improves correctness. The recursive loop: generate → execute → trace → compare → improve → recurse.

Scenarios Traces Δ(v, v-1) RecursaScore Recurse
Groundtrace NoisyChannel Entropy Regret Nash

Data Flow

LegalEngine Production Application
Elan Runtime
CSC Compiler
TokenGov Budget
OpenCompliance Evidence
Spectral Compositional Safety · ZK Proofs
LegalLean Legal Reasoning
CCAP Wire Protocol
EconLib4 253 theorems · Formal Foundations

Integration Matrix

Every cell describes what the row system imports from the column system.

EconLib4 Elan CSC TokenGov Spectral LegalLean OC CCAP
Elan Regret, Bayesian, AdverseSelection Compiled pipelines Budget allocation Safety status, circuit breaker Compliance posture Execution traces
CSC Shapley, Groundtrace, Nash, ZK Skill registry Budget ceiling; FiduciaryScope calls TokenGov.NormfallAlert.check_all — first live cross-system runtime integration Coalition safety cert Trace format
TokenGov VCG, Revelation, Reputation, Regret Agent pool Budget requests Cross-account safety proof Reputation bridge
Spectral ZK, Commitment, Safety.Compositional Process topology SkillDAG envelopes Capability sets Legal constraints Regulatory forbidden sets Per-agent attestations
LegalLean ExtensiveForm, MoralHazard, Arrow Legal safety surface Control library
OC DirectMechanism, GS, Commitment Compliance-as-safety Control formalisation Evidence attestation
CCAP Commitment, ZK, Reputation HandoffProofs Coalition attestation (ZK) Evidence format
LegalEngine Runtime Token budget Legal reasoning Trust-surface reports
Recursa Groundtrace, Entropy, Regret, Nash Traces Replay, paraphrases Budget snapshots Temporal speculum Scenario seeds Audit scenarios Trace format

Compliance Architecture

19 compliance modules across three layers: Elan provides infrastructure-level controls (audit, policy, model governance, non-repudiation, incident response). TokenGov provides data-level controls (PII, AML, HITL, retention, export). CSC provides trustworthiness controls (Phase 1–5: hallucination gate, audit chain, escalation, competence, pathway, client profile, data grounding, fiduciary scope). Together they cover 7+ regulatory frameworks. BenchArena Tier 8 compliance_mapping: stack 55% > standard 45%.

Compliance Data Flow
Agent ComplianceAuditLog PIIVault NonRepudiationChain AgentPolicyEngine HumanReviewQueue AMLMonitor Ledger
Elan Module TokenGov Module

Priority Ranking by π-Score

Module Layer π Score Regulations Description
ComplianceAuditLog Elan 94.2 FINRA 4511, SEC 17a-4, SOC2 CC7, PCI Req.10 Immutable HMAC-chained event log with 6-year retention
AgentPolicyEngine Elan 91.7 SOC2 CC6, FINRA 3110, SR 11-7 RBAC with kill-switch per agent class
ModelRegistry Elan 88.4 SR 11-7, FINRA 3110, SOC2 CC8 Full SR 11-7 model inventory with risk tiers
PIIVault TokenGov 85.1 GDPR Art.22, CCPA ADMT, PCI DSS Tokenization + PII classification + context window redaction
AMLMonitor TokenGov 82.9 BSA, FinCEN CTR/structuring/velocity rules, SAR 30-day SLA
NonRepudiationChain Elan 79.3 FINRA 4511, SEC 17a-4 Cryptographic HMAC chain-of-custody
HumanReviewQueue TokenGov 76.8 FINRA 3110, SR 11-7, GDPR Mandatory HITL gate with SLA tracking
IncidentResponse Elan 71.4 SOC2 CC9, BSA, PCI DSS 12.10 P0/P1 auto-kill, circuit breaker, automated RCA
DataRetentionEngine TokenGov 68.9 FINRA 4511, PCI, GDPR Policy-driven retention with GDPR erasure handling
RegulatoryExportAPI TokenGov 64.2 SEC 17a-4, FINRA Search/retrieve records for regulator production
ConfabulumRate CSC Phase 1 Epistemic integrity 9-type hallucination gate, halt threshold 0.65
GroundtraceRecord CSC Phase 2 SEC 17a-4, Rule 17a-4 20-field SHA-256 hash chain, Rule 17a-4 path
EscalationGate CSC Phase 3 FINRA 3110, FINRA 3120 I11 invariant, FINRA 3110/3120 material-decision gate
CompetenceSignal CSC Phase 3 Epistemic risk controls Vocabulary-gated synthesis by confidence score
PathwayAudit CSC Phase 3 FINRA 3110, FINRA 3120, SEC 17a-4, DOL fiduciary Compositional deontic compliance, 4 FINRA/SEC obligations
ClientProfile CSC Phase 4 Suitability / fiduciary I13 invariant, freshness-gated advice context
DataAdapter CSC Phase 4 Data quality / citeability Typed/citable FactualGround, stale-ground-blocked proved
FiduciaryScope CSC Phase 5 DOL fiduciary rule, SEC AI governance Licensed-operator wrapper, liability_acceptance_hash gate
NormfallAlert TokenGov Phase 5 DOL fiduciary rule, SEC AI governance, FINRA agentic AI Tracks DOL/SEC/FINRA norm obsolescence, struck-norm halt

Regulatory Coverage Matrix

Module FINRA SEC SOC2 BSA/AML PCI-DSS GDPR SR 11-7
ComplianceAuditLog
AgentPolicyEngine
ModelRegistry
NonRepudiationChain
IncidentResponse
PIIVault
AMLMonitor
HumanReviewQueue
DataRetentionEngine
RegulatoryExportAPI

Part of OpenCompliance Foundation

These 10 modules implement the compliance controls defined by the OpenCompliance Foundation schema. Typed, machine-readable evidence chains replace compliance theatre.

Addressing the Regulatory AI Accountability Gap

The stack closes the regulatory AI accountability gap across four dimensions: ConfabulumRate gates hallucination at the source (9-type classifier, halt threshold 0.65); FiduciaryScope requires a licensed operator before advice is generated (liability_acceptance_hash gate); NormfallAlert detects when governing norms are struck (e.g. DOL fiduciary rule, March 2026) and halts advice generation until norms are re-evaluated; and CompetenceSignal prevents confident language when internal confidence is low (CertaintyVocabulary: Verified / HighConfidence / Moderate / Uncertain / Halted).

Trustworthiness Roadmap — Complete

Five phases of formally-verified trustworthiness controls, all proved and passing CI.

Phase Theme Key Modules Status
Phase 1 Epistemic Integrity RAG grounding, ConfabulumRate gate, CertaintyVocabulary ✓ Complete
Phase 2 Audit Trail GroundtraceRecord, SHA-256 hash chain, BenchArena telemetry ✓ Complete
Phase 3 Agentic Risk Controls EscalationGate (I11 invariant), CompetenceSignal, PathwayAudit ✓ Complete
Phase 4 Data Grounding ClientProfile (I13 invariant), DataAdapter (PerplexitySearch + FRED) ✓ Complete
Phase 5 Legal / Normative NormfallAlert (TokenGov), FiduciaryScope (licensed operator wrapper) ✓ Complete

The SemanticCompression Layer

EconLib4's SemanticCompression module — a novel contribution that exists in no other formalisation library — cuts across every system.

TokenGov

Redundancy quantifies wasted tokens; tersiture sets minimum budgets

CSC

Groundtrace verifies wind tunnel; NoisyChannel bounds chaos monkey

Spectral

Groundtrace over hypergraph closure — proves safety certificates preserve semantic content of capability attestations

Recursa

Groundtrace verifies trace compression; NoisyChannel bounds scenario-vs-reality information loss; Entropy detects redundant scenarios

LegalLean

Legal text compression with proved semantic preservation

Elan

InformationDensity measures prompt quality before dispatch

CCAP

semantic_channel_coding sets agent-to-agent communication rate bounds

OpenCompliance

Regulatory language simplification preserving regulatory intent

Technical Lexicon

Terms coined across the stack that form a shared vocabulary.

chorema
CSC Geometric shape of a skill composition graph
groundtrace
EconLib4 / CSC Conjunction of all HandoffProofs; if inhabited, pipeline is safe
promptome
CSC Full semantic content of a prompt after IR extraction
normfall
CSC / TokenGov Failure mode where a proof attempt collapses
clausome
CSC Universe of skill type signatures known to the compiler
ergotropy
TokenGov Ratio of useful work to total token expenditure
tersiture
EconLib4 / TokenGov Maximum semantic density per token
loquency
TokenGov Verbosity overhead in agent communication
witnesshood
CCAP Third-party attestation of execution correctness
yoneme
TokenGov Cross-account task identity token for deduplication
colimese
CSC Categorical colimit of composed skill types at fan-in
driftlock
CSC / TokenGov Irreversible capability envelope contraction
speculum
Spectral The computed audit surface — the “mirror” reflecting all reachable, frontier, and forbidden capabilities of a coalition
confabulum
Recursa A synthetic scenario that appears realistic but exercises a never-before-tested integration path
ergodrift
Recursa Long-term trend in ergotropy across versions — are we getting more useful work per token over time?
temporal speculum
Recursa / Spectral Δ(speculum(v), speculum(v-1)) — how the safety surface evolved between versions

The Thesis

The stack is not ten systems bolted together. It is one system expressed at ten levels of abstraction.

  1. EconLib4 asks: what are the mathematical properties we need?
  2. CSC asks: how do we compile intent into verified pipelines?
  3. TokenGov asks: how do we allocate scarce resources incentive-compatibly?
  4. Elan asks: how do we run everything concurrently and fault-tolerantly?
  5. Spectral asks: is the composed system — all agents running simultaneously — safe?
  6. LegalLean asks: how do we formalise the rules that govern us?
  7. OpenCompliance asks: how do we prove we follow those rules?
  8. CCAP asks: how do agents communicate and attest across boundaries?
  9. LegalEngine asks: how does all of this generate revenue?
  10. Recursa asks: is the system getting better over time — and can it prove it?

Each question is answered formally. Each answer is connected to the others via EconLib4's shared type vocabulary. The result is a vertically integrated stack where mathematical proof, economic incentive, legal reasoning, and commercial application share a single formal substrate.

Repositories