C程序形式验证服务器

frama-c-mcp-server

An MCP server for Frama-C, enabling AI agents to perform C program formal verification — abstract interpretation (EVA), deductive proof (WP), ACSL annotation reasoning, and sandboxed CEGIS experimentation.

面向 Frama-C 的 MCP 服务器，让 AI 智能体能够执行 C 程序形式验证——抽象解释 (EVA)、演绎证明 (WP)、ACSL 注解推理，以及沙箱化的 CEGIS 迭代实验。

Architecture / 架构

AI Agent <── MCP (stdio) ──> Rust Server ──┬── Unix Socket ──> Frama-C (main)   ── EVA / WP / CIL
                              rmcp 1.x      │                   + ast-utils plugin
                              42 tools      │
                              session state └── Unix Socket ──> Frama-C (sandbox) ── isolated CEGIS
                                                                + ast-utils plugin

Two halves, both required / 两个必需的部分：

• Rust MCP server — bridges MCP (JSON-RPC over stdio, via rmcp) to the Frama-C server protocol (custom binary protocol over Unix socket, the same one Ivette uses). It lazily spawns Frama-C itself — you no longer start a Frama-C server by hand.

• ast-utils Frama-C plugin (OCaml, in ast-utils/) — registers the server requests the MCP relies on for AST access, dependency extraction, ACSL injection and WP config. Without this plugin most tools will fail, so it must be built and installed into the same opam switch as Frama-C.

• Rust MCP server — 桥接 MCP（stdio 上的 JSON-RPC，用 rmcp）与 Frama-C server 协议（Unix socket 上的自定义二进制协议，与 Ivette 相同）。它会惰性拉起 Frama-C——不再需要你手工启动 Frama-C server。

• ast-utils Frama-C 插件（OCaml，见 ast-utils/）——注册 MCP 依赖的 server request（AST 访问、依赖提取、ACSL 注入、WP 配置）。没有它，大部分工具会失败，因此必须构建并安装到与 Frama-C 相同的 opam switch。

Sandbox model / 沙箱模型

create_sandbox extracts a function with all its type/callee/global dependencies into a temporary self-contained C file and launches a separate Frama-C instance on it. The agent can then iterate ACSL annotations and run WP there without touching the main project; verified results are merged back explicitly.

create_sandbox 把一个函数连同它全部的类型/被调用者/全局依赖提取成一个独立的临时 C 文件，并在其上启动独立的 Frama-C 实例。智能体可在沙箱里反复迭代 ACSL 注解并跑 WP，不污染主工程；验证通过的结果再显式合并回去。

MCP Tools / MCP 工具（42）

Project & Source / 工程与源码

Analysis / 分析

WP / 演绎证明

Annotations / 注解

Sandbox / 沙箱

Navigation & Scheduling / 导航与调度

Verification State / 验证状态

Quick Start / 快速上手

Prerequisites / 前置条件

• Frama-C 31.0 (Gallium)
• OCaml >= 4.14.2 + opam + dune >= 3.0 — required to build the ast-utils plugin
• Rust (edition 2021)
• WP provers: alt-ergo (pulled in by Frama-C), and optionally z3 / cvc5

Build / 构建

# 1. Build + install the ast-utils Frama-C plugin (same opam switch as Frama-C)
#    构建并安装 ast-utils 插件（与 Frama-C 同一个 opam switch）
cd ast-utils
dune build && dune install
cd ..

# 2. Build the MCP server / 构建 MCP 服务器
cargo build --release

After changing the plugin, run dune clean && dune build && dune install — an incremental build may not relink the .cmxs, leaving the old plugin installed. 改动插件后请 dune clean && dune build && dune install——增量构建可能不重新链接 .cmxs，导致装的还是旧版。

Usage / 使用

The server spawns Frama-C itself on the first reload_project call. You only point it at the frama-c binary:

服务器在第一次 reload_project 时自行拉起 Frama-C。你只需告诉它 frama-c 二进制在哪：

./target/release/frama-c-mcp-server --frama-c /path/to/frama-c

MCP Configuration / MCP 配置

.mcp.json (project) or claude_desktop_config.json:

{
  "mcpServers": {
    "frama-c": {
      "command": "/path/to/frama-c-mcp-server",
      "args": ["--frama-c", "/path/to/frama-c"]
    }
  }
}

Verification Workflows / 验证工作流

Direct loop / 直接循环 — EVA finds problems, agent writes ACSL, WP proves:

reload_project → run_eva → get_eva_alarms → investigate_alarm
              → add_annotation_main / inject_all_annotations_main
              → run_wp_main → get_wp_goals   (repeat until all VALID)

Sandboxed CEGIS / 沙箱化 CEGIS — iterate without touching the main project:

create_sandbox → validate_acsl → inject_all_annotations_sandbox → run_wp_sandbox
              → get_wp_goals / get_vc_details   (counter-example guided retry)
              → extract_annotations → inject into main → run_wp_main
              → store_function_conclusion → delete_sandbox

Whole-program, bottom-up / 全程序自下而上 — verify callees before callers:

reload_project → get_callgraph → compute_topological_order
              → get_ready_functions → (verify each) → store_function_conclusion
              → repeat until every function has a conclusion

Testing / 测试

# Unit tests — no Frama-C needed / 单元测试，无需 Frama-C
cargo test --lib

# Integration + MCP stdio E2E — need frama-c + ast-utils installed on PATH
# 集成与 MCP stdio 端到端测试——需要 PATH 上有 frama-c 且已装 ast-utils
export PATH="$(opam var bin):$PATH"
cargo test --test integration_test -- --test-threads=1
cargo test --test mcp_stdio_test --release -- --test-threads=1

CI runs both lanes (.github/workflows/ci.yml): a fast Rust-only job, and a full job that installs Frama-C + provers + the ast-utils plugin.

CI 跑两条线（.github/workflows/ci.yml）：纯 Rust 快跑；以及安装 Frama-C + 证明器 + ast-utils 插件的完整集成。

Project Structure / 项目结构

src/
├── main.rs                 # CLI entry point (lazy spawn) / 入口（惰性拉起）
├── lib.rs                  # Library root / 库根
├── state.rs                # Session + conclusion + project state / 会话、结论、工程状态
├── topo.rs                 # Tarjan + Kahn topological order / 拓扑排序
├── error.rs                # Error types / 错误类型
├── frama_c/
│   ├── client.rs           # Frama-C client (GET/SET/EXEC/POLL)
│   ├── codec.rs            # Wire protocol codec / 协议编解码（S/L 长度前缀分帧）
│   └── transport.rs        # Unix socket transport / Unix Socket 传输层
└── mcp/
    ├── server.rs           # 43 MCP tool implementations / 43 个 MCP 工具实现
    ├── param_compat.rs     # Tool parameter compatibility / 参数兼容层
    └── types.rs            # Tool parameter types / 工具参数类型

ast-utils/                  # Frama-C plugin (OCaml) — REQUIRED / Frama-C 插件（OCaml），必需
├── src/                    # AST export, extraction, sandbox, ACSL injection, request registry
└── test/                   # Plugin regression tests / 插件回归测试

test/                       # C fixtures for integration tests / 集成测试用 C 文件
tests/                      # Rust integration tests / Rust 集成测试
docs/                       # Architecture and design notes / 架构与设计文档

Technical Notes / 技术要点

Frama-C Server Protocol / Frama-C 服务器协议: Custom binary protocol (not JSON-RPC). Commands: GET/SET/EXEC/POLL/SHUTDOWN. Framing: S+3 hex or L+7 hex length prefix. SET and EXEC are queued — must use a POLL loop. Same protocol Ivette (Frama-C's official GUI) uses. / 自定义二进制协议（非 JSON-RPC）。SET 和 EXEC 为队列式——需 POLL 轮询。与 Ivette（官方 GUI）使用相同协议。

AST Reload / AST 重载: File reparse requires setFiles([]) → setFiles(files) → compute. Direct setFiles(same_value) is a no-op due to Frama-C's state dependency system. This matches Ivette's reparseFiles() implementation. / 文件重新解析需要三步。直接 setFiles(同值) 是空操作。与 Ivette 的 reparseFiles() 一致。

Fetch APIs are incremental / fetch API 是增量的: fetchFunctions returns everything only on the first call, deltas afterwards. Call reloadFunctions first whenever you need a full snapshot. / fetchFunctions 只在首次返回全量，之后只返回变更；需要全量前先 reloadFunctions。

WP memory model / WP 内存模型: This server configures WP with Typed+nocast; casts make the corresponding VCs fail safely rather than being silently assumed away. / 本服务器把 WP 配为 Typed+nocast；存在 cast 时相关 VC 会安全失败，而非被静默放过。

Callee contracts / 被调用者契约: A bare declaration with no contract defaults to assigns \nothing, which is unsound (WP manual §2.1). Sandbox extraction therefore emits empty-body stubs for callees that lack an explicit assigns. / 无契约的裸声明默认 assigns \nothing，这是不可靠的；因此沙箱提取会为缺少显式 assigns 的被调用者生成空体 stub。

License

MIT — including the bundled ast-utils Frama-C plugin.