Conformidade Verificada por Tipos: Barreiras de Segurança Determinísticas para Sistemas Financeiros Autônomos Usando a Prova de Teoremas Lean 4
Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving
April 1, 2026
Autores: Devakh Rashie, Veda Rashi
cs.AI
Resumo
A rápida evolução da inteligência artificial autónoma e agentiva nos serviços financeiros introduziu uma crise arquitetónica existencial: os grandes modelos de linguagem (LLMs) são sistemas probabilísticos e não determinísticos a operar em domínios que exigem garantias de conformidade absolutas e matematicamente verificáveis. As soluções de guardrail existentes – incluindo NVIDIA NeMo Guardrails e Guardrails AI – dependem de classificadores probabilísticos e validadores sintáticos que são fundamentalmente inadequados para impor restrições regulamentares complexas e multivariáveis exigidas pela SEC, FINRA e OCC. Este artigo apresenta o *Lean-Agent Protocol*, uma plataforma de guardrail de IA baseada em verificação formal que aproveita o modelo neuro-simbólico Aristotle desenvolvido pela Harmonic AI para autoformalizar políticas institucionais em código Lean 4. Cada ação agentiva proposta é tratada como uma conjectura matemática: a execução é permitida se e somente se o kernel Lean 4 provar que a ação satisfaz axiomas regulamentares pré-compilados. Esta arquitetura fornece certeza de conformidade a nível criptográfico com latência de microssegundos, satisfazendo diretamente a SEC Rule 15c3-5, a OCC Bulletin 2011-12, a FINRA Rule 3110 e os mandatos de explicabilidade do CFPB. É fornecida uma rota de implementação em três fases, desde a verificação em sombra até à implantação em escala empresarial.
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.