Designed to gate every PR and every merge.
One required check, rustproof, reports the conclusion computed by the rustproof CLI’s verdict command; the platform only relays it. One sticky comment will carry the patches, the spec diff and any counterexamples.
What the build engineer will do.
One check run per commit, with a section per affected crate
Will listen to pull_request, pull_request_review, merge_group and check_run. Annotations will point at the exact Rust line: counterexample inputs, weak specs, changed theorems.
One comment, updated in place
Its sections will come in a fixed order: patches, then the spec diff, then counterexamples, then coverage. Patches as before/after diffs, the spec diff in plain English and Lean, counterexamples with the failing input. Markdown only: tables, headings, glyphs, so it reads without color.
Proof-only commits as rustproof[bot]
Proof repairs are designed to be pushed to the PR branch by rustproof[bot]; spec and patch changes are proposed for a person to review, and the bot never pushes them.
Limited on purpose.
Every surface is designed to enforce the same table. Specs will live in their own directory under CODEOWNERS, so branch protection will enforce this, not policy.
| May do on its own | Proposes; a person merges | Never without a human |
|---|---|---|
| Write and repair proofs | Apply patches from the built-in brick library (visible, tested, reversible) | Change a theorem statement |
| Change extraction and build config, caches, and which functions to re-check | Apply a custom brick, or any patch an org has set to require approval | |
| Move the proof boundary, or weaken any guarantee |
The combined result will be verified before it lands.
Merge-queue commits are immutable, so repairs are designed to happen at PR time; the queue will only re-verify. By design, no failing, counterexample or stale obligation ever yields a green check, and that rule is among the first properties we plan to prove.
check_conclusion · a failing, counterexample or stale obligation never yields successcrates/rustproof-corePlannedBy design, CI never uses a person’s token; the integration will authenticate with its installation token.
Make the gate the engineer.
The GitHub App will install on the repositories that already run rustproof.