Browse
→ Code & Dev
→ frama-c-mcp
frama-c-mcp
Rust stdio MCP server that gives AI agents Frama-C formal-methods tools for C programs, including EVA abstract interpretation, WP deductive proof, ACSL annotation injection and isolated sandboxes for iterative proof repair. The server keeps project/session state across MCP calls so an agent can propose annotations, run proofs, inspect failed goals and revise without driving Frama-C directly from the shell. Public GitHub repository created August 19, 2026.
MCP unverified
Integration
| Transport | stdio |
| Auth | none |
| Endpoint | https://github.com/sysprog21/frama-c-mcp |
| Install | git clone https://github.com/sysprog21/frama-c-mcp && cd frama-c-mcp && cargo build --release |
Use Cases
| 01 | Let an assistant iterate on ACSL contracts and Frama-C proof failures through MCP tools |
| 02 | Run EVA abstract interpretation and WP deductive proofs without exposing a raw shell workflow to the agent |
| 03 | Keep proof receipts and sandboxed annotation experiments tied to the active project session |
Tags
formal-methods frama-c c static-analysis proof acsl rust stdio
Machine-readable: /api/servers.json
· JSON-LD schema embedded in <head>