A programme of Foundation-0
Proven Commons rewrites widely used software libraries in Lean and proves that the new code follows its written specification. It is a programme of Foundation-0, a non-profit organisation. It also trains future verifiers on live work: trainees learn by shipping real verified modules, with a mentor checking their work.
What a project ships
A finished project publishes the library, the specification, a proof a computer can check, and a test report that compares the new code against the original on millions of inputs.
New code in Lean, published as open source.
What the code must do, in writing, approved by a reviewer who did not write it.
A proof a computer can check, and one command anyone can run to re-check it.
The new code compared against the original, with the seed, the input count, and the results on record.
Projects
Each verified library gets a repo of its own in the Proven-Commons organisation, named for the software it verifies.
built, not yet verified
The tar extractor lives in its own repo, tar. Its goal is a proved rule that no file in an archive can be written outside the destination folder. Its proofs check, but the bar audit of 2026-10-24 found that the main theorem states less than that rule, that two statements under “What is not proved” on its project page are false, and that three of the six items of the first version of the bar are not yet fully met. The audit lists the fixes.
A policy engine in the style of AWS Cedar, a reader for the SQLite file format, and a parser for the Redis protocol with a small key-value store.
This is a plan: no wave starts without funding for its full run. From the founding brief: Wave 1, months 4 to 9. Three projects in parallel, one squad each:
Aims to
Prove that a satisfied forbid gives a deny, that no satisfied permit gives a deny, and that policy order does not change the decision.
Aims to
Parse the 100-byte header, the page header, and records. Prove the parser returns an error instead of reading outside the file, and that a record it reads stays inside its page.
Aims to
Prove that reading what the printer wrote gives the same command back, and that a get after a set returns the set value and a get after a delete returns nothing.
A Lean parser and printer for the Redis protocol with a small key-value store lives in its own repo, redis. It proves that parsing what the printer wrote gives the same value back, that the parser accepts nothing else, and that a get after a set or delete behaves as specified. Its differential tests against hiredis and redis-server are recorded in that repo. It is not yet verified: a reviewer who did not write its specification must approve it first.
This is a plan: no wave starts without funding for its full run. From the founding brief: Wave 1, months 4 to 9. Three projects in parallel, one squad each:
Aims to
Prove that a satisfied forbid gives a deny, that no satisfied permit gives a deny, and that policy order does not change the decision.
Aims to
Parse the 100-byte header, the page header, and records. Prove the parser returns an error instead of reading outside the file, and that a record it reads stays inside its page.
Aims to
Prove that reading what the printer wrote gives the same command back, and that a get after a set returns the set value and a get after a delete returns nothing.
Candidate list: CANDIDATES.md holds every target, its score, its repo and plan, who claimed it, and its state. It is updated as targets ship and new candidates are proposed.
Each project sends reusable lemmas to CSLib and Mathlib, the shared libraries for computer science and mathematics in Lean. The shared library grows. The next project starts cheaper.
The factory
Each project follows the same seven steps. The playbook is public. Each step has a named owner and a check.
Score it (see Target scoring). Freeze the original tests, the written specification or RFC, and sample files.
SPEC.md in plain words, and a Lean file that states each property as a theorem with sorry in place of the proof. State what inputs are valid, what errors are allowed, and what must always hold. Pair each safety property with one that a program doing nothing would fail, or say on the project page that usefulness rests on tests alone. A reviewer who did not write the specification must approve it, and the approval records a hash of what was approved.
Pure functions. Total functions that return an error instead of crashing. No pointer tricks carried over from C.
A failed proof is treated as a bug report against the code, the specification, or a missing lemma.
Run lake comparator --paranoid. Try to write a wrong program that still meets each statement. Run differential tests against the original library on random and mutated inputs. Record the seed, the input count, and the failures found. Write up what the attack found as a review record in this repo.
Offer the code to the upstream project in the form that project can use: a Lean replacement library, or a Lean model plus a production implementation kept in step by differential tests, as AWS does with Cedar. Publish a page that states what was proved, what was not proved, and what a reader must still trust (the Lean kernel, compiler, runtime, hardware, and any foreign function code).
The bar check runs in continuous integration on every change. A change that breaks a proof blocks a release until the proof is fixed. A change to the specification, or to the claims and limits on the page, voids the approval and blocks a release until a reviewer approves it.
The academy, as planned
People learn here by shipping. Lectures support the work. They do not replace it.
Lean basics, reading a proof, the codec pack: base64, hex, CRC-32, each with a round-trip proof.
Exit test One small proof, no sorry, checked by a mentor.
Works inside a live factory project. Owns one lemma or one parser function and its tests.
Exit test Code merged into a public project.
Owns a module: specification, code, proofs, differential tests, and the public page.
Exit test A module that passes the verified bar with a separate reviewer.
Writes and reviews specifications, runs a squad, teaches Level 1. This is the senior role the job market cannot supply. The academy is the only planned source of these people.
Funnel: public hack weekend (3 days, one small specification problem), then Level 0, then a paid Level 1 cohort, then Level 2 posts in the factory or placement with a sponsor who needs a verifier. Mentors: one senior verifier per 4 apprentices. No larger ratio.
Each graduate leaves with public proof of work: merged code, a proof a computer checked, and a page that states what they proved. That record is what an employer can check in minutes.
Read more
The full plan, in these parts: