Axiom Protocol: Mathematical Determinism for AI Agents

Axiom Protocol treats agent tool calls as formal conjectures in Lean 4. Only actions with a machine-verifiable proof of compliance are executed, replacing probabilistic risk with logic.

Comment

Inspiration: The Probability Gap in Compliance

Financial regulations are structured as deterministic "hard rules"—legal obligations rather than guidelines. For example, "Do not execute trades exceeding 10% of available daily capital" is a binary constraint. However, the AI agents increasingly responsible for these decisions are probabilistic. They do not "know" a rule; they output tokens statistically likely to represent compliance. This creates a fundamental misalignment between the deterministic nature of law and the non-deterministic nature of Large Language Models (LLMs).

Existing solutions often fail to bridge this gap:

  • NeMo Guardrails: Utilizes an LLM to judge another LLM, adding significant latency (~500ms) and remaining susceptible to prompt injection.
  • Guardrails AI: Performs syntactic validation (e.g., Pydantic), confirming data types (integers) but failing to verify semantic legality against dynamic constraints like margin usage.

Neither approach satisfies SEC Rule 15c3-5, which requires risk controls to be under a firm’s "direct and exclusive control." A system that blocks 99.9% of violations remains a probabilistic risk. Axiom Protocol was developed to move from estimating safety to proving it using formal verification.

System Overview

Axiom Protocol intercepts trading agent actions and subjects them to mathematical proof before execution.

When an agent triggers a command, such as execute_trade(symbol="AAPL", volume=50000), the Orchestrator captures the request. It maps the parameters against a pre-compiled Policy Environment—a set of Lean 4 axioms encoding specific compliance rules. The Lean kernel then determines if the trade satisfies these axioms.

The result is binary: true or false. There are no confidence scores or thresholds. This verification occurs in under one millisecond. The system includes a live demo where trading scenarios are processed through the kernel; each decision is recorded in an audit log featuring the raw Lean 4 proof trace alongside a natural-language explanation for regulatory transparency.

Architecture & Implementation

The system is designed around the verification step as the primary control point.

Core Components

  • Lean Worker: A Dockerized Python server wrapping elan and lake. Policy .olean binaries are baked into the image at build time. To ensure kernel decidability, all policy thresholds are expressed as basis-point integers over Nat (Natural Numbers) rather than floats. This allows Lean 4’s decide tactic to resolve arithmetic at the kernel level with extreme speed.
  • FastAPI Backend (Orchestrator): Captures agent calls, formats them as Lean conjectures, and manages the flow of verdicts and audit logs via WebSockets and asyncio.Queue.
  • Frontend: A React + Vite interface (TypeScript) providing a three-panel view of the policy compiler, agent runner, and real-time audit log.
  • Infrastructure: Deployed on Hetzner via Coolify. A translation layer utilizes Claude to back-translate Lean error traces into human-readable adverse action notices, ensuring the audit trail is accessible to non-technical stakeholders.

Technical Challenges

The Decidability Constraint

Standard financial policies often use decimals and percentages. However, formal verification through the Lean kernel requires decidable arithmetic. This necessitated re-encoding all policy layers into integer basis-point form to allow the decide tactic to function, ensuring the system remains mathematically airtight.

Latency Optimization

Formal verification is often perceived as too slow for high-frequency environments. Axiom Protocol solves this by decoupling proof generation (slow, performed at deployment) from proof checking (fast, performed at runtime). By utilizing pre-compiled .olean files, the runtime burden is reduced to simple type-checking.

Translation & Safety

While the Lean kernel is mathematically certain, the translation from natural language to Lean code (via neural-symbolic models) remains a potential point of failure. The architecture addresses this through context sanitization and strict symbol constraints to prevent "formalization drift" or indirect injection during the policy-creation phase.

Performance & Regulatory Alignment

Benchmarks

The system achieves verification latencies comparable to AWS Cedar (~5µs per evaluation). By resolving Nat constraints at the kernel level, Axiom Protocol demonstrates that formal verification is compatible with the low-latency requirements of modern finance.

Regulatory Mapping

The protocol aligns with specific institutional requirements:

  • SEC Rule 15c3-5: Provides immutable, pre-trade controls under exclusive firm control.
  • OCC 2011-12: Ensures model transparency through deterministic proof traces.
  • FINRA Rule 3110: Enables predictable, verifiable supervision.
  • ECOA/CFPB: Generates plain-language adverse action notices through the back-translation pipeline.

Insights Gained

The development of Axiom Protocol highlights that the choice of data representation—such as committing to Nat over floating-point arithmetic—is a fundamental compliance decision. Floating-point imprecision renders a system formally undecidable at the kernel level; switching to basis-point integers is a requirement for provable correctness.

Furthermore, the "explainability" problem remains a significant research frontier. While LLMs can back-translate proof states into human-readable text, ensuring the absolute fidelity of that translation (avoiding "hallucinated explanations") is the next stage of development for high-assurance systems.

Roadmap: Mathematical Determinism for AI

  • WASM Sandboxing: Transitioning the verification environment to WebAssembly to provide a zero-trust execution layer for AI-generated code.
  • Policy Scaling: Expanding the library of axioms to cover the full breadth of Basel III, the EU AI Act, and GDPR.
  • Multi-Agent Orchestration: Scaling the kernel to handle concurrent agent populations with bounded MPSC (Multi-Producer, Single-Consumer) mailboxes and work-stealing schedulers.

Built With

Share this project:

Updates