Type-gecontroleerde naleving: Deterministische beveiligingsmaatregelen voor agent-gebaseerde financiële systemen met behulp van Lean 4-theorema-bewijzen
Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving
April 1, 2026
Auteurs: Devakh Rashie, Veda Rashi
cs.AI
Samenvatting
De snelle opkomst van autonome, agent-gebaseerde kunstmatige intelligentie in de financiële dienstverlening heeft een existentiële architectuurcrisis veroorzaakt: grote taalmodellen (LLM's) zijn probabilistische, niet-deterministische systemen die opereren in domeinen die absolute, wiskundig verifieerbare nalevingsgaranties vereisen. Bestaande beveiligingsoplossingen – waaronder NVIDIA NeMo Guardrails en Guardrails AI – steunen op probabilistische classificatiemodellen en syntactische validatoren die fundamenteel ontoereikend zijn voor het afdwingen van complexe, multi-variabele regelgevende beperkingen zoals opgelegd door de SEC, FINRA en OCC. Dit artikel presenteert het Lean-Agent Protocol, een op formele verificatie gebaseerd AI-beveiligingsplatform dat gebruikmaakt van het Aristotle neuraal-symbolische model, ontwikkeld door Harmonic AI, om institutioneel beleid automatisch te formaliseren naar Lean 4-code. Elke voorgestelde agent-actie wordt behandeld als een wiskundig conjecture: uitvoering is alleen toegestaan indien en slechts indien de Lean 4-kernel bewijst dat de actie voldoet aan vooraf gecompileerde regelgevende axioma's. Deze architectuur biedt cryptografisch niveau van nalevingszekerheid bij microseconde latentie, en voldoet direct aan SEC Rule 15c3-5, OCC Bulletin 2011-12, FINRA Rule 3110, en de CFPB-vereisten voor verklaarbaarheid. Een driefasen implementatieroutekaart, van schaduwverificatie tot implementatie op ondernemingsschaal, wordt gepresenteerd.
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.