SkyShannonProver/shannon-prover
GitHub: SkyShannonProver/shannon-prover
Shannon Prover 是一个利用 LLM 智能体在 EasyCrypt 中自动编写机器可检验密码学证明脚本的系统。
Stars: 4 | Forks: 0
# Shannon Prover
**编写机器可检验密码学证明的 LLM 智能体。**
Shannon Prover 通过受管理的证明会话，将语言模型智能体连接到
[EasyCrypt](https://www.easycrypt.info) 证明助手。智能体从不直接驱动证明器：
每一轮它会读取一个结构化的证明状态面板，以单次工具调用作为回应，
随后会话管理器会应用该调用，对照 EasyCrypt 进行检查，并重新渲染视图。
每个被接受的证明都不包含 `admit` 并且会进行离线重验证 —— 每次运行都是一份
关于智能体所看到的内容、做出的选择以及证明过程的完全可审计记录。
- **论文：** [ShannonProver: 走向自动化形式化密码学证明](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)
- **本地站点：** 运行[演练场服务器](#the-playground-and-the-benchmark-browser)
并打开 `http://127.0.0.1:8000/` 以获取引导教程、实时演练场和基准测试浏览器。
## 此工具的功能 —— 以及您需要提供什么
形式化安全证明经历三个阶段（论文，图 1）：
| 阶段 | 负责方 | 内容 |
|---|---|---|
| **I — 安全建模** | 专家 | 将方案及其安全概念表达为 EasyCrypt 模块和定义 |
| **II — 引理分解** | 专家 *（辅助功能即将推出 —— 敬请期待）* | 将主定理分解为中间引理陈述 —— 即构建证明的游戏跳跃 |
| **III — 战术级引理证明** | **Shannon Prover** | 使用 EasyCrypt 接受的战术脚本证明每个引理 |
**Shannon Prover 的范围是阶段 III**：您提供安全模型以及到引理级义务的分解，
它便会为每个引理编写战术级的证明脚本 —— 这是您现在可以委派的繁琐且耗时的部分。
各阶段之间存在反馈：证明成功的引理让您得以继续推进，而停滞的搜索通常意味着需要修改阶段 II 的分解。
## MCP 工具
Shannon Prover 通过 [Model Context Protocol](https://modelcontextprotocol.io) 与智能体进行通信。
智能体拥有且仅拥有**一个工具**，`submit_proof_intent` —— 每轮执行一个证明级别的操作。
始终可用的操作被刻意保持在很少的数量：提交 tactic、撤销、回退至检查点、重启、完成。
所有其他意图（符号查找、诊断、专用视图）在证明状态使其变得相关时，会由面板本身逐轮提供。
其他所有内容都隐藏在管理器之后：实时的 EasyCrypt 会话、文件、
会话状态、修复提示。当您运行证明时，每个树节点都会自动获得其专属的私有 MCP 服务器，
连接到一个无头模式的 Claude Code 实例 —— 无需任何配置，
且智能体在物理上除了通过此工具外，无法触碰证明器。
```
{"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 switch 被命名为 `easycrypt`（配置位于
`core/easycrypt/ec_env.py`）：
```
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 中：
```
eval "$(opam env --switch=easycrypt)"
```
### 2. Python 环境
```
uv sync # installs from pyproject.toml (Python >= 3.12)
claude --version # the prover drives the Claude Code CLI — install & log in first
```
默认的证明器模型是处于 `high` 努力程度下的 `claude-opus-4-8`；可以通过某个套件的 `defaults` 下的
`"model"`/`"effort"` 键进行覆盖，或者在直接运行 `workflow.orchestrator` 时
使用 `--prover-model`/`--prover-effort`。
提示：在没有供应商 API 密钥的 Claude 订阅下，启动运行时
请取消设置供应商密钥变量（`env -u ANTHROPIC_API_KEY …`），以便 CLI 使用
您的登录状态。
### 3. 证明您的第一个引理
该仓库为 Claude Code 提供了一个 `/prove` 命令。在检出版本中打开 Claude Code，
并将其指向 `eval/examples/` 下的任意引理：
```
/prove PIR_correct # Workbench mode (default)
/prove PIR_correct l1_goal_projection # Goal-only mode
```
Claude 会找到该引理的源码，生成一个单目标的评估套件，
并在评估模式下启动运行 —— 源码会被复制到一个隔离的容器中，
并且目标的证明体会被剥离，因此智能体是在盲状态下进行证明的。
等效的直接命令：
```
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/.ec`，或者是包含目标及其导入的所有同级 `.ec`/`.eca`
文件的项目目录 `eval/examples//`。
在 `eval_suite/suites/` 下创建一个 JSON 套件（复制 `demo_pir.json` 并编辑
`targets[0]`）：
```
{
"suite": "local_",
"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": "",
"file": "eval/examples//Target.ec",
"lemma": "",
"include_dir": "easycrypt-src/theories",
"copy_root": "eval/examples/"
}
]
}
```
（如果是单个自包含文件，则省略 `copy_root`。）务必先进行干运行，并
检查展开后的命令是否指向位于
`artifacts/eval_suite/.../source/...` 下的隔离源码：
```
uv run python -m eval_suite.run --suite eval_suite/suites/local_.json \
--profiles l4_checked_action_surface --dry-run
uv run python -m eval_suite.run --suite eval_suite/suites/local_.json \
--profiles l4_checked_action_surface
```
## 解读结果
指标会存放在 `artifacts/eval_suite////r01/`
（`eval_metrics.md`，`source_manifest.json`，`iteration_1/summary.json`）。每次
运行还会自动构建 **bundle** —— 这是每一次
回合的可点击且已提交的时间线：
```
agent_view_runs//__/
timeline_report.md # env header + per-step table + committed proof
timeline_report.json
run_meta.json
views//turn_NNN.json # the exact view the agent saw at each turn
```
每一行代表一个回合 —— *智能体看到的视图 → 它提交的意图 →
管理器给出的结果*。浏览 bundle 的最佳方式是使用
[基准测试浏览器](#the-playground-and-the-benchmark-browser)。如果某次运行在
自动钩子触发前被终止，可以通过
`python3 -m workflow.validation.run_report_bundle --timestamp …` 手动重建。
### 它真的证明了吗？
- 只有当最终证明**不包含 `admit.`** 时，运行才算真正的成功 ——
`admit.` 会在未证明的情况下将目标搁置。只要已提交的 admit 仍然存在，管理器就会阻止 `finish`，
回写路径会拒绝包含它的最终证明，并且每个被接受的证明都会通过全新的离线
EasyCrypt 运行进行重验证。请在 `eval_metrics.md` 中读取结果，并在 bundle 的
`## Agent's committed proof` 下查看证明体。
- **评估模式下的隔离是刻意设计的。** 运行器会剥离一份隔离副本；请**不要**
为了“帮助”完成证明而手动编辑主检出目录 —— 这会
破坏隔离性并影响数据准确性。
- **`why3server` / 沙盒（头号设置失败原因）。** 如果 OS 沙盒阻止了
`nice()` 系统调用，`why3server` 将永远无法启动，且 `smt()` 会失败并提示
*"cannot start & connect to why3server"*。请在沙盒之外运行 EasyCrypt/Why3。
## 演练场和基准测试浏览器
一个本地服务器托管了引导教程（`/`）、实时演练场（`/playground`
—— 选择一个引理，按开始，观看面板和提交的实时流），以及
基准测试浏览器（`/results/` —— 模型能力排行榜以及所有记录在案的
运行记录，均可逐回合重放）：
```
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 时，请不要运行演练场。
## 架构
```
flowchart TD
Orchestrator["workflow/orchestrator.py + tree policy
proof-search strategy"] --> Runtime["workflow/proof_node_runtime.py
long-lived proof node"] Runtime --> Manager["workflow/proof_node_manager.py
ProofNodeManager"] Agent["Prover agent"] -->|"submit_proof_intent MCP tool
JSON proof intent"| Runtime Runtime -->|"private manager bridge"| Manager Manager --> ReplMgr["ReplSessionManager
session lifecycle"] ReplMgr --> Backend["core/easycrypt backend
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
ProofContextView"] ToolView --> ContextView Analysis["core/easycrypt/analysis
ProofIR / candidate menu / actions"] --> ContextView ContextView --> Workspace["session_prover_workspace_view.py
ProverWorkspaceView"] Analysis --> Navigator["workspace navigation adapters
current-view map interpreter"] Navigator --> Workspace Workspace --> ViewMgr["session_workspace_view_manager.py
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"] KB["knowledge/base/agent/*"] --> Agent ``` 经验法则： - 面向智能体的证明交互通过 `ProofNodeManager` 进行； - 长生命周期的证明器 worker 通过逐节点的 `submit_proof_intent` MCP 工具和私有运行时桥接将该交互暴露给 Claude； - EasyCrypt 的生命周期和状态变更由管理器通过 `ReplSessionManager` 负责控制； - 候选方案和证据由 ProofContextView、ProofIR、ToolViews、 诊断和 KB 源生成；`ProverWorkspaceView` 仅负责为面向智能体的表层 过滤、排序、润色和检查这些素材； - 工作流代码仅在通过事件契约验证和离线 EasyCrypt 验证后才会接受证明。 请参阅 [`docs/ARCHITECTURE.md`](docs/ARCHITECTURE.md) 获取贡献者级别的 详细说明，以及 [`TESTING.md`](TESTING.md) 了解重放、回归和 A/B 测试流程。 ## 主要目录 ``` core/easycrypt/ EasyCrypt backend: session runtime, events, projection, workspace views, goal/ProofIR analysis, lemma search workflow/ orchestrator, tree supervisor, proof-node runtime + manager + MCP server, agents, validation (replay/audit) knowledge/ prover-facing KB build/search (+ gitignored trace stores) eval/examples/ EasyCrypt benchmark corpus (data only) eval_suite/ benchmark runner + checked-in suites agent_view_runs/ committed run bundles (browse at /results/) playground/ the local web server: tour, live playground, benchmark bundle_browser/ static benchmark-browser SPA + manifest builder tools/ offline audit & analysis toolboxes (panel fidelity, panel value, L1-vs-L4 metrics) tests/ test suite easycrypt-src/ vendored upstream EasyCrypt (its own MIT license) ``` 生成的运行输出归属于 `artifacts/` 或 `workflow/runs/`；两者均 被 gitignored。 ## 许可证与引用 Shannon Prover 基于 [MIT 许可证](LICENSE) 发布。 `easycrypt-src/` 目录包含了上游 EasyCrypt，其遵循自身的 MIT 许可证。 如果您在研究中使用了 Shannon Prover，请引用 （[CITATION.cff](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} } ``` Shannon Prover 是一个研究原型：欢迎在 [github.com/SkyShannonProver/shannon-prover](https://github.com/SkyShannonProver/shannon-prover) 或 shannonprover@gmail.com 提交问题与进行讨论。
proof-search strategy"] --> Runtime["workflow/proof_node_runtime.py
long-lived proof node"] Runtime --> Manager["workflow/proof_node_manager.py
ProofNodeManager"] Agent["Prover agent"] -->|"submit_proof_intent MCP tool
JSON proof intent"| Runtime Runtime -->|"private manager bridge"| Manager Manager --> ReplMgr["ReplSessionManager
session lifecycle"] ReplMgr --> Backend["core/easycrypt backend
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
ProofContextView"] ToolView --> ContextView Analysis["core/easycrypt/analysis
ProofIR / candidate menu / actions"] --> ContextView ContextView --> Workspace["session_prover_workspace_view.py
ProverWorkspaceView"] Analysis --> Navigator["workspace navigation adapters
current-view map interpreter"] Navigator --> Workspace Workspace --> ViewMgr["session_workspace_view_manager.py
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"] KB["knowledge/base/agent/*"] --> Agent ``` 经验法则： - 面向智能体的证明交互通过 `ProofNodeManager` 进行； - 长生命周期的证明器 worker 通过逐节点的 `submit_proof_intent` MCP 工具和私有运行时桥接将该交互暴露给 Claude； - EasyCrypt 的生命周期和状态变更由管理器通过 `ReplSessionManager` 负责控制； - 候选方案和证据由 ProofContextView、ProofIR、ToolViews、 诊断和 KB 源生成；`ProverWorkspaceView` 仅负责为面向智能体的表层 过滤、排序、润色和检查这些素材； - 工作流代码仅在通过事件契约验证和离线 EasyCrypt 验证后才会接受证明。 请参阅 [`docs/ARCHITECTURE.md`](docs/ARCHITECTURE.md) 获取贡献者级别的 详细说明，以及 [`TESTING.md`](TESTING.md) 了解重放、回归和 A/B 测试流程。 ## 主要目录 ``` core/easycrypt/ EasyCrypt backend: session runtime, events, projection, workspace views, goal/ProofIR analysis, lemma search workflow/ orchestrator, tree supervisor, proof-node runtime + manager + MCP server, agents, validation (replay/audit) knowledge/ prover-facing KB build/search (+ gitignored trace stores) eval/examples/ EasyCrypt benchmark corpus (data only) eval_suite/ benchmark runner + checked-in suites agent_view_runs/ committed run bundles (browse at /results/) playground/ the local web server: tour, live playground, benchmark bundle_browser/ static benchmark-browser SPA + manifest builder tools/ offline audit & analysis toolboxes (panel fidelity, panel value, L1-vs-L4 metrics) tests/ test suite easycrypt-src/ vendored upstream EasyCrypt (its own MIT license) ``` 生成的运行输出归属于 `artifacts/` 或 `workflow/runs/`；两者均 被 gitignored。 ## 许可证与引用 Shannon Prover 基于 [MIT 许可证](LICENSE) 发布。 `easycrypt-src/` 目录包含了上游 EasyCrypt，其遵循自身的 MIT 许可证。 如果您在研究中使用了 Shannon Prover，请引用 （[CITATION.cff](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} } ``` Shannon Prover 是一个研究原型：欢迎在 [github.com/SkyShannonProver/shannon-prover](https://github.com/SkyShannonProver/shannon-prover) 或 shannonprover@gmail.com 提交问题与进行讨论。
标签：DLL 劫持, EasyCrypt, 大语言模型, 定理证明器, 密码学证明, 形式化验证, 漏洞数据库, 逆向工具