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