quorumProof
Every claim names the test that shows it.
The project's safety case lists 118 claims, the test behind each, and what that test does not cover. A build fails if a claim names a test that does not exist, or if a test backs no claim.
How it is tested
Fifteen gates on every change
From the unit suites to the board firmware, on x86-64 and on a Raspberry Pi 5.
Every situation
The compiler solves the whole input space of every rulebook in the repository, on every build.
Real chips
The Pico 2 and Uno R4 decide every situation and print the line the host predicted. Damaged and tampered images are refused.
Proof certificates
The compiler can write a certificate of every state, which a separate small checker verifies on its own.
Checked documents
The figures in the README come from the tools, or are registered with the command that reproduces them.
Independent checks
Checked by code that shares nothing with quorum
A second solver
Most tests compare quorum's code with other code written for it, which proves consistency, not correctness. So the whole labelling is rebuilt with CaDiCaL, Armin Biere's SAT solver, and compared argument by argument.
| Rulebook | States | CaDiCaL calls | Mismatches |
|---|---|---|---|
| permit | 1,024 | 31,744 | 0 |
| vote | 512 | 26,624 | 0 |
| pump | 16,384 | 720,896 | 0 |
| tank | 32,768 | 1,474,560 | 0 |
| total | 50,688 | 2,253,824 | 0 |
A second implementation of the language
The solver check starts after the compiler has turned the rulebook into arguments, so it cannot see a mistake in that step. A second implementation, written from the documentation, reads the rulebook text directly and is compared with the compiler in every situation.
On its first run it found a real compiler bug, now fixed: a doubt could read a reading another doubt had already thrown out. After the fix, 3,000 random rulebooks and every rulebook in the repository agree.
Both implementations were written by the same developer, from documentation the same developer wrote. A shared misreading is less likely, not ruled out. Outside review is the missing step.
Measured on real chips
Footprint and worst-case time
The compiler gives a bound on the number of steps; on both boards the device took exactly the 140 steps it predicted for the pump's worst situation.
| Raspberry Pi Pico 2 (Cortex-M33, 150 MHz) | Arduino Uno R4 (Cortex-M4, 48 MHz) | |
|---|---|---|
| Solver, worst situation | 24.8 µs (bound 34.3 µs) | 75.2 µs |
| Full decision cycle, worst measured | 145.0 µs, cold cache | 284.3 µs |
| Steps, predicted and taken | 140 and 140 | 140 and 140 |
| Flash and RAM, engine with two rulebooks | 2,104 B and 2,657 B | 2,104 B and 2,657 B |
Against a 1 ms budget that is a margin of 3.5 to 6.9 times. It is a measurement, not a worst-case execution time analysis: the memory system has not been analysed statically.
Honest limits
What quorum has not done
- No plant runs it. Both example rulebooks were written by quorum's own developers, from documents whose outcomes were already known. The strongest missing evidence is an engineer outside BioDream writing a rulebook from their own worksheet, and the check finding a gap they did not know about.
- Not certified. quorum is not certified to IEC 61508, IEC 61511 or any other standard, and is not for safety-critical use.
- The check proves the rules, not the plant. Whether each reading comes from the right instrument is shown only by a person working through the commissioning sheet on the real machine, which no plant has done.
- 30 readings per rulebook. The full check doubles in time with each one: 30 readings take about two minutes on an 8-core PC.
- The timing of timed readings is tested, not proved. Rules can use time (how), and the full check still covers every combination of readings. When the board sets a timed reading is shown by tests against a second implementation and by runs on real boards, not by that check. A timed reading cannot be built on a conclusion, only on readings.
- AI drafts miss things. 86% of checks on unseen regulations, with misses that matter. A person approves every draft.