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.
Shannon Prover helps turn lemma-level cryptographic arguments into checked EasyCrypt proof scripts. You define the security model and proof structure; the agent works through each resulting obligation, one checked proof action at a time.

Where Shannon Prover fits

Shannon Prover works at Phase III today. You currently retain control of the security model and the proof's intermediate claims; support for Phase II lemma decomposition is under active development.

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 under active development
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.

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.
Goal after byequiv=> //=.
pre = (glob A){2} = (glob A){m} /\ (glob A){1} = (glob A){m}
INDR_CPA_direct(CBC_Oracle(DoubleQuery(Sample)), A).main
~ INDR_CPA_direct(Compute, A).main
post = DoubleQuery.bad{1} = Compute.bad{2}
Goal after by inline *; auto.
No more goals

The proof is shown exactly from proof. to qed.. Highlighted tactic lines point to the EasyCrypt goal immediately after that line runs.

How the LLM interacts with EasyCrypt

Through MCP, each proof turn is a loop among three roles: the LLM reasons about what to do, the manager and proof-state compiler mediate the current proof state, and EasyCrypt executes and checks every committed tactic.

✦
Proof reasoning

LLM

Reads the compiled proof state, chooses the next move, and submits one proof-level intent.

≡
State-aware interface

Manager + compiler

Owns the live proof session and presents the exact current goal, valid proof controls, and any bounded EasyCrypt-certified compiler output. It never chooses the proof strategy.

✓
Proof authority

EasyCrypt

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

Every turn carries exactly one proof intent. The manager applies it to EasyCrypt, returns the exact resulting goal or error, then compiles a bounded action surface for the unchanged current state. The agent uses that response to choose its next action.

Proof controls
Through submit_proof_intent, the agent can submit a tactic (commit_tactic) or use an available session control: Undo last (undo_last_step), Rewind (undo_to_checkpoint), Restart (fresh_restart), or Finish (finish). After a failed step, the manager may also offer guided amendment and replay (amend_and_replay).
Current panel
The current panel shows the exact EasyCrypt goal, the actions available now, and concise compiler guidance to help the agent decide what to do next.

Run Shannon Prover yourself

Ready to move from the paper to a live proof session? You need macOS or Linux, opam, Python ≥ 3.12, uv, and an authenticated proof-agent CLI. OpenAI Codex is the default; Claude is available when you explicitly choose it.

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.

Add your EasyCrypt project

Create one directory under projects/, put the target file and its project-owned .ec/.eca dependencies there, and leave the target lemma with an unfinished proof.

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

Start the proof agent

Run Codex from the repository and invoke the repo-scoped Prove skill. Claude Code provides the same one-argument interface through its project command:

# Codex — default backend and model
$prove my_lemma

# Claude Code — explicitly selects Claude
/prove my_lemma

The agent submits one intent per turn through submit_proof_intent. A proof is written back only after a fresh offline EasyCrypt verification succeeds.

Good to know
  • Codex is the default. The default model is gpt-5.6-sol with high reasoning effort; direct runs may select another backend, compatible model, and effort.
  • Ordinary use is not an evaluation run. $prove and /prove work directly on your project. Proof stripping and filesystem isolation belong only to controlled research evaluation.
  • EasyCrypt remains the authority. Compiler suggestions are bounded and state-bound; final success is reported only after independent offline verification.

See it in use

Run the prover ›

Install Shannon Prover and start a managed EasyCrypt proof from Codex or Claude.

  • bring your EasyCrypt project and unfinished lemma
  • submit one proof intent per checked turn
  • write back only after offline verification

Benchmark work in progress›

Development dashboard for our ongoing controlled evaluation across models.

  • the current examples and results are provisional
  • inspect the dashboard and replayable development runs
  • this is not yet a final model comparison
Shannon Prover — research prototype paper (arXiv) source on GitHub questions? shannonprover@gmail.com EasyCrypt is developed upstream under its own license