Proven CommonsA public foundation for better software

A verified software factory & academy

Software the world
can build on.

The world runs on shared software. We’re here to make its foundations worthy of that trust.

We rewrite critical libraries in Lean, prove the code follows its specification, and train the people who will carry the work forward. In the open.

Explore the work Read our founding brief

A programme of Foundation-0, a non-profit organisation.

THE COMMON FOUNDATION
A foundation anyone can check Many software dependencies converge on a shared library, supported by a specification, a machine-checked proof, and public evidence. Shared software. PUBLICLY CHECKABLE. SPECIFICATION PROOF EVIDENCE
Trust, with the working shown.

Built in Lean 4.

Shared as open source.

Checked by anyone.

The verified standard
01 / PURPOSE & VISION

Better foundations.
More people to build them.

Our mission is to verify the small set of libraries that most software depends on, in the open, to a standard anyone can re-check.

And to train enough people that this work no longer depends on a small set of experts.

The future we’re working toward

Essential software with public, checkable evidence behind it. A growing community of verifiers. And a commons of reusable proofs that makes each new project easier than the last.

One programme. Two reinforcing parts.

The factory ships real verified modules. The academy turns that work into training. Graduates build the next modules, and reusable lemmas flow back to Mathlib and CSLib.

Build useful softwareTrain verifiersGrow the commons
02 / THE WORK

Start small.
Prove something that matters.

We choose useful, bounded slices of critical software: a clear specification, a real risk, and an upstream community to work with.

FIRST PILOT · BUILT, NOT YET VERIFIED · OCTOBER 2026

Keep an archive
inside its boundaries.

The tar pilot's goal is a proved rule for an in-memory ustar extraction model: no accepted path can escape the destination. Its proofs check, but the bar audit of 2026-10-24 found that the main theorem states less than that rule. The audit lists the fixes.

The boundary of the claim: it does not write extracted files to disk. Filesystem integration, races, the parser, checksums, and archive writer are outside the proved guarantee.

Explore the tar pilot Read the evidence
THE IDEA, IN PLAIN TERMS
destination/
docs/readme.txtaccepted
../../outside.txtrejected
/absolute/pathrejected

An illustration of the path rule, not a live proof checker.

Read the actual Lean proof

Next on the roadmap

Planned wave 1 · subject to funding

01 — ACCESS

Policy engine

Cedar-style decisions: a satisfied forbid means deny, no satisfied permit means deny, and policy order does not change the result.

02 — DATA

SQLite file reader

Bounded parsing of headers and records. Return an error instead of reading outside a file; keep records inside their page.

03 — PROTOCOLS · PROOFS DONE

Redis parser & store

Proved in Lean: parsing what the printer wrote gives the same value back, the parser accepts nothing else, and a get after a set or delete behaves as specified. Not yet verified: the specification awaits independent review.

See the work in progress

Targets are scored for harm, reach, specification size, a comparison implementation, a useful independent slice, and upstream engagement. See the selection criteria

03 / OUR PUBLIC STANDARD

“Verified” is a claim
you should be able to check.

A proof establishes that code follows a specification. The specification can still be wrong. Our standard combines independent review, machine checking, adversarial testing, and a clear account of what remains outside the proof.

Read the full verified bar
  1. 01

    A reviewed, pinned specification

    A reviewer on the org's list, who did not write it, approves what the code is meant to do. The approval records a hash, and any later change voids it.

  2. 02

    Every claim names its theorem

    The reviewer checks that each theorem says what the public claim says.

  3. 03

    One command re-checks the proofs

    lake comparator --paranoid checks that the proofs prove exactly the approved statements, with only the standard Lean axioms, under every kernel shipped with Lean.

  4. 04

    The code that runs is the code that was proved

    The programs people run call the proved functions. Project code uses no implemented_by, extern, unsafe, native evaluation, metaprogramming, axiom, or sorry outside the statements, unless the page lists the exception.

  5. 05

    Recorded differential tests

    Compare against the original implementation on random and mutated inputs. Commit the oracle, seed, input count, and results.

  6. 06

    Explicit trust boundaries

    List what remains unproved: the kernel, compiler, runtime, hardware, dependencies, and unverified code.

  7. 07

    Checked on every change

    The check runs in CI, the default branch requires it, and releases are tagged only from the default branch.

04 / INSIDE THE FACTORY

From a useful question
to a maintained proof.

Seven steps. A named owner and a check at each one. Shipping is the beginning of a maintenance commitment.

Agents propose.
The kernel checks.
A human owns the specification and the merge.

Read the factory plan
01 Pick the target

Score the candidate, talk to upstream maintainers, and freeze the original tests, public specification, and sample files.

02 Write the specification

Write the specification in plain words, and state each property as a Lean theorem with the proof left out. A reviewer who did not write it approves it, and the approval records a hash of what was approved.

03 Build for proof

Use pure, total functions in Lean. Invalid inputs return an error. Keep the implementation simple enough to reason about.

04 Prove the theorems

Prove the specification's theorems, under the same names, with the lemmas under them. Treat a failed proof as a bug report against the code, specification, or missing reasoning.

05 Attack the result

Run lake comparator --paranoid. Try to write a wrong program that still meets each statement. Run random and mutated inputs against the original implementation, and record the seed, the count, and what failed.

06 Ship with the evidence

Offer upstream a Lean library, or a Lean model and production implementation kept in step by differential tests. Publish proof limits and benchmarks.

07 Maintain the guarantee

The bar check runs in CI on every change. A broken proof blocks a release until it is fixed. A change to the specification or to the page's claims voids the approval until a reviewer approves it again.

05 / THE ACADEMY

Learn by shipping.
Leave with proof.

Lectures support the work. They don’t replace it. The academy model moves from a first checked proof to responsibility for a complete module.

  1. LEVEL 0 02 weeks

    Reader

    Learn Lean basics, read proofs, and work through a small codec proof.

    PROOF OF WORKOne small proof, checked by a mentor.
  2. LEVEL 1 08 weeks

    Apprentice

    Own one lemma or parser function and its tests inside a live factory project.

    PROOF OF WORKA contribution merged into a public project.
  3. LEVEL 2 06 months

    Verifier

    Own a module: specification, code, proofs, tests, and its public evidence page.

    PROOF OF WORKA module that passes independent review.
  4. LEVEL 3 Lead & teach

    Spec Lead & Mentor

    Write and review specifications, lead a squad, and train the next apprentices.

    THE NEXT GENERATIONMore people able to own the standard.

Public work is the credential. Merged code, a computer-checked proof, and a clear account of what it proves.

This is the planned programme structure. Cohort dates and applications have not been announced here. Follow the public conversation

06 / OBJECTIVES

Make the work measurable.

First-year targets from the founding brief.
Ambitions, not achievements or promises.

4

Projects through the verified bar

One pilot and three wave-1 projects.

40 / 12 / 4

Readers, Apprentices, Verifiers

A pipeline from first proof to module ownership.

10

Reusable upstream contributions

Lemmas or modules accepted into CSLib or Mathlib.

2+

Upstream bugs found & reported

With a fix or a test for maintainers.

We also aim to publish time and cost per project, and link every public “verified” claim to evidence anyone can re-check.

07 / HOW WE HOLD THE LINE

A commons, in practice.

Public benefit is the reason for the programme. The way we choose, fund, and review work has to reflect it.

Public work stays public.

Specifications, code, proofs, and test evidence for open libraries remain open. Useful lemmas and fixes go back upstream.

Priority isn’t approval.

Grants and donations support the public factory. Sponsors can move a library up the queue; they cannot buy the verified label.

Keep the scope honest.

Bounded modules, not entire systems at once. Lean 4, Mathlib, and CSLib, rather than a new prover. Clear limits on every claim.

The funding plan keeps paid training and private work a minority of total effort, with the split capped in the annual plan and reported. Read the funding principles

THE COMMONS GROWS WITH YOU

Help build what
everyone builds on.

Bring a library, a question, a proof, or support for the people doing the work. The conversation starts in the open.

Explore Proven Commons on GitHub
Learn or contributeIntroduce yourself and the work you’d like to do.Propose a libraryHelp identify a useful, well-specified target.Support the public factoryDiscuss grants, sponsorship, or mentor time.

These links open GitHub issue drafts. A GitHub account is needed to submit; issues are public.