Shannon Prover

Towards automating formal cryptographic proofs

Our vision: formal cryptographic proofs should keep pace with cryptographic innovation. We are working toward a future where cryptographers can explore and verify security arguments earlier and faster, without compromising the rigor of machine checking.
You supply the scheme, security assumptions, and final theorem in EasyCrypt. Shannon Prover searches for the intermediate games and auxiliary lemmas, writes their proofs, and checks the complete development with EasyCrypt.

Where Shannon Prover fits

Shannon Prover automates proof construction across Phases II and III. Earlier Shannon workflows proved individual lemmas supplied by a human. Shannon can now also propose and revise the decomposition of the security argument. You still provide the formal security model and theorem in Phase I.

Phase I · expert
Security model
Specify the scheme, games, and security notions in EasyCrypt — the argument you want to establish.
module CBC(P : PseudoRP) = {
  proc enc(key, iv, p) = { … } }
Phase II · Shannon Prover available now
Lemma decomposition
Formulate the intermediate lemmas and game hops needed to decompose the security argument into tractable proof obligations.
lemma CBC_PRP_RF · lemma Bound_by_Birthday · lemma CBC_upto
Phase III · Shannon Prover available now
Write per-lemma proofs
Construct an EasyCrypt tactic script for each lemma. The agent proposes actions; EasyCrypt accepts or rejects every committed step.
proof. byequiv=> //=. proc.
call (_: ={bad,qs} …). qed.

How Shannon Prover builds a security proof

A coordinator agent develops the security argument and delegates proof tasks to other agents within Shannon Prover, called inner agents. An inner agent returns either a checked proof or feedback about what remains unresolved. The coordinator uses those results to refine the argument and assign further tasks.

Coordinator agent

Build the argument and delegate tasks

Choose intermediate games and lemmas, and delegate proof tasks at different levels of detail to the inner agents.

Assign the initial tasks

Proving and feedback — repeat as needed

Inner agents · Prove the task

Attempt the assigned proof

Work on the assigned task in EasyCrypt. Return a checked proof, or feedback explaining the remaining obstacles, to the coordinator.

Proof or feedback
Revised task
Coordinator · Learn from the attempt

Refine the argument

Incorporate proved results, use feedback to revise games or auxiliary lemmas, and delegate the next tasks.

For example, feedback from a game-hop proof may prompt a stronger auxiliary lemma and a new proof attempt. This exchange is what we mean by interleaved.

Once the complete argument is assembled
Final verification

Check the whole proof

EasyCrypt checks the complete development from start to finish, including the final theorem.

Follow the project-level proving guide to prepare a project and interpret the results. The proof browser below shows individual lemma attempts, not a complete interleaved run.

What an EasyCrypt proof looks like

Given a lemma, an EasyCrypt proof is a sequence of tactics that transforms its current goal until no obligations remain. Here is a complete four-tactic example from the public MEE-CBC development in this repository.

eval/examples/MEE-CBC/CBC.ecaDQ_Sample_Compute_pr
lemma
local lemma DQ_Sample_Compute_pr &m:
  Pr[INDR_CPA_direct(CBC_Oracle(DoubleQuery(Sample)),A).main() @ &m:
     DoubleQuery.bad] =
  Pr[INDR_CPA_direct(Compute,A).main() @ &m : Compute.bad]
proof
proof.  byequiv=> //=.  proc; call (_: ={bad,qs}(DoubleQuery,Compute)).  by conseq DQ_Sample_Compute_eq.  by inline *; auto.qed.
1After byequiv=> //=.
pre = … INDR_CPA_direct(…, A).main ~ INDR_CPA_direct(Compute, A).main post = DoubleQuery.bad{1} = Compute.bad{2}
2After by inline *; auto.
No more goals

The proof is shown exactly from proof. to qed.. The numbered highlights match the EasyCrypt goals shown after those steps. In the first goal, … abbreviates the precondition and a module argument for readability.

How an inner agent interacts with EasyCrypt

Each inner agent works on a proof task assigned by the coordinator, using the interface below to interact with EasyCrypt. For each lemma, it sees what EasyCrypt still needs to prove, tries a proof step, and reads the resulting goals or error. It can continue, undo a step, or try another approach.

✦
Proof reasoning

Inner agent

Reads the current goals and proposes the next proof step.

≡
State-aware interface

Shannon

Keeps track of the proof attempt, passes steps to EasyCrypt, and helps the agent use the available declarations and tactic syntax.

✓
Proof authority

EasyCrypt

Executes tactics and returns the resulting goal or error. Only checker-accepted steps enter the proof.

The agent can consult the allowed EasyCrypt source declarations as it works. EasyCrypt remains responsible for interpreting and checking the mathematics. Before a result is accepted, the proof is checked again independently of the interactive attempt.

Run Shannon Prover yourself

Choose how much of the argument you want Shannon Prover to construct. Both workflows use EasyCrypt, but they have different inputs and launch commands.

Phases II + III

Project-level proving

You provide the security model and final theorem. Shannon proposes the necessary games and auxiliary lemmas, proves them, and assembles the final argument.

Start from a terminal with a project configuration that names your target theorem.

Start a project proof
Phase III

Single-lemma proving

You have already chosen the lemma and stated it in EasyCrypt. Shannon searches for its proof.

Use $prove in Codex or /prove in Claude Code, followed by the lemma name.

Prove one lemma

You need macOS or Linux, Git, opam, Python ≥ 3.12, uv, and the agent CLIs you select. For project-level proving, the defaults use Claude Code for the overall argument and Codex for auxiliary lemmas, with their stored Claude and ChatGPT OAuth logins. Steps 1–2 install the shared tools; steps 3–4 launch a Phase II + III proof.

Set up the repository

git clone https://github.com/SkyShannonProver/shannon-prover.git
cd shannon-prover
uv sync

Install the locked EasyCrypt toolchain

Shannon Prover is locked to EasyCrypt r2026.06. The bootstrap command creates and verifies the repository-managed opam root and switch:

uv run python tools/bootstrap_easycrypt.py
uv run python tools/bootstrap_easycrypt.py --verify-only

Python entry points select this environment automatically; no ambient opam switch is required.

Choose the project's final security theorem

Create one directory under projects/ with your security model, final theorem, and local dependencies. Leave the target theorem's proof unfinished. Add interleaved_project.json using the project setup guide, then commit these files so the checkout is clean.

projects/
  my-proof/
    Target.ec
    Dependency.ec
    interleaved_project.json

Start a project proof — Phases II + III

From a terminal at the repository root, first check the setup without starting a proof-generating model:

uv run python -m workflow.interleaved \
  --project projects/my-proof/interleaved_project.json \
  --preflight-only

Once these pass, start the proof attempt:

uv run python -m workflow.interleaved \
  --project projects/my-proof/interleaved_project.json

This run works toward the final theorem named in your configuration and constructs the auxiliary lemmas it needs. To use Codex in both roles, add --outer-provider codex --inner-provider codex to both commands.

Good to know
  • Set the time limits before running. The example allows two auxiliary lemmas at once, up to two hours per attempt, and twelve hours overall. These limits are not a total spending cap.
  • Read the final result. A successful project-level run records status: "proved" and final_verification_passed: true in manifest.json. A verified auxiliary lemma alone is not the final theorem.
  • Review the generated changes. Shannon Prover edits your target during its attempt. Check that the final statements and assumptions express the security claim you intended.

Single-lemma proving — Phase III

After the shared installation in steps 1–2, put your EasyCrypt file and local dependencies under projects/, leaving the selected lemma's proof unfinished. Open Codex or Claude Code from the repository root and enter one of these commands inside that agent:

# In Codex
$prove my_lemma

# In Claude Code
/prove my_lemma

Replace my_lemma with the declaration's name. These commands target that one lemma; they do not launch the Phase II + III project workflow or require interleaved_project.json. The generated proof is written back only after EasyCrypt verification succeeds.

See the single-lemma proving guide for an example.

See it in use

Prove one lemma

Phase III: write the EasyCrypt proof of a lemma you have already stated.

  • bring your EasyCrypt project and unfinished lemma
  • try proof steps and inspect the remaining goals
  • write back only after offline verification

Start a project proof

Phases II + III: construct the security argument and its EasyCrypt proofs together.

  • start from your security model and final theorem
  • let Shannon propose games and auxiliary lemmas
  • check the complete development with EasyCrypt

Proofs & benchmarks

Explore cryptographic proof developments and recorded agent runs.

  • browse source files, lemmas and their complete proofs
  • follow proof construction and verification evidence
  • inspect single-lemma runs separately from case studies
Shannon Prover — research prototype paper (arXiv) source on GitHub questions? shannonprover@gmail.com EasyCrypt is developed upstream under its own license