PaperlayerView exact revision on arXiv

Source-linked AI summary

Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving

Devakh Rashie, Veda Rashi

arXiv:2604.01483v1cs.LOcs.AIcs.CR

TL;DR

Financial agents combine autonomy with probabilistic behavior, while financial regulation demands mathematically verifiable compliance and existing guardrails do not enforce complex constraints. The paper proposes the Lean-Agent Protocol, which uses Aristotle to auto-formalize policies into Lean 4 and gates execution on kernel proofs. It reports mappings to major financial requirements and a roadmap toward zero-trust deployment, while identifying translation-layer and execution-sandbox threats.

  • Problem

    Agentic AI is probabilistic, but financial services require absolute compliance guarantees that existing probabilistic and syntactic guardrails do not provide for complex regulatory constraints.

  • Method

    The Lean-Agent Protocol uses Aristotle to translate institutional policies into Lean 4 and permits execution only when the kernel proves compliance with pre-compiled axioms.

  • Results

    The protocol directly maps to SEC Rule 15c3-5, OCC Bulletin 2011-12, FINRA Rule 3110, adverse-action mandates, and EU AI Act explainability requirements.

  • Takeaways & Limitations

    A three-phase roadmap describes progression from shadow verification to production zero-trust infrastructure for deploying autonomous financial agents at scale.

  • Takeaways & Limitations

    The translation layer remains vulnerable if Aristotle generates structurally valid but semantically malicious Lean code, motivating sandboxing against execution compromise.

Abstract

from arXiv · show

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.

1 Introduction: Deterministic Governance in Agentic AI

Agentic AI brings adaptive, autonomous execution to finance but creates a reliability and compliance crisis because LLM behavior is probabilistic. The Lean-Agent Protocol addresses this gap by translating institutional policies into Lean 4 and permitting actions only after kernel proof.

  • Agentic systems interpret intent, synthesize context, plan multiple steps, and interact autonomously with external environments through APIs and tools.
  • Traditional automation follows predefined logical paths, whereas LLM-based agents generate statistically likely rather than mathematically certain outputs.
  • Existing guardrails mainly use probabilistic classifiers, vector similarity, or syntactic validation, which are inadequate for complex SEC, FINRA, and OCC constraints.
  • The Lean-Agent Protocol uses Aristotle to translate natural-language policies into dependently typed Lean 4 code.
  • Execution occurs if and only if the Lean 4 kernel proves that an action satisfies pre-compiled regulatory axioms.

2 Technical Integration and Workflow Dynamics

The protocol separates asynchronous policy formalization from synchronous action verification. Aristotle translates policies into Lean 4, while the kernel checks proposed actions deterministically before execution, with reported microsecond-scale performance.

  • 2.1 The Aristotle Model: Neural-Symbolic Architecture: Aristotle combines continuous proof search, informal lemma reasoning, and geometry solving, using the Lean compiler as a reinforcement-learning validation signal.
  • 2.2 Translation Error Rates and Handling of Complex Logical Constraints: Aristotle auto-formalizes natural-language concepts into rigorous code and can fill multiple unproven sorry markers in complex policy theorems.
  • 2.2 Translation Error Rates and Handling of Complex Logical Constraints: The system mitigates translation-fidelity risk through deterministic Lean constraints and autonomous self-repair rather than perfect initial generation.
  • 2.3.1 Phase 1: Asynchronous Policy Configuration.: During asynchronous configuration, generated policy code is compiled by Lean and stored as immutable axioms, theorems, and definitions in the Policy Environment.
  • 2.3.2 Runtime Verification: At runtime, the orchestrator intercepts an agent’s API request, extracts parameters, formulates a conjecture, and submits it to the Lean type-checker.
  • 2.3.2 Runtime Verification: A proven conjecture unlocks the gateway, while an unverified conjecture blocks the action and produces a formal audit trace.
  • 2.4 Real-Time Computational Latency in the Agentic Loop: 5 microseconds is the reported average evaluation time for a formalized access-control input in AWS Cedar differential testing, versus 7 microseconds in optimized Rust.
  • 2.4 Real-Time Computational Latency in the Agentic Loop: Lean’s grind tactic can resolve simple arithmetic constraints with sub-millisecond latency during kernel verification.

3 Financial Regulatory and Compliance Mapping

Financial regulations require deterministic controls, organizational supervision, and understandable explanations for automated decisions. The protocol maps agent actions to formal constraints, preserves human control through kernel-gated execution, and back-translates proof failures into natural-language notices.

  • 3.1 SEC Rule 15c3-5: The Market Access Rule and Hard Guardrails: SEC Rule 15c3-5 requires pre-trade controls that reject orders exceeding credit, capital, price, or size thresholds.
  • 3.1 SEC Rule 15c3-5: The Market Access Rule and Hard Guardrails: Because probabilistic filters can theoretically be evaded, they cannot guarantee the direct and exclusive control required by SEC Rule 15c3-5.
  • 3.1 SEC Rule 15c3-5: The Market Access Rule and Hard Guardrails: Immutable Lean axioms make threshold violations fail compilation, causing the gateway to reject the proposed order deterministically.
  • 3.2 OCC Bulletin 2011-12 and FINRA Rule 3110: Supervisory Obligations: OCC Bulletin 2011-12 requires model development, implementation, continuous validation, and governance, while generative agents challenge deterministic MRM assumptions.
  • 3.2 OCC Bulletin 2011-12 and FINRA Rule 3110: Supervisory Obligations: Separating probabilistic reasoning from deterministic execution allows institutions to demonstrate predictable supervisory control to OCC and FINRA examiners.
  • 3.3 The Right to Explanation and Reverse Auto-Formalization for Audit Trails: ECOA, FCRA, GDPR, and the EU AI Act require understandable or meaningful explanations for certain automated decisions, including adverse actions.
  • 3.3 The Right to Explanation and Reverse Auto-Formalization for Audit Trails: Reverse auto-formalization converts technical Lean compilation failures into natural-language adverse-action notices for consumers and non-technical auditors.

4 Security, Vulnerability Analysis, and Formal Sandboxing

The section frames formal methods as a shift from probabilistic LLM safety toward mathematically guaranteed properties, while identifying translation-layer and execution risks. It proposes concept-symbol constraints, context sanitization, and WASM isolation as mitigations.

  • 4.1 Formal Methods for LLM Safety: RLHF, constitutional AI, and automated red-teaming shape behavior but remain reactive and probabilistic as agentic systems expand access to tools and untrusted data.The expanded attack surface is characterized as the “lethal trifecta” of tool access, natural language interfaces, and untrusted external data.
  • 4.1 Formal Methods for LLM Safety: Formal methods seek mathematical guarantees that systems satisfy specified functional and security properties across all possible state spaces.The Lean-Agent Protocol applies this paradigm instead of repeatedly patching models against individual adversarial inputs.
  • 4.2 Vulnerability Analysis: Jailbreaking the Aristotle Translation Layer: The Lean 4 kernel secures execution, but malicious or structurally valid translations from Aristotle could bypass intended policy constraints through logical jailbreaks or formalization drift.The translation layer is identified as the system’s primary vulnerability.
  • 4.2 Vulnerability Analysis: Jailbreaking the Aristotle Translation Layer: LogiBreak, QueryAttack, and sentence-level perturbations shift malicious intent into unfamiliar logical or linguistic forms that can induce symbol drift during formalization.An indirect prompt injection could map a restricted action variable to a permitted Lean symbol, which the kernel would then verify.
  • 4.2 Vulnerability Analysis: Jailbreaking the Aristotle Translation Layer: The proposed translation-layer defenses require explicit concept-symbol mapping tables, hard-coded Lean symbol registries, and static sanitization that strips untrusted external text.These controls constrain terminology-to-logic mapping and limit context reaching the formalization engine.
  • 4.3 Execution Sandboxing: The Strategic Imperative of WebAssembly (WASM): Agent-generated code must be treated as hostile because untrusted execution can enable remote code execution, filesystem manipulation, and sensitive-data exfiltration.The section presents execution sandboxing as a separate security requirement from formal policy verification.
  • 4.3 Execution Sandboxing: The Strategic Imperative of WebAssembly (WASM): Docker shares the host kernel, allowing kernel exploits in generated payloads to escape container boundaries, escalate privileges, and compromise hosts or internal networks.This architectural limitation motivates a stronger isolation substrate for highly untrusted AI execution.
  • 4.3 Execution Sandboxing: The Strategic Imperative of WebAssembly (WASM): WASM provides the mandated execution substrate through linear-memory isolation, a protected call stack, and capability-based security, while compiling both Lean verification and agent tools into sandboxed binaries.The resulting zero-trust perimeter is intended to contain execution even after a translation-layer jailbreak produces malicious Lean code.

5 Competitive and Market Landscape

The paper contrasts probabilistic and syntactic guardrails with Lean-Agent’s theorem-proving approach, then situates Lean verification within cloud authorization and decentralized-finance applications. It also connects machine-checked execution to historical trading failures.

  • 5.1 Evaluating Existing AI Guardrails: Probabilistic vs. Formal Approaches: NVIDIA NeMo Guardrails and Guardrails AI are presented as misaligned with the deterministic requirements of financial regulation.The comparison distinguishes probabilistic vector matching from syntactic validation and formal theorem proving.
  • 5.1 Evaluating Existing AI Guardrails: Probabilistic vs. Formal Approaches: NeMo generates canonical intent forms, matches them with vector similarity, and uses secondary LLM judges, creating adversarial-misclassification risks and latency of hundreds of milliseconds.The cited mechanism relies on continuous vector spaces and additional evaluation calls.
  • 5.1 Evaluating Existing AI Guardrails: Probabilistic vs. Formal Approaches: Guardrails AI uses RAIL and Python libraries such as Pydantic to enforce structural consistency, but cannot prove multi-variable compliance involving margin usage and real-time capital constraints.Syntactic validation can ensure a trade volume is an integer without proving that the value satisfies the broader policy.
  • 5.1 Evaluating Existing AI Guardrails: Probabilistic vs. Formal Approaches: Lean-Agent shifts verification to the Lean 4 kernel, replacing probabilistic matching with theorem proving while exceeding the logical depth of schema validation.The paper characterizes the resulting compliance decision as binary and associates it with microsecond latency.
  • 5.2 Applied Formal Methods in FinTech and Access Control: AWS’s Cedar provides an applied formal-methods precedent: Lean models and verifies its evaluator, authorizer, and validator across quadrillions of production authorizations.The cited theorem guarantees that a “forbid” policy overrides a “permit” policy regardless of evaluation order.
  • 5.2 Applied Formal Methods in FinTech and Access Control: Lean’s reported differential-testing execution time for Cedar averages 5 microseconds, supporting the paper’s claim that formal verification can scale to high-throughput enterprise infrastructure.The passage presents this as evidence from an existing large-scale deployment.
  • 5.2 Applied Formal Methods in FinTech and Access Control: Lean 4 has also been used to mechanically formalize constant-product and fee properties of Automated Market Makers such as Uniswap.These efforts extend formalization from access control into decentralized-finance economic behavior.
  • 5.2 Applied Formal Methods in FinTech and Access Control: The Knight Capital loss of $440 million and the 2007 Hammer case are presented as evidence that algorithmic trading cannot tolerate software ambiguity.The examples connect unchecked errors and manipulated algorithms with material financial-market failures.

6 Strategic Implementation Roadmap

The roadmap proposes phased deployment of Lean-Agent, beginning with risk-free shadow verification, progressing to synchronous WASM-gated enforcement, and ending with autonomous high-frequency enterprise operations.

  • 6 Strategic Implementation Roadmap: The deployment roadmap uses phased integration to manage neuro-symbolic formalization and execution-sandboxing complexity.The phases progress from an MVP toward active gateway operation and then fully autonomous enterprise use.
  • Phase 1: Shadow Verification: The MVP validates Aristotle’s auto-formalization on bounded institutional policies without exposing production systems to risk.The stated objective is capability validation before production enforcement.
  • Phase 1: Shadow Verification: Compliance teams submit bounded policies, including capital thresholds derived from SEC Rule 15c3-5 and fundamental privacy rules, for translation into Lean 4 axioms.MenTaL-style concept-to-symbol constraints are used to reduce formalization drift.
  • Phase 1: Shadow Verification: In Phase 1, live agent outputs are logged and passed asynchronously to the Orchestrator in shadow mode rather than placed directly in the production execution path.This preserves observational validation while avoiding live enforcement exposure.
  • Phase 2: Active Security Gateway: Phase 2 turns the protocol into an active synchronous gateway by compiling the verified policy environment into a hardened WASM runtime.WASI is configured to deny the sandbox access to the host network and filesystem.
  • Phase 2: Active Security Gateway: The Phase 2 Orchestrator intercepts real-time API requests, formulates Lean conjectures, and uses SMT-backed grind tactics for sub-millisecond kernel verification.Verification moves into the critical path of the agentic loop.
  • Phase 3: Enterprise-Scale Deployment: Phase 3 expands the policy environment to global, multi-tiered rules such as GDPR, the EU AI Act, and Basel III.The final phase targets broader enterprise compliance scope.
  • Phase 3: Enterprise-Scale Deployment: Phase 3 adds bounded MPSC mailboxes, work-stealing schedulers, concurrent multi-agent meshes, and cryptographically secure audit logging for high-frequency operations.These orchestration and logging components are intended to support massive-load operation and finalized auditability.

7 Conclusion

The Lean-Agent Protocol addresses the incompatibility between probabilistic agentic AI and deterministic financial regulation through formal verification. It combines Lean 4 enforcement, regulatory mapping, and a three-phase deployment roadmap.

  • The Lean-Agent Protocol uses formal verification to reconcile probabilistic agentic AI with deterministic financial-regulatory requirements.
  • Lean 4 kernel enforcement operates at microsecond latency and is presented as providing cryptographic-level compliance certainty.
  • The protocol maps to SEC Rule 15c3-5, OCC Bulletin 2011-12, FINRA Rule 3110, ECOA/FCRA mandates, and EU AI Act explainability requirements.
  • Lean 4 deployments at AWS through Cedar and in DeFi through AMM formalization are cited as evidence of technical and enterprise-scale viability.
  • A three-phase roadmap progresses from shadow verification MVP to production-ready, zero-trust mathematical AI infrastructure.
Loading 2604.01483v1…