Shannon Prover

From a security theorem to an EasyCrypt proof.

Shannon Prover uses language-model agents to construct machine-checked cryptographic proofs in EasyCrypt. You supply the formal description of the scheme, its security assumptions, and the theorem you want to prove. Shannon Prover automates the search for both the proof decomposition and the proofs of its individual lemmas. It can introduce intermediate games and auxiliary lemmas, try to prove them, and revise the argument as EasyCrypt exposes what remains to be shown.

• Paper: ShannonProver: Towards Automating Formal Cryptographic Proofs

• Website: project overview and proof browser

• Contact: shannonprover@gmail.com · GitHub

What does Shannon automate?

Think of formalizing a cryptographic security proof in three phases:

Phases II and III need not happen in a single forward pass. For example, while trying to justify a game hop, Shannon may discover that a proposed invariant is insufficient. It can refine the auxiliary lemma, try its proof again, and then return to the main argument. This feedback between designing the argument and proving its steps is what we mean by interleaved.

One agent works on the overall argument. It can write proofs directly and ask other agents to work on selected auxiliary lemmas. Their results feed back into the overall proof, which is checked again as a complete EasyCrypt file.

flowchart LR
    Input["You: scheme, assumptions,<br/>security games and theorem"] --> Plan["Shannon: propose games<br/>and auxiliary lemmas"]
    Plan --> Proof["Shannon: write and check<br/>EasyCrypt proofs"]
    Proof -->|"results and remaining goals"| Plan
    Proof --> Final["Check the complete<br/>EasyCrypt development"]

Related MCP server: math-logic-mcp

Install

Use macOS or Linux with Git, opam, Python ≥ 3.12, and uv.

Install the system build tools and native libraries before bootstrapping EasyCrypt. On Ubuntu/Debian:

sudo apt-get update
sudo apt-get install -y git curl opam build-essential autoconf automake m4 pkg-config \
  libgmp-dev libpcre2-dev zlib1g-dev unzip

On macOS, install Xcode Command Line Tools (xcode-select --install if needed). If you use Homebrew, install the native dependencies with:

brew install opam autoconf automake pkgconf gmp pcre2 zlib

For other package managers, see the vendored EasyCrypt installation guide. Shannon's bootstrap builds the OCaml dependencies but expects these system dependencies to be installed already.

1. Python environment

Install uv outside this project's .venv, then synchronize the locked Python environment:

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

2. SMT solvers

EasyCrypt's smt tactic calls external solvers. Install Z3 and CVC5 and put their executables on your PATH before bootstrapping. CI uses Z3 4.15.4 and CVC5 1.2.1. Check that both commands work:

z3 --version
cvc5 --version

The next step installs Alt-Ergo 2.4.3 in Shannon's managed opam switch.

3. Repository-managed EasyCrypt

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

SHANNON_OPAM_ROOT="$(uv run python -c \
  'from core.easycrypt.toolchain import managed_opam_root; print(managed_opam_root())')"
SHANNON_OPAM_SWITCH="$(uv run python -c \
  'from core.easycrypt.toolchain import managed_switch_name; print(managed_switch_name())')"
opam install --yes --root "$SHANNON_OPAM_ROOT" \
  --switch "$SHANNON_OPAM_SWITCH" alt-ergo.2.4.3

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

The solver configuration lives in .toolchains/opam-r2026.06/why3.conf. Installing Alt-Ergo can cause opam to rebuild EasyCrypt dependencies. The second bootstrap command records and verifies the resulting installation as well as refreshing its solver configuration.

Worktrees of one repository share this configuration; independent clones have their own. Bootstrap and runtime checks preserve your global Why3 configuration. After changing solvers on PATH, rerun --configure-solvers. After package changes in the managed opam switch, rerun the full bootstrap instead. Existing Shannon installations need --configure-solvers once to create the local config if their recorded toolchain is otherwise unchanged.

Python entry points select this environment and configuration automatically. For a developer command that invokes easycrypt directly, export the verified environment and pass the configuration explicitly:

eval "$(uv run python tools/bootstrap_easycrypt.py --print-env)"
easycrypt -why3 "$SHANNON_WHY3_CONFIG" config

--verify-only and runtime availability checks read the configuration without regenerating it.

4. Agent login

Project-level proving defaults to OpenAI Codex with gpt-6-astra (high reasoning effort) for both the overall argument (outer) and auxiliary lemmas (inner). Install Codex and authenticate with a stored ChatGPT OAuth login. The commands below use this pair without additional provider flags. Claude Code remains available when explicitly selected for either role. See the project-level proving guide for model settings, login requirements, and time limits.

Project-level proving

This workflow covers Phases II and III: Shannon constructs the proof decomposition and the proofs needed to reach your project's final theorem.

Put your EasyCrypt target and its local dependencies in one directory under projects/. The file should contain the security model and final theorem, with an unfinished proof. You do not need to supply a decomposition into auxiliary lemmas.

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

Create interleaved_project.json with the following contents, replacing the file and theorem names with yours:

{
  "schema_version": 1,
  "target_file": "projects/my-proof/Target.ec",
  "final_lemma": "TargetSecurity",
  "include_dirs": ["easycrypt-src/theories", "projects/my-proof"],
  "artifact_root": "artifacts/my-proof-interleaved",
  "max_parallel": 2,
  "max_inner_minutes": 120,
  "outer_timeout_seconds": 43200
}

This allows at most two auxiliary-lemma attempts at once, up to two hours per attempt, and a twelve-hour overall task. These are time limits, not a total spending cap. Adjust them before running.

Commit your project files and configuration: the runner requires a clean Git working tree, including for the preliminary check. Then, from the repository root, check the setup without starting a proof-generating model:

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

If the check passes, run the same command without --preflight-only:

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

Shannon works on the target file in your checkout and prints the directory containing the run's results. The project-level proving guide explains how to read the outcome, continue partial work, and add checks that protect your original theorem and assumptions.

For a supplied cryptographic task, follow the ChaChaPoly example. It includes a security model and target theorem, without a human-supplied decomposition, and uses stricter checks that preserve the supplied problem.

What counts as a proof?

For an interleaved run, success requires a fresh EasyCrypt check of the complete target file and no remaining admit. in that file. The run's manifest.json records status: "proved" and final_verification_passed: true; final_verification.json contains the final checking result. A completed auxiliary lemma alone does not establish the final theorem. A partial proof is reported as incomplete.

EasyCrypt checks the statements in the submitted development under its assumptions. You should also review that these are the security statement and assumptions you intended. The generic checker does not freeze the original definitions or prohibit new assumptions; projects needing those restrictions must supply additional checks. The ChaChaPoly example supplies them for its fixed task.

Single-lemma proving

This workflow covers Phase III for a lemma you have already stated.

The standalone Codex prover defaults to gpt-5.6-sol with high reasoning effort. Project-level proving uses gpt-6-astra with high reasoning effort for both outer and inner agents, as described above. Both workflows default to Codex; their model settings are separate.

If you already know the decomposition, you can ask Shannon to prove one lemma. Put its EasyCrypt file and local dependencies under projects/, leaving the selected lemma with an unfinished proof, for example:

lemma my_lemma : true.
proof.
  admit.
qed.

Run Codex from the repository and enter $prove my_lemma. In the Codex desktop app, type / and choose Prove from the skills list. It searches projects/ first, then the bundled eval/examples/. For example, the supplied PIR lemma can be launched with:

$prove PIR_correct

Claude Code has the corresponding command:

/prove PIR_correct

These commands prove a selected lemma; they do not start the interleaved project-level workflow. The Codex command uses Codex, and the Claude command uses Claude. A generated proof is written back only after a fresh EasyCrypt verification succeeds. See the Prove instructions for the explicit-file command and other details.

Examples and research evaluation

The proof browser shows recorded single-lemma attempts and their checked steps. It does not yet show the complete sequence of game choices, auxiliary-lemma attempts, and revisions in an interleaved run.

Research evaluation is a different workflow

You do not need eval_suite to run an ordinary proof on your own project. Controlled evaluations additionally hide existing answers and fix the task, models, and budgets so results can be compared. Strict live evaluation currently requires Linux and bubblewrap when using the isolated benchmark suite; the ChaChaPoly reference has its own documented source-access policy. See the benchmark guide and ChaChaPoly reference guide.

Further reading

• Project-level proving guide: project setup, agents, limits, and results.

• ChaChaPoly example: reproduce the supplied security-proof task.

• Architecture: optional implementation details for contributors.

License and citation

Shannon Prover is released under the MIT License. The vendored EasyCrypt source has its own MIT license. If you use Shannon Prover in research, please cite CITATION.cff:

@article{ma2026shannonprover,
  title   = {ShannonProver: Towards Automating Formal Cryptographic Proofs},
  author  = {Ma, Yiping and Tsai, Yu-Lin and Rathee, Mayank and Rathee,
             Deevashwer and Dupressoir, Fran\c{c}ois and Strub, Pierre-Yves
             and Popa, Raluca Ada},
  journal = {arXiv preprint arXiv:2607.02847},
  year    = {2026}
}