Checking is cheap and local. Finding is expensive and remote.
Checking a proof is deterministic and fast: the Lean kernel plus Lake’s build cache. It runs on your laptop and will run in hooks. Finding a proof is expensive and runs remotely, so search and repair will run here, many attempts in parallel.
One proof API, designed for every surface.
It will also be exposed as a remote MCP server, so the same endpoint will work in Claude Code, as a claude.ai connector, and in other MCP clients.
Check
The Lean kernel with a content-addressed cache of build artifacts. Reruns will skip finished work.
Search and repair
Leanstral, through Mistral’s hosted API in v1, is designed to run as an agent against the obligation’s Lean project with the kernel as the judge. Many attempts will run in parallel; bricks will ship proof templates so search starts from a skeleton. Self-hosting the open weights is planned for later.
Counterexamples
Property-based search and fuzzing will run against the patched Rust. “fib(94) overflows u64” is a bug report. “Proof failed” is not.
Mutation
Mutants of the patched Rust will be re-checked. A spec that still holds for a mutant will be flagged as a weak spec.
Durable workflows
DBOS on Postgres. A crashed worker will resume from its last completed step.
Fan-out with limits
Queues will cap concurrent proof searches. Every external side effect is designed to be idempotent, so retries are safe.
Three front doors, one API, one CLI everywhere.
The architecture as it is designed.
The same binary, every runner.
Every step (scan, rank, patch, extract, propose, prove, check, mutate, counterexample, build, test, report) is designed to be idempotent and keyed by content hash. Workers will call the open-source CLI, so there is one implementation of every primitive. Nobody will need Postgres to use rustproof.
| Where | What runs | Engine |
|---|---|---|
| Laptop and Claude Code | rustproof CLI | Content-addressed step cache |
| rustproof cloud | Python workers calling rustproof step … | DBOS Transact, workflow state in the same Postgres as the platform’s data |
| Self-hosted runner (later) | The same worker image on your machines, pulling jobs from the API | DBOS on your Postgres |
| Cloud API | FastAPI | Nothing; it is designed to enqueue workflows through the DBOS client. |