# shannon-prover

**Repository Path**: uisu/shannon-prover

## Basic Information

- **Project Name**: shannon-prover
- **Description**: 基于llm的密码学证明器：https://github.com/SkyShannonProver/shannon-prover
- **Primary Language**: Unknown
- **License**: MIT
- **Default Branch**: main
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2026-10-19
- **Last Updated**: 2026-10-19

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# Shannon Prover

**From a security theorem to an EasyCrypt proof.**

Shannon Prover uses language-model agents to construct machine-checked
cryptographic proofs in [EasyCrypt](https://www.easycrypt.info).
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](https://arxiv.org/abs/2607.02847)
- **Website:** [project overview and proof browser](https://skyshannonprover.github.io/shannon-prover/)
- **Contact:** shannonprover@gmail.com · [GitHub](https://github.com/SkyShannonProver/shannon-prover)

## What does Shannon automate?

Think of formalizing a cryptographic security proof in three phases:

| Phase | Work to do | With Shannon Prover |
|---|---|---|
| **I — State the security problem** | Define the scheme, adversary, security games, assumptions, and final theorem in EasyCrypt. | You provide these. |
| **II — Build the security argument** | Choose intermediate games, formulate auxiliary lemmas, and connect them to the final theorem. | Shannon proposes and revises this decomposition. |
| **III — Prove each step** | Write the detailed EasyCrypt proofs of the lemmas and the final theorem. | Shannon searches for proof scripts and checks them with EasyCrypt. |

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.

```mermaid
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"]
```

## Install

Use macOS or Linux with Git, [opam](https://opam.ocaml.org), Python ≥ 3.12,
and [uv](https://docs.astral.sh/uv/).

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

```bash
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:

```bash
brew install opam autoconf automake pkgconf gmp pcre2 zlib
```

For other package managers, see the vendored
[EasyCrypt installation guide](easycrypt-src/INSTALL.md). 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:

```bash
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](https://github.com/Z3Prover/z3) and [CVC5](https://cvc5.github.io) 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:

```bash
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:

```bash
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:

```bash
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](workflow/interleaved/README.md#choose-the-agents-and-limits)
for model settings, login requirements, and time limits.

<a id="prove-a-security-theorem"></a>

## 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.

```text
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:

```json
{
  "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:

```bash
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`:

```bash
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](workflow/interleaved/README.md)
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](experiments/interleaved_shannon/README.md). 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.

<a id="prove-your-first-lemma"></a>

## 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:

```easycrypt
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:

```text
$prove PIR_correct
```

Claude Code has the corresponding command:

```text
/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](.agents/skills/prove/SKILL.md)
for the explicit-file command and other details.

## Examples and research evaluation

The [proof browser](https://skyshannonprover.github.io/shannon-prover/)
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](eval_suite/README.md) and
[ChaChaPoly reference guide](experiments/interleaved_shannon/README.md).

## Further reading

- [Project-level proving guide](workflow/interleaved/README.md): project setup, agents, limits, and results.
- [ChaChaPoly example](experiments/interleaved_shannon/README.md): reproduce the supplied security-proof task.
- [Architecture](docs/ARCHITECTURE.md): optional implementation details for contributors.

## License and citation

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

```bibtex
@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}
}
```