Financial regulation does not operate on confidence intervals. SEC Rule 15c3-5 requires broker-dealers to maintain controls with automated, pre-trade hard blocks — binary, deterministic, and under the direct and exclusive control of the firm. A probabilistic classifier cannot satisfy this. It can only approximate it.
Lost by Knight Capital in 45 minutes to an unchecked algorithmic error. No probabilistic guardrail would have prevented it — only a hard, formal constraint.
The latency cost of an LLM-as-a-judge guardrail call. At that speed, high-frequency agentic systems aren't just slow — they are architecturally broken.
The acceptable false-negative rate under SEC Rule 15c3-5. A 98.3%-accurate guardrail has a 1.7% failure rate — across thousands of actions an hour, that is a violation waiting to happen.
NeMo Guardrails and similar tools use LLM inference and vector similarity to evaluate actions. Vector spaces are continuous — adversarial inputs can shift semantic distance and misclassify a restricted action as permitted. This is not a limitation to manage; it is a fundamental incompatibility with financial regulation.
Schema validators like Pydantic confirm that a trade-volume field is an integer. They cannot prove that the specific integer, combined with current capital and historical margin usage, satisfies a multi-tiered regulatory constraint. Type-checking structure is not verifying semantics.
When an LLM evaluates another LLM's output, the decision trail is probabilistic all the way down. There is no machine-verifiable proof of why an action was permitted — only a natural-language explanation that may itself be hallucinated. FINRA Rule 3110 requires tamper-evident records. A log of LLM outputs is not that.
"The rule requires that brokers have risk management controls and supervisory procedures reasonably designed to manage the financial, regulatory, and other risks of this business activity."
— SEC Rule 15c3-5, Market Access Rule
Compliance becomes code, every action becomes a theorem, and the Lean 4 kernel returns a verdict — not a confidence score.
Compliance officers author policies in plain English — capital thresholds, position limits, risk parameters. The Aristotle neural-symbolic model translates each into a Lean 4 axiom, compiled and stored in an immutable Policy Environment. They do not change at runtime. They do not drift. They cannot be jailbroken.
When an agent proposes a trade, rebalance, or credit decision, the biject orchestrator intercepts the call before the execution layer. It extracts the parameters, maps them against the Policy Environment, and serializes the action as a formal Lean 4 conjecture — the claim that this action satisfies all applicable policies.
The conjecture is submitted to the Lean 4 type-checker. The kernel either produces a machine-verifiable proof or determines none exists — a binary, deterministic decision, not a score. PROVED routes to execution; REFUTED is blocked, and the error trace is back-translated into a plain-language adverse-action notice satisfying ECOA and CFPB.
The Lean 4 kernel runs at ~5µs per verification on warm cache. The decision is independent of request complexity — it is a type-check, not an inference. biject adds no meaningful latency to agent execution.
NeMo Guardrails and Guardrails AI were built for consumer-facing LLM applications — not regulated environments where compliance is binary, latency is critical, and every decision must be auditable. The difference is not of degree. It is of kind.
| NVIDIA NeMo Guardrails | Guardrails AI | ↦ biject | |
|---|---|---|---|
| Core architecture | Colang dialog flows, vector similarity, LLM prompts | RAIL spec, Pydantic schema validation | Aristotle auto-formalization + Lean 4 kernel |
| Verification paradigm | Probabilistic | Syntactic | Deterministic |
| Latency | ~500ms (secondary LLM) | Low (Python-level) | ~5µs (kernel type-check) |
| Regulatory fit · SEC 15c3-5 | Inadequate — vector space drifts under adversarial input | Inadequate — cannot verify multi-variable capital logic | ⊢ Optimal — immutable axioms, mathematical certainty |
| Adverse action notices | Not provided | Not provided | Auto-generated from Lean trace (ECOA / CFPB) |
| Audit trail | LLM output logs | Schema validation logs | Cryptographic, hash-linked proof record |
| Adversarial robustness | Vulnerable to semantic perturbation | Vulnerable to type-coercion edge cases | ⊢ Immune — a proof exists or it does not |
"The Lean-Agent Protocol transcends both paradigms. By shifting the verification burden to the Lean 4 kernel, the platform abandons probabilistic vector matching in favor of deep mathematical theorem proving, while vastly exceeding the logical depth of simple schema validation."
— Rashie & Rashi (2026), arXiv:2604.01483
The same proof gate, encoding whichever obligations govern your desk — from market-access hard blocks to automatic adverse-action notices.
The Market Access Rule requires automated, pre-trade hard blocks on orders that exceed capital thresholds or create undue risk. biject provides these at the mathematical layer — not a heuristic, but a formal proof requirement. An order that cannot be proved compliant is blocked before it reaches the exchange.
Managers under mandated portfolio constraints — sector exposure, concentration limits, benchmark deviation — encode these directly as Lean axioms. Every rebalancing action an autonomous agent proposes is verified against the full constraint set before execution.
biject exposes a Python SDK and a Model Context Protocol server. Any agent on Claude, GPT-4, LangGraph, or any framework can be wrapped without architectural changes. The agent calls tools as normal — biject intercepts at the API layer.
The CFPB requires automated systems denying financial actions to provide specific, machine-generated explanations. biject's back-translation pipeline converts every Lean error trace into a plain-language notice citing the exact policy violated — automatically, at the point of refutation, with no additional inference.
biject was designed against the specific technical requirements of financial regulation — not adapted from a consumer guardrail product. Each regulation maps directly to an architectural property.
This demo runs against pre-compiled Lean 4 policy axioms modelling SEC Rule 15c3-5 capital constraints and position concentration limits. Select a scenario to submit it to the real biject orchestrator — the kernel verdict returns in microseconds.
Reference demo against pre-compiled Lean 4 .olean policy binaries. The kernel runs decide-tactic resolution on integer basis-point arithmetic; latency shown is wall-clock time at the orchestrator layer.
The orchestrator sits between your agent and its execution layer — intercepting tool calls, verifying them against the Policy Environment, and routing or blocking them. Your agent code does not change.
Broker-dealers and asset managers in air-gapped environments deploy the orchestrator and Lean worker as on-premise Docker containers. Trade data never leaves your infrastructure; policy compilation runs locally; the audit log is written to your own storage.
Full documentation at docs.biject.ai · github.com/bijectai/biject · hello@biject.ai
biject is built on a formal architecture described in a peer-reviewed paper — the full theoretical basis for the Lean-Agent Protocol, including the regulatory mapping, adversarial threat model, latency benchmarks, and competitive analysis. Available in full on arXiv.
AbstractThe rapid evolution of autonomous, agentic AI within financial services has introduced an architectural crisis: large language models are probabilistic, non-deterministic systems operating in domains that demand absolute, mathematically verifiable compliance guarantees. This paper presents the Lean-Agent Protocol — a formal-verification guardrail platform that leverages the Aristotle neural-symbolic model 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 the action satisfies pre-compiled regulatory axioms.
This is not the first production deployment of Lean 4 at scale. AWS uses Lean 4 to formally verify Cedar — its authorization policy language — across quadrillions of production authorizations. biject applies the same approach to financial compliance.
biject is accepting pilot partners. Pilot access includes a pre-compiled SEC Rule 15c3-5 policy library, API access to the orchestrator, Python SDK and MCP integration support, and direct access to the research team.