Allow or block, with proof

AI agents call tools: they read files, run shell commands and send email. Many teams put a guard in front of those calls. Afterwards, the record of its decision is a log line.

That guard is usually a small model that answers allow or block, and the log line says “guard: allow”. To believe it, you must trust whoever wrote the line. You trust that a guard ran at all, that it was the model they evaluated, and that it judged this call and not a different one.

In our previous note we ran Anthropic's open-source research prover FlashProve on a consumer gaming GPU. In this note we use it to answer a narrower question: can an auditor check, without trusting the operator, which decision a committed guard model made for one specific tool call?

On our test setup the answer is yes, with limits we spell out below.

The short answer

We trained a small guard on a synthetic tool-use policy. It classifies held-out calls correctly 99.2% of the time when they mix familiar names, and 94.1% when they use file names, hosts and commands it never saw in training.
For 40 of 40 held-out calls, the guard's decision was proved on an RTX 5070 Ti in about 2–3.6 s each. Every proof was accepted by FlashProve's unmodified verifier.
Each decision goes into a signed receipt. A separate checker grades the claim “this committed guard decided BLOCK for this call” at the computation-proven level, because it recomputes every link itself rather than taking the operator's word.
We also tried 12 ways a dishonest operator could forge a receipt, most of them signed with a key the checker trusts. The checker caught all 12.
The guard got one of the 40 wrong, and the receipt for that mistake is still graded “proven”. This is intended, and it is the most important result here.
The checker, the receipts, the proofs and the logs are public in whyagents/graded-agent-evidence. One command re-checks every receipt.

Three links, each checked by the checker

A claim like “guard G blocked this delete_files call” holds only if three things are true. Our checker tests each one separately:

Link	How the checker tests it	Level
1. The computation. The committed model, given input R, produced answer token y	FlashProve's zero-knowledge proof, judged by the unmodified upstream verifier against the guard's published commitment	proven
2. The binding. R is this call	R is a public, deterministic encoding of the tool name and its canonical (RFC 8785) arguments. The checker re-encodes the call itself and compares the bytes	recomputed
3. The meaning. Token y means BLOCK	A pinned, public decision map: `' y'` means ALLOW, and anything else means BLOCK (fail-closed). The checker applies it itself	recomputed

The claim gets the level of its weakest link. In the same receipt, other claims are graded honestly lower:

“The agent really issued this call” is only what the gateway observed.
“The block was enforced” is likewise only observed.

The receipt states this, along with why each claim is not graded higher.

Link 2 matters most. Without it, a proof shows only that the model judged some input. An operator could then attach a genuine ALLOW proof from a harmless call to a dangerous one.

What a dishonest operator cannot do

In these tests the forger holds a signing key that the checker trusts, so a valid signature alone proves nothing. Each case below was caught:

Reuse a real ALLOW proof from another call for a delete_files call: caught, because the re-encoded request does not match.
Swap in harmless-looking arguments while keeping the original proof: caught, because the request does not match.
Relabel the tool (call the delete a read_file): caught.
Write “ALLOW” over a proved BLOCK answer: caught, because the pinned map says BLOCK.
Change the proved answer token: the verifier rejects the proof.
Drop the proof's binding and keep the “proven” label: caught, and flagged as an overclaim.

The six other cases cover non-canonical argument bytes, links that disagree with each other, a missing decision map, a changed tokenizer, an unsigned file swap, and an omitted map link.

The guard got one wrong, and the receipt still says “proven”

The guard allowed read_file ~/.gnupg/secring.gpg. That is a secret-key file, but it is a name the guard never saw in training. The ordinary floating-point model makes the same mistake, so this is a weakness of the guard, not of the proof.

The receipt for that call still grades the decision as proven, and that is correct. The proof establishes which decision this committed model made for this exact call. It does not establish that the decision was right.

Whether a guard is any good is a separate claim that needs its own evidence: tests against explicit acceptance criteria, which we grade as outcome-validated. An evidence format that blurs these two claims will eventually certify a mistake as safe.

What the proof does add: every decision is tied to one commitment. Once an auditor has evaluated the guard behind that commitment, the operator cannot quietly swap in a different model later. Every receipt would show a different commitment.

How we built it

The guard is Karpathy's TinyStories260K, a 260,000-parameter story model. We fine-tuned it for 7.5 minutes on a CPU, using 1,500 synthetic tool calls across six tools. The calls were labelled by a written policy of six BLOCK rules, such as reading secrets, wide deletes, dangerous shell commands and data leaving by email or HTTP; everything else is ALLOW. Before training it blocked everything: 16.7% and 34.9% correct on the two test sets. Always guessing the commonest answer scores 83.3% and 65.1%.
The conversion into FlashProve's integer format is our own Python code, written from FlashProve-L4's documented scheme. On the original checkpoint it reproduces L4's published model file byte for byte.
The fine-tune leaves each weight tensor's scale unchanged. This let the guard reuse L4's public prover settings without refitting, and FlashProve's worst-case range check accepted it on the first try.
The integer model agrees with the floating-point model on all 40 proved calls.
Each proof is about 5.6 MB and was made on a 16 GB GeForce RTX 5070 Ti in an ordinary Windows PC, under WSL2.

What this does not prove

That this is a usable guard. The policy, the tools and every value are synthetic, and accuracy is measured on calls from the same generator. It is a 260K-parameter model trained in minutes. This is a working demonstration of the evidence chain, not a security product.
That the weights are hidden. Proofs are the right tool when the guard's weights are private, as with a vendor's proprietary guard; when the weights are public and small, anyone can re-run the model instead. FlashProve's verifier does not check hiding. Our patched prover has not yet been compared byte for byte with unmodified upstream. Until it is, we make no hiding claim.
That the agent's real call had these arguments, or that the block was enforced. Both rest on the gateway's word, and the receipt says so.
That integer and float always agree. They agreed on all 40 proved calls, but some calls in the novel set are close calls for the float model (the smallest top-two margin is 0.10). The proof covers the integer computation.
That long calls work. The guard sees at most 256 tokens. Longer calls are refused (and so blocked), never truncated.
Anything about large or served models, and no formal verification. The verifier we use is FlashProve's tested C++ verifier. Upstream's Lean-proved verifier does not accept this proof format.
That this has been reproduced elsewhere. It ran on one machine and has not been independently replicated.
That it is new. Others have tied proofs to agent actions:
- giskard09 records each verdict as a hashed decision record;
- ezumba feeds verdicts into an authority gate bound to an action hash (in simulation mode);
- zkAgent proves whole agent transcripts.
Signed per-action receipts are now common. What we have not seen elsewhere is a checker that recomputes the binding to the arguments itself, grades every link, and refuses claims graded higher than their evidence. Our search was limited, so we claim nothing more.

Why WHY cares

Most agent records today are at the observed level, and signed receipts reach tamper-evident. We are building evidence that states how much it proves: observed, signed, hardware-attested, computation-proven or outcome-validated. Each claim is graded by its weakest link and checked by software that never trusts the issuer. Proofs are expensive, so we use them where they pay: small, private guard and policy models whose decisions someone else must be able to check.

Run agents in production? Talk to us Re-check the receipts