Conformità Verificata Staticamente: Barriere Protettive Deterministiche per Sistemi Finanziari Agenti mediante il Teorema Prover Lean 4
Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving
April 1, 2026
Autori: Devakh Rashie, Veda Rashi
cs.AI
Abstract
La rapida evoluzione dell'intelligenza artificiale autonoma e agentica all'interno dei servizi finanziari ha introdotto una crisi architetturale esistenziale: i grandi modelli linguistici (LLM) sono sistemi probabilistici e non deterministici che operano in domini che richiedono garanzie di conformità assolute e matematicamente verificabili. Le soluzioni di guardrail esistenti – incluse NVIDIA NeMo Guardrails e Guardrails AI – si basano su classificatori probabilistici e validatori sintattici che sono fondamentalmente inadeguati per far rispettare i complessi vincoli normativi multi-variabile imposti dalla SEC, dalla FINRA e dall'OCC. Questo articolo presenta il Lean-Agent Protocol, una piattaforma di guardrail per l'IA basata sulla verifica formale che sfrutta il modello neuro-simbolico Aristotle sviluppato da Harmonic AI per auto-formalizzare le politiche istituzionali in codice Lean 4. Ogni azione agentica proposta viene trattata come una congettura matematica: l'esecuzione è consentita se e solo se il kernel Lean 4 dimostra che l'azione soddisfa assiomi normativi pre-compilati. Questa architettura fornisce una certezza di conformità di livello crittografico con latenza a microsecondi, soddisfacendo direttamente la SEC Rule 15c3-5, l'OCC Bulletin 2011-12, la FINRA Rule 3110 e i mandati di spiegabilità del CFPB. Viene fornita una roadmap di implementazione in tre fasi, dalla verifica in shadow mode fino al dispiegamento su scala enterprise.
English
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.