Your agent’s build engineer, inside its own loop.
CI reports a broken proof after the PR is opened. The plugin is designed to catch it earlier, in the agent’s own turn: it will bundle the CLI and move the CI rules into hooks that run while Claude works.
The floor and the ceiling.
Hooks are the floor: they are designed to work even where mods are turned off. The mod is the ceiling: rustproof’s own interface, drawn inside Claude Code.
| Component | Purpose |
|---|---|
bin/ | The CLI on the Bash tool’s PATH. A SessionStart hook will install the pinned platform binary. |
| Skills | /rustproof:login, /rustproof:init, plus make-provable (how to write Rust inside the subset, with bricks as idioms), port-python (how to port a Python span into the subset) and write-spec. |
.lsp.json | Lean’s language server, so proof diagnostics will reach Claude after every edit. |
| Settings hooks | Will re-scan after .rs edits and block spec edits and self-approval. The Stop hook is designed to block once when an edit leaves a previously proven function failing; stale functions are reported, not blocking. |
| Mod | Status band, proof pane, spec and patch review in the terminal, live progress, “more provable” nudges, coverage heat map, guards. |
.mcp.json | Will connect the remote rustproof MCP server (auth borrowed from the CLI) and lean-lsp-mcp. |
Provable from the first draft.
When Claude writes a function outside the subset, the mod is designed to name the brick that would apply, so the agent rewrites it the provable way and the build-time patch stays nearly empty.
One function, one turn
Claude writes a function → the PostToolUse hook re-scans → outside the subset? the mod names the brick, Claude rewrites → a spec is proposed → you approve it in the pane → the proof lands and the kernel checks it.
The Stop hook is designed to block once when an edit leaves a previously proven function failing; stale functions are reported, not blocking.
Claude can’t press a mod’s button
The mod is designed to refuse approvals coming from the shell, and the PreToolUse guard to refuse edits to .rustproof/specs/ and generated Lean, with instructions Claude can act on. Both are designed to fail closed.
By design, the PR’s CODEOWNERS review stays the final gate for specs.
To be drawn in the terminal and the Desktop app.
Monospace, box-drawing borders, status glyphs, hotkeys shown as 1: Obligations. Elsewhere the hooks will still run and the mod will fall back to plain transcript lines.
Status band
Will sit above the prompt, only when something needs attention or a run is active, for example ● 12 ◆ 1 needs review ✕ 1 counterexample ◌ searching 3/5 (illustrative). Digits will jump to the right tab.
Proof pane
/proofs will open it, even while Claude is working: Obligations, Needs you, Run, Coverage. You will approve a theorem without leaving the terminal.
Live progress
A spinner suffix, compact rows for rustproof tool calls instead of raw JSON, a one-line summary under each answer, toasts when a proof lands.
Three steps, inside Claude Code.
Install the Claude Code plugin coming soonNot published yet. It will bundle the CLI, hooks, Lean’s language server and the mod.
/rustproof:login coming soonBrowser sign-in (PKCE, loopback redirect), with sign-up in the same flow. One login is designed to cover Claude Code, hooks and the terminal.
/rustproof:init coming soonWill report, on an existing crate, coverage as-is, with patches, and what is excluded and why.
Prove the next function you write.
The plugin and the rustproof crate are not released yet. Early-access teams will get both before the marketplace listing.