Why Raucle's gate actually holds

EPIC28 Ltd · 1 September 2026

You built a gate. The gate checks every tool call your AI agent makes. If the call violates policy, the gate denies it. The agent never reaches the tool. Clean architecture.

Now: what happens when the gate throws an exception?

If the answer is "the tool runs anyway," you don't have a gate. You have a suggestion box. And the agent is free to ignore suggestions.

This is the fail-open problem, and it is the most common structural defect we see in AI agent security tooling. Not the most exotic, not the most sophisticated. The most common. It survives in production because it doesn't show up in a demo, doesn't trigger in a unit test, and doesn't raise an alarm in a dashboard. The security layer fails silently, the agent carries on, and nobody knows the gate was advisory all along.

We know because we ran a security review against our own product, Raucle, and found three ways ours could fail open. This post walks through all three, the fixes, and the layer beneath them: what the formal machinery can and cannot prove. If you're wiring security into an agent framework, at least one of these patterns is probably sitting in your codebase right now.

What fail-open actually means

Fail-open is when a security control's failure path leads to "allow" instead of "deny." The control doesn't crash the system, doesn't raise an alert. It just stops enforcing, and the system continues as if nothing happened.

The opposite is fail-closed: if the security layer can't make a determination, the default action is deny. The system stops. Somebody has to investigate.

In traditional security architecture, fail-closed is the default for anything that matters. Firewalls drop packets they can't evaluate. Authentication layers reject tokens they can't verify. In AI agent security the defaults are inverted, and the reason is structural: the agent frameworks are built to tolerate component failures, which is exactly wrong for a component whose job is to say no.

Bug one: the exception that vanished

The first bug was in the LangChain integration. LangChain uses a callback system to hook the agent's execution loop. The Raucle callback sat on the before_tool_call hook, ran the capability gate, and raised CapabilityDenied on violation. The design was correct. The behaviour was not.

LangChain's callback manager catches exceptions thrown by callback handlers. By default, it logs them as warnings and continues execution. The tool call the gate just denied proceeded anyway. The agent never saw the denial. The only trace was a warning line in a log nobody reads.

A security callback is not a normal callback. Its failure mode needs to be "stop execution," not "log and continue."

The fix was two lines: raise_error=True and run_inline=True on the callback registration. The first tells LangChain to propagate the exception; the second keeps the callback synchronous so it can't vanish into a handler pool. Both are load-bearing. Both are commented, because if either disappears in a refactor, the gate becomes advisory again and nothing will warn you.

The regression test doesn't mock the callback. It runs the real tool.run() dispatch path with a blocked call and asserts the tool never executes. You can't catch framework-circumvention by stubbing out the framework.

Bug two: the missing argument that scanned nothing

The second bug lived in the MCP server, where a scanner checked call arguments for policy violations before passing them through. When a tools/call request omitted a schema-required argument, the scanner received an empty string. It scanned the empty string. The empty string is clean. ALLOW. The tool executed with a missing required argument.

That is fail-open by omission. The scanner didn't crash; it just didn't account for the case where the thing it was checking wasn't there. "No match" was treated as "clean," which is correct for a detection system and wrong for an enforcement system.

The fix: schema validation moved ahead of policy evaluation, and any malformed call now produces DENY with a receipt explaining why. If the gate can't evaluate the request, the request does not happen.

Bug three: the clock that ran out

The third bug involved capability expiry. Capabilities carry a time-to-live; an expired capability should be as good as absent. The expiry check compared timestamps correctly, but the comparison ran on the issuing machine's clock, and the check happened at mint time only, not at every use. A long-running session could carry a capability past its lifetime, and the gate would honour it because it had already been honoured once.

Expiry now evaluates at gate time, every call, against the gate's own clock, and a stale capability produces DENY with a receipt. The principle underneath all three fixes is the same: enforcement decisions are made at the enforcement point, with the enforcement point's own inputs, and the default when anything is missing is no.

What the maths underneath actually proves

Fixing fail-open bugs makes the gate behave correctly in the cases you thought of. Formal verification is how you cover the cases you didn't. Raucle pairs the runtime gate with a verification layer, and it's worth being precise about what each part delivers.

The policy proofs (SMT)

For each tool, Raucle takes the tool's JSON Schema and the security policy, and hands both to an SMT solver (Z3). The solver either proves that every schema-valid call satisfies the policy, or it returns a concrete counterexample: a call that is valid against the schema and violates the policy. Proofs are content-addressed and cited by every capability derived from them.

The practical value: you learn, before deployment, whether your policy has holes a schema-valid call can walk through. A policy that says "IDs starting with C- only" gets proven against the entire space of calls the schema admits, not just the calls in your test suite.

The soundness theorems (Lean 4)

Three theorems are mechanised in Lean 4 with zero sorrys. Attenuation cannot broaden permissions: delegating a capability can only shrink what it allows. Gate ALLOW implies constraint satisfaction for the modelled constraint kinds. And assuming prover soundness (an explicit axiom), a call under a PROVEN proof satisfies the policy.

Equally important is what the mechanisation does not cover. Some runtime behaviours — starts_with constraints, forbidden field combinations, revocation, expiry, signature and issuer pinning — are enforced by the runtime gate and covered by tests, but are not yet in the Lean model. The proof boundary is published precisely. Anyone claiming the theorem prover makes the gate "unbreakable" hasn't read the boundary; anyone claiming formal verification is marketing hasn't read the theorems.

The receipts (Ed25519)

Every gate decision, ALLOW or DENY, produces a receipt: Ed25519-signed, content-addressed, hash-linked into a chain with periodic signed checkpoints. The deploying organisation publishes its verification key. A third party with only the published material verifies receipts offline: signature, cited schema and proof hashes, attenuation chain, decision. By default the receipt carries a hash of the call arguments, not the arguments themselves, so evidence travels without payload data.

The honest scorecard

On the AgentDojo banking suite, the gate blocked 100% of attacker-controlled tool calls across 720 LLM-driven attempts. That number is a structural property, not a classifier score: a call outside the signed capability cannot execute because the gate sits on the execution path and denies it. The residual benchmark successes trace to a known IBAN-collision artefact in the oracle itself. On other suites, a small residual rate remains, concentrated in attacks scored on free-form model output outside the gate's tool-call boundary. Median gate latency is 69µs without an attenuation chain; end-to-end agent wall time is at or below unprotected baselines on four of eight measured cohorts, because terminating attacker-induced reasoning loops early pays for the gate's cost.

Read that scorecard the way we intend it: the gate holds where it sits, and we publish exactly where it sits. No security claim survives contact with a path it doesn't mediate, and the strongest deployment is credential custody, where the agent never holds the tool's key and cannot act without passing the gate.

Raucle is Apache-2.0, the Lean developments and benchmark harness are published with the code, and the paper draft is in the repository. If you're building agent security and want a second pair of eyes on your integration path, that is quite literally our practice: [email protected].