Software that is proven, not promised.
We run a small software factory in South Shields. Specifications go in; SPARK-Ada comes out with every proof obligation discharged by machine, and the failures published alongside the passes. The numbers below are the factory's own state, not copy.
Counter history is public: every deploy appends a row to factory-timeline.jsonl. When we get something wrong, the correction is published in the open — including our own defects.
The model bench, this week
A fixed battery of SPARK specifications; a pass means compiled and mathematically proven, re-verified independently. No self-reporting.
| 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 |
Latest from the floor
The fourteen-pence run — two new models on the proof bench, one summit proof, and the one unanimous failure that turned out to be ours to own.
What we do
We convert legacy numerical code to provable SPARK-Ada, prove it, and publish the evidence — the per-routine results are open, including the obligations we haven't discharged yet. If your software has consequences when it is wrong, talk to us.