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

• URL: http://arxiv.org/abs/2604.01483v1
• Date: Wed, 01 Apr 2026 23:39:43 GMT
• Title: Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving
• Abstract summary: This paper presents the Lean-Agent Protocol, a formal-verification-based AI guardrail platform.<n>Every proposed agentic action is treated as a mathematical conjecture.<n>This architecture provides cryptographic-level compliance certainty at microsecond latency.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Provably Secure Agent Guardrail [89.79561918065122]
  Existing defense architectures rely on empirical semantic guardrails and probabilistic large model adjudicators.<n>This paper proposes a new security paradigm for agents based on the fundamental limitations of logical reasoning.
  arXiv  Detail & Related papers  (2026-05-28T02:12:41Z)
• AgenticAITA: A Proof-Of-Concept About Deliberative Multi-Agent Reasoning for Autonomous Trading Systems [0.0]
  AGENTICAITA is an agentic AI framework that replaces the traditional signal then execute paradigm with a fully autonomous loop.<n>The framework demonstrates operational correctness of the deliberative pipeline, achieving 157 zero-intervention invocations across 76 assets.
  arXiv  Detail & Related papers  (2026-05-01T16:25:43Z)
• Position: agentic AI orchestration should be Bayes-consistent [92.04373485710285]
  This paper argues that coherent decision-making requires Bayesian principles at the orchestration level of the agentic system.<n>It provides examples and design patterns to illustrate how beliefs and utility-aware policies can improve agentic AI orchestration.
  arXiv  Detail & Related papers  (2026-05-01T15:43:43Z)
• TRUST: A Framework for Decentralized AI Service v.0.1 [47.384270414446604]
  Large Reasoning Models (LRMs) and Multi-Agent Systems (MAS) in high-stakes domains demand reliable verification.<n>We introduce TRUST (Transparent, Robust, and Unified Services for Trustworthy AI), a decentralized framework with three innovations.<n>We prove a Safety-Profitability Theorem ensuring honest auditors profit while malicious actors incur losses.
  arXiv  Detail & Related papers  (2026-04-29T19:32:58Z)
• From CRUD to Autonomous Agents: Formal Validation and Zero-Trust Security for Semantic Gateways in AI-Native Enterprise Systems [0.0]
  This paper proposes the design, formal validation, and empirical evaluation of a Semantic Gateway governed by the Model Context Protocol (MCP)<n>The gateway reframes the enterprise API as a semantic surface where tools are dynamically discovered, authorized, and executed based on intent and policy enforcement.<n>The architecture introduces a three-layer Zero-Trust security model comprising a pre-inference Semantic Firewall, deterministic Tool-Level RBAC, and out-of-band Cryptographic Human-in-the-Loop approval.
  arXiv  Detail & Related papers  (2026-04-28T12:25:06Z)
• Architecting Secure AI Agents: Perspectives on System-Level Defenses Against Indirect Prompt Injection Attacks [46.32011684548212]
  AI agents are vulnerable to indirect prompt injection, in which malicious instructions embedded in untrusted data can trigger dangerous agent actions.<n>This position paper discusses our vision for system-level defenses against indirect prompt injection attacks.
  arXiv  Detail & Related papers  (2026-03-31T17:15:46Z)
• FormalJudge: A Neuro-Symbolic Paradigm for Agentic Oversight [21.731032636844237]
  This paper proposes a neuro-symbolic framework that employs a bidirectional Formal-of-Thought architecture.<n>We validate across three benchmarks spanning behavioral safety, multi-domain constraint adherence, and agentic upward deception detection.
  arXiv  Detail & Related papers  (2026-02-11T18:48:11Z)
• Self-Evolving Coordination Protocol in Multi-Agent AI Systems: An Exploratory Systems Feasibility Study [0.0]
  Self-Evolving Coordination Protocols (SECP)<n>SECP: coordination protocols that permit limited, externally validated self-modification.<n>This paper presents an exploratory systems feasibility study of Self-Evolving Coordination Protocols.
  arXiv  Detail & Related papers  (2026-02-02T14:45:04Z)
• Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification [49.506412445511934]
  Large Language Models (LLMs) show remarkable capabilities, yet their next-token prediction creates logical inconsistencies and reward hacking.<n>We introduce a formal logic verification-guided framework that dynamically interleaves formal symbolic verification with the natural language generation process.<n>We operationalize this framework via a novel two-stage training pipeline that synergizes formal logic verification-guided supervised fine-tuning and policy optimization.
  arXiv  Detail & Related papers  (2026-01-30T07:01:25Z)
• Towards Verifiably Safe Tool Use for LLM Agents [53.55621104327779]
  Large language model (LLM)-based AI agents extend capabilities by enabling access to tools such as data sources, APIs, search engines, code sandboxes, and even other agents.<n>LLMs may invoke unintended tool interactions and introduce risks, such as leaking sensitive data or overwriting critical records.<n>Current approaches to mitigate these risks, such as model-based safeguards, enhance agents' reliability but cannot guarantee system safety.
  arXiv  Detail & Related papers  (2026-01-12T21:31:38Z)
• The Agentic Regulator: Risks for AI in Finance and a Proposed Agent-based Framework for Governance [6.107950696680386]
  Current model-risk frameworks assume static, well-specified algorithms and one-time validations.<n>We model these technologies as decentralized ensembles whose risks propagate along multiple time-scales.<n>We propose a modular governance architecture that decomposes oversight into four layers of "regulatory blocks"
  arXiv  Detail & Related papers  (2025-12-12T05:57:32Z)
• Towards a Science of Scaling Agent Systems [79.64446272302287]
  We formalize a definition for agent evaluation and characterize scaling laws as the interplay between agent quantity, coordination structure, modelic, and task properties.<n>We derive a predictive model using coordination metrics, that cross-validated R2=0, enabling prediction on unseen task domains.<n>We identify three effects: (1) a tool-coordination trade-off: under fixed computational budgets, tool-heavy tasks suffer disproportionately from multi-agent overhead, and (2) a capability saturation: coordination yields diminishing or negative returns once single-agent baselines exceed 45%.
  arXiv  Detail & Related papers  (2025-12-09T06:52:21Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• Making LLMs Reliable When It Matters Most: A Five-Layer Architecture for High-Stakes Decisions [51.56484100374058]
  Current large language models (LLMs) excel in verifiable domains where outputs can be checked before action but prove less reliable for high-stakes strategic decisions with uncertain outcomes.<n>This gap, driven by mutually cognitive biases in both humans and artificial intelligence (AI) systems, threatens the defensibility of valuations and sustainability of investments in the sector.<n>This report describes a framework emerging from systematic qualitative assessment across 7 frontier-grade LLMs and 3 market-facing venture vignettes under time pressure.
  arXiv  Detail & Related papers  (2025-11-10T22:24:21Z)
• Agentic AI for Financial Crime Compliance [0.0]
  This paper presents the design and deployment of an agentic AI system for financial crime compliance (FCC) in digitally native financial platforms.<n>The contribution includes a reference architecture, a real-world prototype, and insights into how Agentic AI can reconfigure under regulatory constraints.
  arXiv  Detail & Related papers  (2025-09-16T14:53:51Z)
• Safe and Certifiable AI Systems: Concepts, Challenges, and Lessons Learned [45.44933002008943]
  This white paper presents the T"UV AUSTRIA Trusted AI framework.<n>It is an end-to-end audit catalog and methodology for assessing and certifying machine learning systems.<n>Building on three pillars - Secure Software Development, Functional Requirements, and Ethics & Data Privacy - it translates the high-level obligations of the EU AI Act into specific, testable criteria.
  arXiv  Detail & Related papers  (2025-09-08T17:52:08Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.