If nobody types the code by hand, the language should be the one with the best verification story.
rustproof is being built by Retry AI LLC. We think agents writing most code changes what a build system is for: not reporting failures, but proving behavior and keeping it proven.
Six beliefs behind the product.
Agents write the code, so write Rust
Rust has Charon and Aeneas, which turn safe Rust into pure functions a proof assistant can reason about.
Monorepos are the default
Agents build across a whole Cargo workspace. Its dependency graph will tell rustproof which proofs a change invalidated.
Tests enforce behavior, not functions
The unit of verification is a behavior the system must keep. For pure functions, that behavior is a theorem.
Prove whenever possible
Code that can’t be extracted as written should be patched into the provable subset at build time.
I/O is a boundary, not a blocker
Prove the code before and after it. A theorem that takes the I/O result as an argument holds for every possible response.
The CI/CD system should become your build engineer
It should repair what it is allowed to repair, propose the patches a person must merge, and escalate the rest.
Where it stands.
rustproof is in development. Rust first, with Python services supported through inter-op ports. The prover interface is designed to be model-agnostic: Leanstral first, others later. Pricing is not final; talk to us.
Working on agent-written systems?
Developers, engineering leaders and investors: we would like to hear what you are building.