From 05c3f7b33409a9ee887bf4646b6dae86e1b50d3d Mon Sep 17 00:00:00 2001 From: ahrazzle <38987266+ahrazzle@users.noreply.github.com> Date: Thu, 12 Nov 2026 06:59:34 -0600 Subject: [PATCH] link verified bar doc verified bar doc was not linked in readme --- profile/README.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/profile/README.md b/profile/README.md index fc6944b..d4e6afa 100644 --- a/profile/README.md +++ b/profile/README.md @@ -4,9 +4,11 @@ Proven Commons rewrites widely used software libraries in [Lean](https://lean-la A finished project publishes four things: 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. -[Website](https://proven-commons.github.io/mission/) · [Mission and founding brief](https://github.com/Proven-Commons/mission) · [Open issues and decisions](https://github.com/Proven-Commons/mission/issues) +[Website](https://proven-commons.github.io/mission/) · [Mission and founding brief](https://github.com/Proven-Commons/mission) · [Open issues and decisions](https://github.com/Proven-Commons/mission/issues) · [Verified Bar](https://github.com/Proven-Commons/mission/blob/main/playbook/verified-bar.md) ## The verified bar +Core operating framework for formally verified software: + A project may use the word verified in public only when all of these hold: @@ -17,6 +19,7 @@ A project may use the word verified in public only when all of these hold: - The public page lists what is outside the proof: runtime, compiler, hardware, and any unverified code. - A stranger can clone the repo, run one command, and re-check the proof. + ## Repos One repo per library, named for the software it verifies. Each carries its own proof check, releases, and page.