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

arXiv: https://arxiv.org/abs/2604.01483 · HTML: https://mlsanity.com/paper/2604.01483/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Placed in Financial trading and forecasting agents, one of 16 directions in LLM agents and tool use.
- Builds on 12 of its 44 references that are in the map.
- First posted on arXiv 1 Apr 2026.

## Placed in

- LLM agents and tool use / [Financial trading and forecasting agents](https://mlsanity.com/agents/financial-trading-and-forecasting-agents/)
- LLM safety and security / [Prompt injection and agent security](https://mlsanity.com/safety/prompt-injection-and-agent-security/)

## Builds on (most cited first, 12 of 12)

- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation](https://mlsanity.com/paper/2510.05156/) (2025)
- [Process-Driven Autoformalization in Lean 4](https://mlsanity.com/paper/2406.01940/) (2024)
- [Towards Verifiably Safe Tool Use for LLM Agents](https://mlsanity.com/paper/2601.08012/) (2026)
- [APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning](https://mlsanity.com/paper/2505.05758/) (2025)
- [QueryAttack: Jailbreaking Aligned Large Language Models Using Structured Non-natural Query Language](https://mlsanity.com/paper/2502.09723/) (2025)
- [Logic Jailbreak: Efficiently Unlocking LLM Safety Restrictions Through Formal Logical Expression](https://mlsanity.com/paper/2505.13527/) (2025)
- [Systems Security Foundations for Agentic Computing](https://mlsanity.com/paper/2512.01295/) (2025)
- [Are LLMs Stable Formal Logic Translators in Logical Reasoning Across Linguistically Diversified Texts?](https://mlsanity.com/paper/2506.04575/) (2025)
- [Formalizing Automated Market Makers in the Lean 4 Theorem Prover](https://mlsanity.com/paper/2402.06064/) (2024)
- [FastTTS: Accelerating Test-Time Scaling for Edge LLM Reasoning](https://mlsanity.com/paper/2509.00195/) (2025)
- [A Formal Approach to AMM Fee Mechanisms with Lean 4](https://mlsanity.com/paper/2602.00101/) (2026)

## Built on by (most cited first, 2 of 2)

- [Stable Agentic Control: Tool-Mediated LLM Architecture for Autonomous Cyber Defense](https://mlsanity.com/paper/2605.03034/) (2026)
- [Agent Security Meets Regulatory Reality -- A Practitioner Systematization of Autonomous-Agent Threats and Controls in Regulated Financial Systems](https://mlsanity.com/paper/2606.29142/) (2026)

## Abstract (arXiv)

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.