LLM agents that write machine-checked cryptographic proofs

The agent never drives the proof assistant directly. Each turn it reads a structured proof-state panel, answers with a single tool call, and a session manager applies it, checks it against EasyCrypt, and re-renders the view. Every accepted proof is admit-free and re-verified by an independent replay validator — each run is a fully auditable record of what the agent saw, chose, and proved.

What this tool does — and what you bring

A formal security proof moves through three phases (our paper, Fig. 1). Shannon Prover's scope is Phase III: you bring the security model (Phase I) and the decomposition into lemma-level obligations (Phase II), and it writes the tactic-level proof script for each lemma — the tedious, time-consuming part you can now delegate.

Phase I · expert

Security modeling

Express the scheme and its security notions as EasyCrypt modules and definitions — the games the whole argument is played in.

module CBC(P : PseudoRP) = {
proc enc(key, iv, p) = { … } }

Phase II · expert assistance coming — stay tuned

Lemma decomposition

Decompose the main theorem into intermediate lemma statements — the game hops that structure the proof. Extending Shannon Prover to assist here is our next step.

lemma CBC_PRP_RF · lemma Bound_by_Birthday · lemma CBC_upto

Phase III · Shannon Prover this project

Tactic-level lemma proving

Prove each lemma with a tactic script EasyCrypt accepts. Shannon Prover automates this phase — agents search and commit tactics until the checker says qed.

proof. byequiv=> //=. proc.
call (_: ={bad,qs} …). qed.

The phases feed back: a proved lemma lets the cryptographer proceed, while a stalled search is itself information — it often means the Phase II decomposition needs revising. “Given the decomposition, Shannon Prover can fully automate Phase III for MEE-CBC and ChaCha20-Poly1305 in a day.”

The MCP tool

Shannon Prover talks to the agent through the Model Context Protocol. The agent gets exactly one tool: submit_proof_intent — one proof-level action per turn. The always-available moves are deliberately few: commit a tactic, undo, rewind to a checkpoint, restart, finish. Every other intent is offered by the panel itself — when the proof state makes a lookup, a diagnosis, or a specialized view relevant, the panel surfaces it that turn.

Everything else stays behind the manager: the live EasyCrypt session, files, session state, repair prompts. When you run a proof, each tree node automatically gets its own private MCP server wired to a headless Claude Code instance — there is nothing to configure, and the agent physically can't touch the prover except through this tool.

commit_tacticundo_last_stepundo_to_checkpoint fresh_restartfinish

…plus the intents the panel offers in context, turn by turn.

submit_proof_intent

{ "intent": "commit_tactic",
  "payload": {
    "tactic": "while (={r} /\\ 1 <= r{1} <= 6)."
  } }

✓ commit accepted · panel re-rendered with the new goal

🔬 Goal-only mode minimal

The agent sees nothing but the produced EasyCrypt goal — the raw proof state, no analysis, no hints. The clean baseline for what a model can do alone.

surface profile: l1_goal_projection

🛠 Workbench mode default

The agent reads the full compiler surface: the analyzed goal, candidate moves, route health, and inspection handles it can pull on.

surface profile: l4_checked_action_surface

The two modes drive the same manager and the same EasyCrypt session — only the panel changes, which is exactly what our interface ablations measure. Flip between them live in the playground.

Run it yourself

Prerequisites: macOS or Linux, opam, Python ≥ 3.12 with uv, and the Claude Code CLI (logged in). Grab the source from github.com/SkyShannonProver/shannon-prover and run the steps below from the checkout.

Install EasyCrypt via opam

The pipeline expects the opam switch to be named easycrypt (configured in core/easycrypt/ec_env.py).

opam init
opam switch --empty create easycrypt
opam pin -yn add easycrypt https://github.com/EasyCrypt/easycrypt.git
opam install --deps-only easycrypt
opam install alt-ergo.2.6.0 easycrypt
easycrypt why3config

Then, in every shell that runs the prover or the playground:

eval "$(opam env --switch=easycrypt)"

Set up the Python environment

uv sync            # installs from pyproject.toml (Python ≥ 3.12)
claude --version   # the prover drives the Claude Code CLI — install & log in first

Open Claude Code and prove a lemma

The repo ships a /prove command. Open Claude Code in the checkout and point it at any lemma under eval/examples/:

# inside a Claude Code session opened on the repo:
/prove PIR_correct                        # Workbench mode (default)
/prove PIR_correct l1_goal_projection     # Goal-only mode

Claude finds the lemma's source, generates a one-target eval suite, and launches the run in eval mode — the source is copied into an isolated container and the target's proof body is stripped, so the agent proves it blind. All the MCP plumbing (per-node server, config, tokens) happens automatically. Equivalent direct command:

eval "$(opam env --switch=easycrypt)"
uv run python -m eval_suite.run --suite eval_suite/suites/demo_pir.json \
    --profiles l4_checked_action_surface

Read the results

Metrics land in artifacts/eval_suite/…/eval_metrics.md; every run also produces a replayable bundle under agent_view_runs/<lemma>/<timestamp>__<commit>/ — browse it turn by turn in the benchmark browser. A run counts as proved only if EasyCrypt accepts the complete proof with no admit. anywhere; the pipeline itself rejects proofs that still have one.

Good to know

why3server needs a real terminal. An OS sandbox that blocks the nice() syscall prevents why3server from starting, and smt() fails with “cannot start & connect to why3server”. Run outside sandboxes.
Eval isolation is deliberate. Don't hand-edit the checkout to help a proof — the run works on an isolated proof-stripped copy, and helping breaks the numbers.
Model default. Suites inherit claude-opus-4-8 at effort high; override with "model"/"effort" keys under the suite's defaults, or --prover-model/--prover-effort on direct workflow.orchestrator runs.
Playground: start it with uv run --with fastapi --with "uvicorn[standard]" uvicorn playground.server:app --port 8000 — local only, no auth layer; one EasyCrypt workload per checkout.

Explore

Playground ›

Take the agent's seat — drive a live EasyCrypt proof through the exact panel the agent reads.

pick a target file and lemma, press start
commit tactics and watch the panel re-render each turn
flip between Goal-only and Workbench mode live

Benchmark ›

Model capability board and replayable run bundles.

which models close which lemmas
every run replayable turn by turn — panel, thinking, tactic
proved = EasyCrypt-accepted, admit-free, replay-verified

Shannon Prover — research prototype paper (arXiv) source on GitHub questions? shannonprover@gmail.com EasyCrypt is developed upstream under its own license