| # bmc-agent for Claude Code |
|
|
| Verify C code for memory-safety (and overflow / reachability) bugs from inside a |
| Claude Code session, using CBMC-backed bounded model checking. Claude Code calls |
| the `bmc_verify` tool on the function/file you're working on, gets structured |
| findings (counterexamples, confidence, advisory triage), and helps you fix them. |
|
|
| ## What you get |
| - MCP tool **`bmc_verify(file, function, goal)`** — `goal`: `memsafety` (default, |
| low false-alarm), `overflow`, `reach`, or `all`. |
| - Slash command **`/verify`** — e.g. `/verify http.c parse_header`. |
| - Optional **auto-verify hook** — nudges a verify after Claude Code edits a `.c` file. |
|
|
| ## Requirements |
| 1. **CBMC** on PATH — `apt install cbmc` (Linux) or `brew install cbmc` (macOS). |
| 2. The **`claude` CLI logged in** — `claude /login`. bmc-agent runs its internal |
| spec-gen/triage LLM through your Claude **subscription** (no separate API key, |
| flat-rate). The MCP server strips `ANTHROPIC_API_KEY` from its child env so the |
| subscription is used, and pins a subscription-served model. |
| 3. Python deps: `pip install mcp`, and bmc-agent's own requirements. |
|
|
| ## Install |
| Add the plugin (or point Claude Code's MCP config at `bmc_mcp_server.py`). The |
| bundled `.mcp.json` registers the `bmc-agent` server; `BMC_AGENT_ROOT` points at |
| the bmc-agent checkout. |
|
|
| ## Notes |
| - Do **not** run the MCP server under a `ulimit -v` cap — the `claude` CLI (Node) |
| needs unbounded virtual memory. |
| - The solver verdict is ground truth; `triage` is advisory. `memsafety` does not |
| check integer overflow — use `goal=overflow`/`all` for that. |
| - Large files: raise `BMC_AGENT_VERIFY_TIMEOUT` (default 600s). |
|
|
