Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving
Devakh Rashie, Veda Rashi
cs.LO
Apr 1, 2026 · v1
TL;DR
Auto-formalizes regulatory policy into Lean 4 so the kernel gates each agent action.
Abstract
The rapid evolution of autonomous, agentic artificial intelligence within financial services has introduced an existential architectural crisis: large language models (LLMs) are probabilistic, non-deterministic systems operating in domains that demand absolute, mathematically verifiable compliance guarantees. Existing guardrail solutions -- including NVIDIA NeMo Guardrails and Guardrails AI -- rely on probabilistic classifiers and syntactic validators that are fundamentally inadequate for enforcing complex multi-variable regulatory constraints mandated by the SEC, FINRA, and OCC. This paper presents the Lean-Agent Protocol, a formal-verification-based AI guardrail platform that leverages the Aristotle neural-symbolic model developed by Harmonic AI to auto-formalize institutional policies into Lean 4 code. Every proposed agentic action is treated as a mathematical conjecture: execution is permitted if and only if the Lean 4 kernel proves that the action satisfies pre-compiled regulatory axioms. This architecture provides cryptographic-level compliance certainty at microsecond latency, directly satisfying SEC Rule 15c3-5, OCC Bulletin 2011-12, FINRA Rule 3110, and CFPB explainability mandates. A three-phase implementation roadmap from shadow verification through enterprise-scale deployment is provided.
Problem
Autonomous AI agents in financial services operate as probabilistic systems, yet regulatory compliance (SEC, FINRA, OCC) demands absolute, mathematically verifiable guarantees. Existing guardrail solutions rely on probabilistic classifiers and syntactic validators that cannot enforce complex multi-variable regulatory constraints.
Approach
The authors propose the Lean-Agent Protocol, which uses Lean 4 theorem proving to provide deterministic compliance verification for agentic financial systems. The architecture integrates the Aristotle auto-formalization engine to translate regulatory rules into Lean 4 type specifications, then validates agent actions against these formal constraints before execution. Each financial transaction is type-checked against regulatory predicates (position limits, capital requirements, reporting obligations) with binary proof/refutation outcomes.
Results
The system provides deterministic verification with binary pass/fail outcomes, contrasted with probabilistic approaches. NVIDIA NeMo Guardrails adds approximately 500ms latency per call via secondary LLM inference, while the Lean-based approach operates via direct kernel verification. The paper presents a comparative analysis showing the Lean-Agent Protocol achieves formal guarantees that probabilistic (NeMo) and syntactic (Guardrails AI) systems cannot provide.
