No escape hatches. Limited authority. Your identity in your keychain.
rustproof is designed so that every guarantee it makes is enforced by the Lean kernel, by branch protection, or by a hook that fails closed. None will rest on policy alone.
What “proven” means here.
Proven against the tree that shipped
The build will record the hash of the patched tree; proofs will be keyed to that hash; release artifacts will be stamped with it. “Proven” always means “proven against the tree this was built from.”
No escape hatches
The build is designed to fail on sorry, on any axiom outside the approved set (checked with #print axioms), and on any proof that relies on unchecked evaluation.
Specs must have teeth
rustproof will mutate the patched Rust and re-check. A spec that still holds for a mutant will be flagged as weak.
The runtime matches the model
Overflow checks are designed to stay on in the patched build, so the running code fails exactly where the model says it fails, inside and outside every precondition.
Specs will live under CODEOWNERS.
The build engineer is designed to write and repair proofs and change caches and config; patches from the built-in brick library are proposed for a person to merge. It may never change a theorem, apply a custom brick, or move the proof boundary. Branch protection will enforce this; agents will be refused by hooks that fail closed.
The CLI will own identity.
One login
The CLI’s login will run browser sign-in (PKCE, loopback redirect) and store the token in the OS keychain. One login is designed to cover Claude Code, hooks and the terminal.
MCP will borrow it
The plugin’s remote MCP entry will ask the CLI for a bearer token and rerun it on a 401, so refresh will live in one place. The server is designed to also speak standard MCP OAuth for other clients.
CI never uses your token
By design, the GitHub integration will authenticate with its installation token.
Where your code will go.
In v1
Finding a proof is expensive, so v1 will run extraction, search and checking on rustproof cloud. Your code and proofs will be processed there for speed, keyed by content hash, and cached as build artifacts.
Later: self-hosted runners
For banks and other sensitive customers: runners on your own machines that will pull jobs from the API and send back only results, with proof search on your own hardware. Leanstral has open weights, so the prover can run where the code is.
Processors
- Railway (hosting) hosts this website.
- GitHub (repository access) will give the GitHub App access to the repositories you connect.
- WorkOS (sign-in) will handle sign-in to the dashboard.
- Mistral (proof search) will receive generated Lean goals and context.
- Anthropic (spec proposals) will draft spec proposals from your code, for a person to review.
- Twilio (contact form) delivers the messages sent through the contact form, and the confirmation email.
Retention terms will be published before early access.
Questions about a review?
We will walk your security team through the boundary and the authority model.