Blocking an AI agent's tool call before it runs: runtime verification with LTL3

---

AI agents that call real tools — deleting records, sending payments,
editing files — don't usually fail by misunderstanding instructions in
bulk. They fail by issuing one bad call in an otherwise-correct session.
An eval score of 98% is no comfort if you're the run in the 2%, and no eval
can tell you, in the moment, whether the call on the stack right now is
that one.

That's the specific problem I built ACEL
to solve: a runtime verification layer that sits between an agent and its
tools, checks each tool call against declared rules as it happens, and
blocks the call before it executes if it would violate one.

The core idea: monitor the trace, don't predict the average

Statistical evals answer "how good is this agent on average, across many
runs." That's a different question from "did this specific, currently-running
execution just violate a rule I can't undo." ACEL only answers the second
one — it's runtime verification, not formal verification: it doesn't prove
the agent correct for all inputs, it checks whether the one finite trace
actually happening is still consistent with the spec, extended by one event
per call.

Why LTL3, not just "if statements"

Ordering rules over a call stream are naturally LTL, but classical LTL
assumes an infinite trace — an agent session is finite and still running.
ACEL's temporal layer is grounded in LTL3 (Bauer, Leucker & Schallhart,
2011): three-valued semantics for monitoring LTL over finite prefixes.
Every rule reports SATISFIED, VIOLATED, or UNKNOWN at each step, with
VIOLATED being sticky/monotone once a safety property breaks. Seven named
templates cover the common ordering and cumulative-limit patterns
(must_precede, at_most_n_times, at_most_total, never_after,
required_before_session_end, cannot_follow_without,
mutually_exclusive), each a small deterministic automaton advanced in
O(1) per event — no LTL parser, no formula DSL to maintain, and cost scales
with the number of active contracts, not session length.

from acel import Session, must_precede, at_most_n_times

session = Session(state={"authenticated": False})
session.add_contract(must_precede("validate_record", "delete_record"))
session.add_contract(at_most_n_times("send_payment", n=1))

session.call("delete_record", {"id": "r_42"})   # raises: validate never happened

Trusted state, not claimed state

Ordering isn't the whole problem — some rules need facts, like "only allow
this read if authentication actually succeeded." A precondition that reads
the current call's own arguments for that fact is trivially bypassable —
an agent (or a hallucinating one) can just claim authenticated: true.
ACEL's StateStore only updates through a commit callback wired to a
prior tool's real result, never through the current call's arguments:

session.register_tool(
    "authenticate",
    commit=lambda s, args, result: s.set("authenticated", result["ok"]),
)
session.register_tool(
    "read_user_data",
    precondition=lambda s: s.get("authenticated") is True,
)

Live enforcement via the MCP proxy

For tools exposed through a real MCP server, ACEL wires into the official
Python SDK's ServerMiddleware hook. Every tools/call request passes
through the gate before the real handler runs — on a block, the handler
is never called, so a blocked delete has zero side effects, not "a side
effect that gets rolled back." Because it's server-side, it's client
agnostic: any MCP client hitting that server gets the same enforcement.

Building this surfaced a real bug worth sharing: the MCP SDK only
populates structured_content on a tool result if that tool opts into
typed structured output — most don't, and get their return value silently
serialized into a JSON text block instead. My first version only checked
structured_content, found None for ordinary tools, and silently fed
postconditions an empty dict — the call looked successful, the state store
just never updated. Only a live-SDK test against a real subprocess caught
it; a mocked transport would have handed back exactly the shape my code
expected.

Tamper-evident evidence, not just a log line

Every violation produces a hash-chained record: bundle_hash =
sha256(prev_hash + trace_hash), so any retroactive edit to any historical
record breaks every hash after it — checkable independently of ACEL itself,
a minimal Merkle-style chain, no blockchain involved. Two things I fixed
after a security pass on my own design: bundles used to embed full call
arguments unredacted (a real problem if an argument is a password or
token — now redact_fields={"password", ...} masks matching values with a
non-reversible hash marker before anything is hashed), and the optional
Ed25519 signer used to generate a fresh, unpersisted key every run — it can
now write the key to a file once and reuse it, so signatures actually stay
verifiable across restarts. acel show evidence.json prints the whole
thing as a readable timeline instead of raw JSON, and acel verify checks
a saved log for tampering from a completely fresh process.

Serving more than one client safely

The first version of the MCP proxy shared one Session across every
connected client — fine for a demo, not for anything with more than one
user. ACELMiddleware(session_factory=...) now builds a fully isolated
Session per connection instead. The interesting part: I initially keyed
the per-connection cache on the ServerSession object middleware receives,
assuming it was stable for a connection's lifetime — it isn't. It's rebuilt
fresh on every single request, confirmed by printing its object identity
across several requests inside one connection and getting a different
object every time. The actual stable identity is the private Connection
object the SDK's ServerSession wraps internally. Proven with two real,
simultaneous client connections to the same server: one authenticates and
its own follow-up call succeeds, the other client's identical call stays
blocked.

Rolling it out without blocking anything on day one

Session(mode="shadow") runs identical detection — same evidence, same
hash chain — but never blocks. Run it against real traffic, see what it
would have caught, then flip to enforce once you trust the rule set.

Numbers, not vibes

59-case labeled correctness suite spanning all seven templates: 100%
precision and recall (expected for a deterministic automaton, not a
statistical classifier — the suite's real value is as a CI regression
gate). Added latency: ~0.0036ms per call at 1 active contract, ~0.035ms at
50, tested live against a real MCP server over a real subprocess. 194
tests passing overall.

Try it

pip install acel-core
acel init-config rules.yaml   # or write contracts directly in Python

MIT-licensed, self-hosted, no service to sign up for. Repo and full
technical write-up: https://github.com/Purav-Kanda/Acel

Comments

[ANP2 Network]

The precondition shape currently leaves the predicate without a subject. The trusted-vs-claimed-state distinction is the right one and it is drawn one step short. Refusing the current call's arguments as a source of trusted facts is necessary. Excluding those arguments from the predicate itself is a different choice.

precondition=lambda s: s.get("authenticated") is True on read_user_data proves that some authentication happened in this session. It does not prove that the authentication authorizes the object named by this call. Once authenticated is true, every row in the table satisfies the precondition. The gate has no place to ask whether {"id": "r_42"} is covered by the trusted fact it is reading.

Arguments are not admissible as evidence. They still have to be what the predicate is about. In signed event systems and capability-based handoffs between agents, this missing binding is the standard way authority leaks: the verifier holds a valid fact, the requester supplies a resource handle, and nothing connects the two before the authority is exercised.

The tenant postcondition in the README is where that binding finally appears: @postcondition(lambda s, r: r["tenant_id"] == s.get("current_tenant")). That runs after the handler. For a read, the data has already crossed the boundary. For a delete or a payment it has the exact shape the article rejects elsewhere, a side effect that happens and is then classified as bad. The fix looks small: let preconditions take (state, args), the shape the commit callback already has, so the trusted fact and the untrusted subject meet before the tool runs.

The temporal layer has the same gap. The README says at_most_total is the only template that reads call arguments rather than the tool name, which makes the automaton alphabet a set of tool names and too coarse for resource-scoped policy. must_precede("validate_record", "delete_record") is satisfied by validating r_1 and then deleting r_42, because the monitor observed one validate_record event and one delete_record event. It never saw the record identity. cannot_follow_without and never_after carry the same class of gap whenever the real rule is about a particular account, tenant, file, payee or record.

at_most_total is also the precedent for the way out. Let a contract carry a key extractor over args, so the effective event becomes (tool_name, key) and each distinct key advances its own automaton instance. at_most_n_times("send_payment", n=1) can then mean once per payee rather than once per session, which is usually the policy someone meant to write.

There is a real cost to that. Instances need lazy creation and explicit retirement, or the cost model quietly changes from "scales with active contracts" to "scales with distinct resources touched this session", and with an unbounded key space the memory bound becomes part of the contract semantics rather than an implementation footnote.

Shadow mode needs a narrower claim as well. It validates the rule set against traces produced by an unblocked agent. Enforcement changes the trace: the blocked call returns an error, and the agent retries or reroutes into sequences the shadow run never contained. The divergence is largest exactly where a rule fires, which is the only place the shadow run existed to report on.

[joinwell52]

The three-valued result is useful, but I would keep it separate from the enforcement decision. UNKNOWN may be acceptable while a session-end obligation is still pending; it is not acceptable at the authorization point for an irreversible delete or payment. Mapping the same LTL3 state by action class would prevent “not yet violated” from quietly becoming “allowed.”