内容
# 香农证明器
**编写机器校验的密码学证明的LLM代理。**
香农证明器通过托管的证明会话将语言模型代理连接到
[EasyCrypt](https://www.easycrypt.info) 证明助手。代理永远不会直接驱动证明器：每回合它读取一个结构化的证明状态面板，回答一个工具调用，会议管理器应用它，检查它是否符合EasyCrypt，并重新渲染视图。每个被接受的证明都是无条件允许的，并且离线重新验证 - 每次运行都是一个完全可审计的记录，记录了代理看到的内容、选择的内容和证明的内容。
- **论文：** [香农证明器：迈向自动化形式化密码学证明](https://arxiv.org/pdf/2607.02847) (arXiv:2607.02847)
- **网站：** [skyshannonprover.github.io/shannon-prover](https://skyshannonprover.github.io/shannon-prover/) — 托管的首页 + 可重放运行的基准测试浏览器
- **联系方式：** shannonprover@gmail.com · [github.com/SkyShannonProver/shannon-prover](https://github.com/SkyShannonProver/shannon-prover)
- **本地站点：** 运行 [游乐场服务器](#游乐场和基准测试浏览器)
并打开 `http://127.0.0.1:8000/` 以获取引导式游览、实时游乐场和基准测试浏览器。
## 该工具的作用 — 以及您需要带来的
形式化安全证明经历三个阶段（论文，图 1）：
| 阶段 | 谁 | 做什么 |
|---|---|---|
| **I — 安全建模** | 专家 | 将方案及其安全概念表示为EasyCrypt模块和定义 |
| **II — 引理分解** | 专家 *(辅助即将到来 — 请关注)* | 将主要定理分解为中间引理语句 — 构成证明的游戏跳转 |
| **III — 战术级引理证明** | **香农证明器** | 用EasyCrypt接受的战术脚本证明每个引理 |
**香农证明器的范围是第三阶段**：您带来安全模型和分解成引理级义务，它为每个引理编写战术级证明脚本 — 这是您可以委派的繁琐、耗时的部分。阶段之间相互反馈：证明了的引理允许您继续，而停滞的搜索通常意味着第二阶段的分解需要修订。
## MCP工具
香农证明器通过
[模型上下文协议](https://modelcontextprotocol.io) 与代理通信。代理获得
**一个工具**，`submit_proof_intent` — 每回合一个证明级操作。始终可用的操作很少：提交战术、撤销、重置到检查点、重启、完成。所有其他意图（符号查找、诊断、专用视图）由面板本身在每回合中提供，当证明状态使其相关时。
除了经理之外，其他一切都留在后台：实时的EasyCrypt会话、文件、会话状态、修复提示。当您运行证明时，每个树节点自动获得自己的私有MCP服务器，连接到一个无头的Claude Code实例 — 无需配置，代理无法物理触及证明器，只能通过此工具。
```json
{"intent": "commit_tactic", "payload": {"tactic": "byequiv=> //."}}
```
### 两种界面模式
相同的引擎、管理器和EasyCrypt后端在下面运行；只有代理读取的面板会发生变化。这是我们的接口消融实验所测量的实验性拨盘（论文的L1/L4表面级别）：
| | **仅目标** (`l1_goal_projection`) | **工作台** (`l4_checked_action_surface`, 默认) |
|---|---|---|
| 代理看到的内容 | 基本上只是**当前目标** — 原始证明状态，无分析，无提示。 | 完整的`ProverWorkspaceView`：目标 **加上** 事实编译器骨架 — 程序前沿与对齐、调用站点结构、类型化的`candidate_moves`菜单和签名/桥引理查找句柄。 |
| 特征 | 模型的清洁基线，看看模型可以单独完成什么。 | 默认情况下，实际上尝试**关闭一个艰难的证明** — 大多数关系/概率证明需要结构图。 |
工作台显示的是**事实和合法选项**，而不是配方：它从不排名“最佳行动”，从不向代理提供策略，也没有任何启发式门控提交。代理选择行动；视图只告诉它在这里什么是合法的，哪些事实行动必须携带，哪些引理需要查找。
## 安装
先决条件：macOS 或 Linux，[opam](https://opam.ocaml.org)，Python ≥ 3.12
使用 [uv](https://docs.astral.sh/uv/) 和 Claude Code CLI（已安装并登录）。
### 1. 通过 opam 安装 EasyCrypt
管道希望 opam 切换到名为 `easycrypt` （在
`core/easycrypt/ec_env.py` 中配置）：
```bash
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
```
然后，在 **每个** 运行证明器或游乐场的 shell 中：
```bash
eval "$(opam env --switch=easycrypt)"
```
### 2. Python 环境
```bash
uv sync # 从 pyproject.toml 安装（Python >= 3.12）
claude --version # 证明器驱动 Claude Code CLI — 先安装并登录
```
默认证明模型为 `claude-opus-4-8`，努力程度为 `high`；在套件的 `defaults` 下或直接在 `workflow.orchestrator` 运行中覆盖，使用
`"model"`/`"effort"` 键或
`--prover-model`/`--prover-effort`。
### 3. 证明您的第一个引理
存储库附带了一个 `/prove` 命令，用于 Claude Code。打开 Claude Code 并将其指向 `eval/examples/` 下的任意引理：
```text
/prove PIR_correct # 工作台模式（默认)
/prove PIR_correct l1_goal_projection # 仅目标模式
```
Claude 查找引理的源代码，生成一个单目标评估套件，并在评估模式下启动运行 — 源代码被复制到隔离的容器中，目标的证明体被剥离，因此代理盲目地证明它。等效的直接命令：
```bash
eval "$(opam env --switch=easycrypt)"
uv run python -m eval_suite.run --suite eval_suite/suites/demo_pir.json \
--profiles l4_checked_action_surface
```
## 引入您自己的引理
将新的基准测试文件放在 `eval/examples/` 下 — 单个自包含的 `eval/examples/<name>.ec`，或包含目标和每个兄弟 `.ec`/`.eca` 文件的项目目录
`eval/examples/<project>/`。
在 `eval_suite/suites/` 下创建一个套件 JSON（复制 `demo_pir.json` 并编辑
`targets[0]`）：
```json
{
"suite": "local_<short_id>",
"profiles": ["l1_goal_projection", "l4_checked_action_surface"],
"defaults": {
"eval_mode": true,
"max_iterations": 1,
"timeout_minutes": 30,
"repeats": 1,
"output_dir": "artifacts/eval_suite",
"source_isolation": true,
"strip_proofs": true
},
"targets": [
{
"id": "<short_id>",
"file": "eval/examples/<project>/Target.ec",
"lemma": "<TargetLemmaName>",
"include_dir": "easycrypt-src/theories",
"copy_root": "eval/examples/<project>"
}
]
}
```
（省略 `copy_root` 以获取单个自包含文件。）始终先进行干运行并检查扩展命令指向隔离源下的
`artifacts/eval_suite/.../source/...`:
```bash
uv run python -m eval_suite.run --suite eval_suite/suites/local_<short_id>.json \
--profiles l4_checked_action_surface --dry-run
uv run python -m eval_suite.run --suite eval_suite/suites/local_<short_id>.json \
--profiles l4_checked_action_surface
```
## 阅读结果
指标位于 `artifacts/eval_suite/<suite>/<profile>/<target>/r01/`
（`eval_metrics.md`、`source_manifest.json`、`iteration_1/summary.json`）。每次运行还会自动构建**捆绑包** — 一个提交的、可点击的时间线，记录每一次操作：
```text
agent_view_runs/<lemma>/<TS>__<commit>/
timeline_report.md # 环境头部 + 每步表格 + 已提交证明
timeline_report.json
run_meta.json
views/<Tree_x_y>/turn_NNN.json # 代理在每一步看到的确切视图
```
每一行是一次操作 — *代理看到的视图 → 它提交的意图 → 管理员的结果*。浏览捆绑包的最好的方法是
[基准测试浏览器](#游乐场和基准测试浏览器)。如果运行在自动钩子触发之前被终止，请手动重建
`python3 -m workflow.validation.run_report_bundle <run_iteration_dir> --timestamp <TS> …`。
### 它真的证明了吗？
- 仅当最终证明包含 **无 `admit.`** 时，运行才是真正的成功 — `admit.` 将目标搁置一边而无需证明。管理器阻止 `finish`，同时提交的 admit 仍然存在，写回路径拒绝包含最终证明的证明，每份被接受的证明都通过新的离线 EasyCrypt 运行进行重新验证。在 `eval_metrics.md` 和捆绑包的 `## Agent's committed proof` 下阅读结果。
- **评估模式隔离是故意为之。** 运行器证明剥离隔离的副本；**不要** 编辑主检出以“帮助”证明 — 这会破坏隔离和数字。
- **`why3server` / 沙盒（#1 设置失败）。** 如果 OS 沙盒阻止 `nice()` 系统调用，`why3server` 永远不会启动，`smt()` 失败并显示 *"cannot start & connect to why3server"*。在沙盒外运行 EasyCrypt/Why3。
## 游乐场和基准测试浏览器
一个本地服务器托管引导式游览（ `/` ）、实时游乐场（ `/playground` — 选择一个引理，按下启动，观察面板和提交流），和基准测试浏览器（ `/results` — 模型能力板和每个记录的运行，可重放逐一回放）：
```bash
eval "$(opam env --switch=easycrypt)"
uv run --with fastapi --with "uvicorn[standard]" \
uvicorn playground.server:app --host 127.0.0.1 --port 8000
```
仅限本地 — 没有身份验证层；请将其绑定到 `127.0.0.1`，并且在同一检出中使用 EasyCrypt 运行评估套件时不要运行游乐场。
## 架构
```mermaid
flowchart TD
Orchestrator["workflow/orchestrator.py + tree policy<br/>proof-search strategy"] --> Runtime["workflow/proof_node_runtime.py<br/>long-lived proof node"]
Runtime --> Manager["workflow/proof_node_manager.py<br/>ProofNodeManager"]
Agent["Prover agent"] -->|"submit_proof_intent MCP tool<br/>JSON proof intent"| Runtime
Runtime -->|"private manager bridge"| Manager
Manager --> ReplMgr["ReplSessionManager<br/>session lifecycle"]
ReplMgr --> Backend["core/easycrypt backend<br/>session_cli/runtime/daemon"]
Backend --> EC["EasyCrypt REPL / daemon"]
Backend --> Events["events.jsonl + completed snapshot"]
Events --> Projection["session_projection.py"]
Projection --> ToolView["session_tool_view.py"]
Projection --> ContextView["session_agent_view.py<br/>ProofContextView"]
ToolView --> ContextView
Analysis["core/easycrypt/analysis<br/>ProofIR / candidate menu / actions"] --> ContextView
ContextView --> Workspace["session_prover_workspace_view.py<br/>ProverWorkspaceView"]
Analysis --> Navigator["workspace navigation adapters<br/>current-view map interpreter"]
Navigator --> Workspace
Workspace --> ViewMgr["session_workspace_view_manager.py<br/>sanitize/order/lint"]
ViewMgr -->|"IDE-style view"| Manager
Manager -->|"factual candidate_moves"| Runtime
Runtime -->|"bounded result + latest view ref"| Agent
ContextView --> Observer["workflow/session_observer.py"]
Workspace --> Observer
Observer --> Tree["workflow/progress.py"]
Events --> Acceptance["workflow/proof_acceptance.py"]
Acceptance --> Replay["workflow/validation/proof_replay.py"]
```
经验法则：
- 代理证明交互通过 `ProofNodeManager` 进行；
- 长期证明工作者通过节点特有的 `submit_proof_intent` MCP 工具和私有运行时桥接器向 Claude 公开交互；
- EasyCrypt 生命周期和突变由管理器通过
`ReplSessionManager` 拥有；
- 候选人和证据由 ProofContextView、ProofIR、ToolViews 和诊断产生；`ProverWorkspaceView` 仅过滤、排序、
编写和整理材料以供代理使用的界面；
- 工作流代码仅在事件合约验证和离线 EasyCrypt 验证后接受证明。
参见 [`docs/ARCHITECTURE.md`](docs/ARCHITECTURE.md) 以获取贡献者级别的详细讲解，以及 [`TESTING.md`](TESTING.md) 以获取回放、回归和 A/B 测试程序。
## 主要目录
```text
core/easycrypt/ EasyCrypt后端：会话运行时、事件、投影、
工作区视图、目标/ProofIR分析、引理搜索
workflow/ 协调器、树监管器、证明节点运行时 +
管理器 + MCP服务器、代理、验证（回放/审计）
eval/examples/ EasyCrypt基准测试语料库（仅数据）
eval_suite/ 基准测试运行器 + 检查的套件
agent_view_runs/ 已提交的运行捆绑包（在/results/下浏览）
playground/ 本地Web服务器：游览、实时游乐场、基准测试
bundle_browser/ 静态基准测试浏览器SPA + 清单构建器
tools/ 离线审计和分析工具箱（面板保真度、
面板值、L1-vs-L4指标）
tests/ 测试套件
easycrypt-src/ 供应商上游EasyCrypt（其自己的MIT许可证）
```
生成的运行输出位于 `artifacts/` 或 `workflow/runs/` 下；两者都
被gitignore。
## 许可证和引用
香农证明器在 [MIT License](LICENSE) 下发布。`easycrypt-src/` 目录在自己的 MIT 许可证下提供上游 EasyCrypt。
如果您在研究中使用香农证明器，请引用
([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}
}
```
香农证明器是一个研究原型：问题和讨论欢迎在
[github.com/SkyShannonProver/shannon-prover](https://github.com/SkyShannonProver/shannon-prover) 或
shannonprover@gmail.com。
