The working, for anyone who wants to check it.
The front of this site is written for people who buy software. This page is for people who want to see the numbers, the method and the failures. Nothing here is a summary of the front page — it is the evidence underneath it.
The factory’s own state
state as of 2026-08-13These are counters, not claims. Every deploy appends a row to factory-timeline.jsonl, so the history is public and the numbers can be checked against their own past. When we get something wrong, the correction is published in the open — including our own defects.
What those words mean
- Proof obligation
- A single logical claim about the code — that a number can never go out of range, that an array is never read past its end, that a result matches what was specified. A program has thousands of them. Each is checked by machine, individually.
- Discharged
- Proved. A discharged obligation is one the prover has settled — not tested, not reviewed, but shown to hold for every possible input. The percentage above is honest: the obligations we have not discharged are counted and published rather than quietly dropped.
- SPARK
- A subset of the Ada programming language designed so that a machine can reason about it mathematically. It is used in aircraft, rail signalling and defence systems, and it is recognised by the certification authorities in those industries.
- Proof, versus testing
- A test runs the software on cases somebody thought of. A proof covers every case, including the ones nobody thought of. Testing can show that defects are present; only proof can show that a whole class of them is absent. Where we cannot prove something, we test it and label it as tested.
The model proof bench
A fixed battery of specifications is put to different language models. A pass means the code compiled and was mathematically proven, re-verified independently — not the model’s own report of how it did.
| claude-fable-5 | frontier API | 20/21 |
| kimi-k2.7-code | provider API · the whole run cost £0.14 | 19/21 |
| qwen3.6-27b | open weights, on-premises | 17/21 |
We run this bench to measure the gap between code a machine merely wrote and code a machine has proven. No model’s output reaches a customer without passing the proof gate first — the generator is never trusted; the gate decides.
The full table and its caveats · submit your model · per-routine results
Where the failures are
They are published beside the passes, on purpose. The results pages list the obligations still undischarged, and the field notes carry the runs that went wrong, including the ones that turned out to be our fault. A supplier who only publishes successes is telling you about their marketing, not their method.