AIエージェントを付与するMCPサーバー Frama-C: EVA抽象解釈、WP導電 証拠、ACSLのアノテーションの注入および試すアノテーションのための隔離されたサンドボックス お問い合わせ

サーバは、人ではなく、エージェントによって運転されるように設計されています。 MCPとは クライアントはそれをスプーンし、stdio上でそれを話すので、人間のためのコマンドはありません タイプに。 反復ループの周りに構築されています。アノテーションを提案し、それを証明します。 目標が閉じていない理由を読んで、その後、修正します。 セッションの状態は、 1つのプロジェクトが渡るとどまるので貝の使用からではなくループ 呼び出し、サンドボックスは名前によってアドレスをとり、証拠のレシートは内部だけを比較します 実行します。

クロード コード、クロード デスクトップ、または任意の MCP クライアントにそれをワイヤーで縛って下さい、それからプロンプトで 日本語 English エージェントを接続する プロンプトパターン。 A check CI のサブコマンドが存在し、 手で実行する唯一の部分。

アーキテクチャ

サーバには2つの必須コンポーネントがあります。

• Rust MCPサーバー:MCP stdio上のツールを公開し、リクエストを変換する Frama-C のサーバプロトコル、および lazily は、Frama-C のメインプロセスを開始します。 最初のプロジェクト操作。
• [ast-utils Frama-C プラグイン: AST アクセスのカスタムリクエストを提供します,

frama-c-mcp

An MCP server that gives an AI agent Frama-C: EVA abstract interpretation, WP deductive proof, ACSL annotation injection, and isolated sandboxes for trying annotations out.

The server is designed to be driven by an agent rather than by a person. An MCP client spawns it and speaks to it over stdio, so there is no command for a human to type. It is built around an iterative loop: propose an annotation, prove it, read why the goal did not close, then revise. The session state follows from that loop rather than from shell use, since one project stays loaded across calls, sandboxes are addressed by name, and proof receipts compare only within a run.

Wire it into Claude Code, Claude Desktop, or any MCP client, then prompt in English. See Connect an agent and Prompt patterns. A check subcommand exists for CI and is the only part intended to be run by hand.

Architecture

┌──────────┐  MCP over stdio   ┌────────────────┐  Unix socket  ┌─────────────────┐
│ AI agent │◄─────────────────►│ frama-c-mcp    │◄─────────────►│ Frama-C main    │
└──────────┘                   │ Rust server    │               │ + ast-utils     │
                               └───────┬────────┘               └─────────────────┘
                                       │ Unix socket per sandbox
                                       ▼
                               ┌──────────────────┐
                               │ Frama-C sandbox  │
                               │ + ast-utils      │
                               │  per experiment  │
                               └──────────────────┘

The server has two required components:

• Rust MCP server: exposes the tools over MCP stdio, translates requests into Frama-C’s server protocol, and lazily starts the main Frama-C process on the first project operation.
• ast-utils Frama-C plugin: provides the custom requests for AST access, dependency extraction, ACSL injection, sandboxing, and WP configuration. Build and install it in the same opam switch as Frama-C.

create_sandbox extracts a function together with its type, callee, and global dependencies into a temporary C file, then starts a separate Frama-C process. An agent can iterate on annotations there without mutating the main project; verified sandbox annotations are merged back explicitly.

Session model

The server holds one project: reload_project or the first check loads it, and later calls operate on that AST. Sandboxes are separate processes, addressed as experiment_id:function.

The preprocessor surface is nostdinc, include_paths, isystem_paths, defines, force_includes, and machdep, applied in that order. Each value is written without its compiler flag. nostdinc drops the preprocessor’s default system directories and isystem_paths are searched after include_paths; pair