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.