frama-c-mcp

这是什么？适合谁？

frama-c-mcp（sysprog21/frama-c-mcp，15 Stars，MIT）是一个 MCP server，把 Frama-C 的形式化验证能力交给 AI Agent 驱动。Frama-C 是 C 代码静态分析的工业级框架，frama-c-mcp 让 Agent 能调用它的核心三件套：

• EVA：抽象解释，推导程序所有执行路径上的变量取值区间
• WP：演绎验证，把 C 代码 + ACSL 规约转成证明义务，交给 SMT 求解器证明
• ACSL 注解注入：自动生成/注入函数契约（前置/后置条件、循环不变式）到 C 源码

它的设计哲学写得很清楚：「server 是被 Agent 驱动的，不是被人驱动的」——没有给人敲的命令行，一切通过 MCP stdio 交互。核心工作流是一个迭代循环：提出注解 → 证明它 → 读失败目标的原因 → 修订。项目会话跨调用保持（一次加载整个项目），沙箱按名字寻址，证明回执只在同一次运行内比较。

架构是三层：AI Agent ⇄（MCP stdio）⇄ Rust MCP server ⇄（Unix socket）⇄ Frama-C 主进程 + 每个实验一个独立的 Frama-C 沙箱（create_sandbox 会把目标函数连同其类型、被调用者、全局依赖抽到临时 C 文件再开独立进程跑验证）。还有一个 check 子命令供 CI 使用——这是唯一为人设计的入口。

出品方是 sysprog21（台湾系统程式社群，Linux 核心与系统能力培养营的社群组织），在 C 语言工程教育深耕多年，C 代码正确性验证方向国内罕见。

适合人群：

• 安全关键 C 代码（内核模块/固件/工控）的工程师：想给 AI 生成代码上「数学证明」保险
• 形式化方法学习者：用 Agent 对话的方式入门 Frama-C/EVA/WP
• 编译器/静态分析研究者：把 Frama-C 接入 LLM 工作流做混合验证实验

不适合：非 C 语言项目；想「一键全自动证明」的用户（证明循环仍需人盯失败目标）；Windows 原生环境（Frama-C 生态以 Linux 为主）。

使用前提：Linux + opam 环境 + Frama-C 与配套 ast-utils 插件（同 opam switch）；Rust 工具链（构建 server）。

准备工作

1. Frama-C：通过 opam 安装（如 opam install frama-c），与 ast-utils 插件装在同一 switch。
2. Rust 工具链：rustup，用于构建 MCP server。
3. MCP 客户端：Claude Code / Claude Desktop 等。
4. 成本：全部开源免费；消耗自己 LLM tokens。
5. 时间预算：环境搭建 30-60 分钟（opam 依赖编译较久）；上手验证第一个函数约 15 分钟。

快速上手（3 步）

第一步：环境就绪

# opam 环境 + Frama-C + ast-utils（同 switch）
opam install frama-c
# 构建 MCP server
cargo build --release

第二步：接入 MCP 客户端

在 Claude Code / Claude Desktop 配置中添加 frama-c-mcp（stdio 传输），指向构建出的二进制。

第三步：跑第一个证明循环

对 Agent 说（英文 prompt 效果最佳）：

Load the project in ./src, pick function parse_header,
write a function contract in ACSL (requires/ensures),
and prove it with WP. Report which goals fail and why.

预期结果：Agent 加载项目 → 注入 ACSL 注解 → 调 WP 证明 → 拿到失败目标清单与原因 → 修订注解再证，最终报告「全目标闭合」或剩余风险。

常见踩坑

踩坑 1：Frama-C/ast-utils 版本不匹配

• 现象：server 起动后工具调用报协议错误。
• 原因：ast-utils 插件与 Frama-C 版本必须同 switch 配套。
• 解决：严格按仓库文档在同一 opam switch 安装两者。

踩坑 2：沙箱抽取漏依赖

• 现象：沙箱里证明结果与主项目不一致。
• 原因：create_sandbox 按依赖分析抽取函数及其类型/被调用者/全局依赖，复杂全局状态可能抽取不全。
• 解决：先用 EVA 在主项目跑一遍取值信息，再开沙箱；复杂函数直接在主项目验证。

踩坑 3：循环不变式写不出

• 现象：WP 对循环体目标全部失败。
• 原因：ACSL 循环不变式是证明闭合的关键也是最难写的部分。
• 解决：让 Agent「先证不含循环的版本，再逐步加不变式」，渐进式逼近。

踩坑 4：SMT 求解器超时

• 现象：证明目标 pending 不返回。
• 原因：默认求解器（Alt-Ergo/Z3 等）对复杂目标耗时。
• 解决：增加超时预算、分拆目标、或提示 Agent 弱化注解分步证。

踩坑 5：证明回执跨运行比较

• 现象：两次运行的回执对不上。
• 原因：设计上 proof receipts 只在同一次 run 内可比。
• 解决：以「一次 run 内的目标闭合率」为进度指标，别跨 run 对账。

踩坑 6：把 EVA 和 WP 混着用却期待相同结论

• 现象：EVA 说区间 OK、WP 说证明失败，困惑。
• 原因：两者机制不同——EVA 是过近似分析（可能误报），WP 是精确证明义务（可能因注解不足失败）。
• 解决：工作流上先 EVA 探路（找可疑点）再 WP 证明（下结论）。

初级用法

1. 单函数契约验证：挑一个纯函数（无副作用），让 Agent 写 requires/ensures 并证明——15 分钟体验完整闭环。
2. EVA 取值探路：对可疑函数跑 EVA，让 Agent 解读变量区间报告，标出潜在除零/越界。
3. 注解体检：对已有 ACSL 注解的代码，让 Agent 检查注解是否真的能证（防止「写了但证不了」的装饰性注解）。
4. CI 集成：用 check 子命令把「注解可证明」纳入 CI 门禁。

高级玩法

1. AI 写代码 + AI 证明代码：让 Agent 先实现一个 C 函数，再用同一会话生成契约并证明——「生成即验证」的完整流水线。
2. 反例驱动开发：WP 失败目标本身就是反例线索，让 Agent 据此修代码或补约束，迭代收敛。
3. 内核代码审计：对开源内核模块（如 Linux 驱动片段）做 EVA+WP 混合分析，产出「数学证据支撑」的审计报告。
4. 教学场景：让 Agent 出题（带 bug 的 C 函数）+ 学员用 Agent 辅助写注解定位 bug——形式化方法教学的新形态。

小技巧

1. 英文 prompt：README 明确说「prompt in English」，工具描述与提示模式按英文打磨。
2. 一个项目一个会话：会话状态跨调用保持，别在同一个 server 实例里混多个项目。
3. 先简后繁：从纯函数到带循环函数再到指针操作，注解难度陡增。
4. 读失败原因再动手：WP 的失败 goal 输出是修订注解的金矿，别急着换思路。
5. opam 慢就预热：依赖编译期间正好读 Frama-C 文档。

常见问题 FAQ

Q1：它能自动证明任意 C 代码正确吗？

A：不能。它提供的是「Agent 驱动的证明循环」：注解仍需设计（Agent 提案、人可干预），不可判定性决定了没有全自动保证。来源：README

Q2：支持 C++ 吗？

A：Frama-C 生态聚焦 C；C++ 支持有限（模板等基本不可用）。

Q3：为什么设计成「Agent 驱动、无人命令」？

A：迭代证明循环（提议-证明-读失败-修订）天然是多轮对话形态，LLM Agent 是最合适的驱动者；人只需 CI 里的 check。来源：README

Q4：能找内存安全漏洞吗？

A：EVA+WP 组合可证内存安全性（如某指针访问永不出界），前提是注解写到位；比 fuzzing 给出的是更强的确定性结论。

Q5：和 CBMC/KLEE 类工具有何区别？

A：CBMC 是有界模型检查、KLEE 是符号执行——都给出反例但覆盖有界；Frama-C WP 是无界演绎证明（配好注解可证全路径），定位互补。

进阶学习建议

• 吃透「沙箱」设计：读 README Architecture 一节，理解 create_sandbox 如何把函数+依赖抽到隔离环境做实验——这个「以函数为单位的验证沙箱」模式，是大规模项目里控制验证爆炸半径的关键技巧。
• 练 ACSL 注解的渐进式写法：从 ensures \result == x*y 级别的朴素契约，到循环不变式、谓词抽象，逐步加码；让 Agent 每次只加一条注解并跑证明，你会直观看到每条注解闭合了哪些 goal。
• 关注 sysprog21 生态：出品方是台湾系统程式社群，周边有大量 C 语言工程与验证教学资源，适合作为中文母语者入门形式化方法的支点。

参考链接

• frama-c-mcp GitHub 仓库
• Frama-C 官网
• ACSL 规范文档
• sysprog21 社群

免责声明：本文基于官方仓库 README 与 GitHub 公开数据整理，AI 辅助生成，MagicNetWorld 尚未完成独立实测。形式化验证环境的搭建与使用有较高门槛，请以官方文档为准。