10 open-source artifacts built on one asymmetry: checking a proof is cheap and auditable, so the thing that produced it does not have to be trusted. The producer can be a solver, a model, or a stranger. The checker fits in an afternoon of reading.
The rule every one of these follows: when in doubt, refuse. Each tool has a
third verdict that is neither pass nor fail — UNVERIFIED,
OUT_OF_SCOPE, UNDECIDED — and it exists so that "I did not
establish this" never has to be rounded to "fine". A verifier that returns a confident answer
it has not earned is worse than no verifier, because it is believed.
New here? What it proves, and what it does not is the five-minute version. The tutorial takes one real bounds check end to end.
Python package
The certificate format, and a checker small enough to read.
Re-checks a proof of program admission using nothing but the standard library. No solver, no search, no floating point. It rebuilds every obligation from the specification and ignores whatever the certificate carries, so a certificate that proves an easy unrelated system cannot pass.
JavaScript package
The same checker again, written separately, in JavaScript.
Two implementations that share no code are worth more than one that has been read carefully. 246 differential vectors generated by the Python package are replayed here, and CI fails on any disagreement. Exact BigInt rationals, zero dependencies, runs in a browser.
Python package
How wrong is this guard? Exactly, or not at all.
Counts the states a guard admits that the safety property forbids, exactly where the region is small enough and by a bracketed estimate otherwise. It never reports a sampled estimate as a proof of zero, because sampling can bound a count and cannot establish its absence.
Python package / benchmark
A benchmark a false certification cannot survive.
The headline metric is a gate, not an average: a tool that ever calls an unsound guard sound fails, whatever else it scores. Abstention is free. Two splits, one synthetic and one derived from real historical CVE relations, and every answer comes from exhaustive enumeration.
pytest plugin
A test that has never failed is a claim, not a regression test.
Reintroduces the defect a test says it catches and asserts the test notices. A test that passes in both states is reported as not detecting the thing it exists to detect.
Python package / MCP server
Proof-gated code review for agents.
Five tools over MCP, OpenAI function calling, Anthropic tool use, or no framework at all. Three verdicts, and the third one is the point: OUT_OF_SCOPE means no verdict was reached, and every adapter is tested to make sure that sentence survives the conversion.
GitHub Action
The gate, as one line of workflow.
Checks certificates on a pull request and writes a SARIF alert when one is refused. Exit 3 -- the tool declining to certify -- fails the build, because in a gate that is not a softer refusal.
Hugging Face dataset
Six real vulnerability classes, with certificates that verify.
The relation each historical bounds check turned on, written as linear atoms, with a machine-checkable proof that the fixed guard implies safety. Every certificate re-verifies from the published data.
Hugging Face Space
Watch a forgery get refused, in your browser.
The real checker, compiled to nothing -- it runs under Pyodide on the page. Nothing you type is uploaded, which is the same argument the format makes.
Hugging Face Space
Score your tool without sending it anywhere.
The suites, the ground truth and the scorer run client-side. There is no server to upload a submission to, and that is deliberate: a scoring service you have to trust is what this whole toolkit argues you should not need.