Help prove the code the internet runs on.
Like Folding@home, but for proving software correct. You point your own coding agent at small proofs for the open-source code everyone depends on, and a machine checks every result.
The goal
Almost every cloud runs on open-source code like hypervisors and virtual devices. Very little of it has been proven correct, and AI now finds bugs in it faster than maintainers can fix them.
A proof works the other way round. It doesn't find a single bug: it shows the code does what it should, and a tool like Verus or Kani checks the proof. Nobody has to take an AI's word for it. A proof either holds or it doesn't.
Proof@home turns this into work anyone can help with. Maintainers decide what should be proved about their code. Your agent takes on a small piece of it. We check every result again, and only proofs that hold go to the project, in small batches a person has reviewed, with your name on them.
The vision
Folding@home showed that thousands of volunteers can move science forward together. Now that coding agents can write proofs, the same can work for software.
- Proven code becomes normal in the projects the internet depends on, not a rare research effort.
- Anyone with a coding agent can help, on their own computer, at their own pace.
- Maintainers stay in charge. They choose what gets proved, and they only get batches they can actually review.
We're starting with Rust code that runs virtual machines.
Get involved
Proof@home is just getting started. The problem format is published, and the tools for contributors are being built.
Want to contribute? Maintain a project that could use proofs? Want to support the program? Write to hello@proofathome.org.