Verifiable code execution for AI agents

Logs record what an agent claims; Ampoule proves what it computed.

When an AI agent runs code, Ampoule runs it in a sealed, single-use micro-VM and returns the output with a signed receipt. For a deterministic run, replay on the pinned kernel recomputes it and must get the same output.

Become a design partner Read the receipt spec

info@ampoule.dev

The problem

Agents act on code output nobody can check.

An agent writes code, runs it, and sends money, emails or reports based on what came back. Afterwards there is no way to show what actually ran, or that the result wasn't changed on the way.

Signatureproves who vouched

Replayproves what ran

A signature only proves who vouched for a result, not what ran. A forger can re-sign a fake receipt with their own key: the signature checks out, but replay of a deterministic run on the pinned kernel rejects it.

How it works

Run. Receipt. Replay.

Deterministic runs replay bit for bit on the pinned kernel, so you can check the result instead of trusting whoever ran it.

01 · Run

Sealed micro-VM

Untrusted code runs in a fresh VM with no network. Input goes in through a mailbox.

02 · Receipt

Signed receipt

Hashes of kernel, input and output, plus work done, signed as an in-toto statement in DSSE.

03 · Replay

Replay to check

Re-execute on the pinned kernel, with the same input and seed. Output and work must match the receipt exactly.

Replay needs the exact kernel the receipt names, and it checks deterministic runs only. A run stopped by the host’s wall-clock safety net instead of its fuel budget is signed as terminated and is not replayable; whether that net fires depends on the host. Under emulation most deterministic Python runaways hit it before their fuel budget, and on QEMU 6.2 under emulation a runaway ends with no receipt at all when the VM time limit is 90 s or less. So replay is a check on a pinned kernel and a known host setup, not on any machine.

The trust gate

Nothing leaves until the receipt checks out.

Before an agent acts on a result, the gate checks its receipt and decides one of four things.

Send

Receipt verifies and replay matches. The action goes out.

Hold

The result checks out, but the draft doesn’t match its receipt or rests on stale data. The action waits for a fix.

Escalate

A duplicate, or a run too costly to recheck automatically. A person decides.

Refuse

Receipt is forged, altered or fails replay. The action is blocked.

Demo scenario

An agent calculates a customer refund

The agent writes code that computes the refund from an order export. Ampoule runs it and returns a receipt.
The receipt verifies and replay matches: send.
Someone changes the amount after the run: replay no longer matches, refuse.
The same refund is submitted twice: the second one is stopped, so it goes out exactly once (shown in simulation on real receipts).

Illustrative scenario, not a customer deployment. Replay proves what ran, not that the code was right, so the demo also checks the code against a second, held-out export.

Where it fits

Results the other side can re-run.

A receipt proves a program ran faithfully on the inputs it names. It does not prove the program is right: a flawed grader or a wrong fee rule still gets a valid receipt.

01 · RL graders

Scores a lab can re-run

A vendor’s grader, a deterministic program, scores an RL episode. The lab replays the grader on the same episode and gets the same score. The grader writes the episode’s ID into its output, so a receipt from a different episode shows up as a mismatch.

02 · Fees and settlements

Amounts the other side can replay

One party calculates a fee or refund. The other party replays the calculation on the same inputs and gets the same amount, or sees that it doesn’t match.

Direction, not a product

03 · Agent quotes

Quotes the payer can check

An agent quotes a total. Before paying, the other side re-runs how that total was calculated.

Today’s limits. Deterministic programs only, so not LLM judges or other model output. Inputs are small and runs are short. Replay needs the program, its inputs and the same pinned runtime. Container-based test runners, SWE-style test suites, pandas and numpy are not supported yet.

Verdicts

Only exit 0 with a final VERIFIED line is a pass.

ampoule-verify with the kernel pinned exits 0 and prints VERIFIED only when all of these hold:

the receipt is signed by a key you named (--key or --trusted-keys), checked with strict Ed25519;
every file you give it (program, output, kernel) matches the digest the receipt signed;
the signed run finished normally (status 0) and was not stopped by the host.

Every receipt forged without the signing key, or whose signed content was changed, fails with exit 1 (FAILED). For a deterministic run, verify --replay re-runs the program on the pinned kernel and prints REPLAY OK only when output, fuel and status match the receipt, so it does not depend on trusting the signer.

What a receipt does not prove. A signature is tamper evidence tied to a key, not remote attestation, so whoever holds the key can sign anything. A receipt of a host-stopped run (exit 3) or a failed run (exit 4) proves only that; a check without a pinned kernel (exit 5) is not a pass. Hypervisor escapes and side channels are out of scope.

exit	`ampoule-verify`	`verify --replay`
0	`VERIFIED` (kernel pinned)	`REPLAY OK`
1	`FAILED`	`REPLAY FAILED: <reason>`
2	usage or I/O error (also a weak key or an unreadable file)	usage (also a weak or malformed `--key`, or code over the 524,160-byte guest channel)
3	`NOT REPLAYABLE` (signature valid, host stopped the run)	`REPLAY N/A` (receipt has `terminated`)
4	`RUN FAILED` (signature valid, nonzero status)	`REPLAY MATCHED, RUN FAILED`
5	`INCOMPLETE` (signature valid, kernel not pinned; not a pass)	none (a replay re-runs the kernel it is given)
6	an input over 64 MiB	receipt or code file over 64 MiB

When several apply, the most serious wins: 2 (and 6) > 1 > 3 > 4 > 5 > 0. VERIFIED and REPLAY OK are printed only on exit 0. Decide on the exit code and the last result line.

A run that used up its fuel budget carries the signed field stop: "fuel": it stays replayable and verifies as RUN FAILED, exit 4. See the receipt spec.

Reproducible builds

Rebuild the kernel and tools, and compare the hashes yourself.

A receipt pins the kernel’s SHA-256, and replay needs that exact kernel. With --strict, the same commit builds the same kernel bytes on any machine and at any checkout path, and the same host-tool bytes on the same OS image.

./scripts/build-kernel.sh --strict       # reproducible kernel, checked against its pinned hash
./scripts/build-host-tools.sh --strict   # reproducible mcp, ampoule-verify, verify

The source code is private: only an auditor who has been given source access can rebuild the kernel with scripts/build-kernel.sh --strict and match the hash the receipt pins. Everyone else still relies on the binaries we publish.

--strict refuses a checkout with uncommitted changes in tracked files, or untracked files the commit does not ignore, so a MATCH under --strict means this exact commit builds this kernel.

For auditors:

Run the build scripts directly as ./scripts/…, not as bash scripts/…. Output from bash scripts/… proves nothing. Trust only output that contains MATCH lines and the printed commit SHA; an exit status of 0 on its own proves nothing.
Compare the commit SHA the script prints (note: --strict: commit <sha> …) with the commit you meant to build. That comparison is the real check that you built the source you were given.
Use a fresh TMPDIR outside the checkout, or leave it unset.

file	sha256 (published on main)	holds on
kernel	60ba914966395b267798704d26a7967dce69b902f10920625e403a856f6d1bf7	any host OS
mcp	760290153905cf72f49d3161e0696b103d496a3fccbf91a43e1a48466b413574	Debian 13, glibc 2.41, x86_64
ampoule-verify	713d2bf2d2067b19d9b1f58dd435eb1654dabb223587fb559c888822123be2cf	same image
verify	d2f9e87da97f10d37f63e106ed270c27bfdff8a9785314797546d478949413b4	same image

The host-tool hashes hold only on the OS image named above; on another image --strict exits 1, because the bytes can’t match there. The kernel hash holds on any host. The runtimes the kernel embeds are pinned too (python.wasm ff256a7e…, qjs-wasi.wasm 42a732a6…).

Building from source needs the pinned runtimes from the tester kit. The tester kit’s own tools come from an earlier main commit and are checked against the kit’s own SHA256SUMS, not the hashes above. There is no packaged release yet.

Open standards

Receipts in formats you already know.

No proprietary format to trust. A receipt is an in-toto statement in a DSSE envelope, signed with Ed25519, with a published predicate.

in-toto Statement v1 ↗

The attestation format for the receipt.

DSSE ↗

The signed envelope around it.

Ampoule run predicate v2 →

Every field a receipt records, and what a signature does and does not prove.

Tester kit v1

Try it without building anything.

The tester kit is available on request. Tell us what you want to check and we’ll get back to you.

Request the tester kit

Prebuilt kernel, verify, ampoule-verify and mcp.
The two pinned runtimes.
The Python agent adapter for the OpenAI Agents SDK and the Claude Agent SDK, with its quickstart and auditor guide.

Needs Linux x86_64 with glibc 2.34 or newer, QEMU 6.2 or newer and Python 3.10 or newer, and no API keys. Testers don’t rebuild anything. The kit carries its own SHA256SUMS file, and its files are checked against that. The kit is sent on request, not offered as a public download.

Status

Working prototype. Looking for design partners in finance, regulated AI and agent platforms.

If your agents act on code output and you need to show what ran, we'd like to hear from you.

or write to info@ampoule.dev