Checking the checker: how a second implementation found a compiler bug

In one minute

• The compiler checks every rulebook. So who checks the compiler? Its own tests cannot, on their own.
• Tests written by the same team prove the code agrees with itself. That is consistency, not correctness.
• An independent solver, CaDiCaL, rebuilt every answer of four rulebooks: 2,253,824 checks, 0 mismatches.
• A second, plain reading of the language, written from the documents, found a real compiler bug on its first random run.
• The honest limit stays: the same developer wrote both the compiler and the second reading, from documents that developer wrote.

Who this is for

This guide is for anyone asking the fair question: the compiler promises it checked every situation, but why should I believe the compiler itself is right. The short answer is that one tool's word is never enough, so quorum has it checked by other tools that share none of its code. This guide explains those checks and, as importantly, what they still cannot see.

The compiler is the program that reads a rulebook and tries every combination of readings. The every-situation check is covered in its own guide. Here the subject is the compiler's own trustworthiness.

Why a team's own tests are not enough

A team writes a tool, then writes tests for it. The tests pass. That feels like proof, and it is weaker than it looks. If the same people write both the tool and the tests, they can share a misreading. If the author misunderstood a rule, the tool applies the wrong rule and the test checks for the wrong answer, and both agree. The test passes, because it was built from the same mistaken idea as the tool.

So agreement between a tool and its own tests proves consistency, not correctness. To get closer to correctness you need a second opinion that does not share the first one's assumptions.

The first independent check: CaDiCaL

The quorum repository calls this independent verification, and it has two independent checks. The first uses CaDiCaL, a well-known SAT solver written by Armin Biere. A SAT solver is a general tool for working out whether a set of logical conditions can all be true at once. CaDiCaL shares no code with quorum.

The trick that lets CaDiCaL rebuild quorum's answers rests on one fact from the theory. The grounded answer, the one the chip computes, is the intersection of all complete answers.

Because of that, CaDiCaL alone can reconstruct quorum's labelling from scratch. For each argument it asks CaDiCaL a question about complete answers, and the reply tells it whether the argument is in, out, or undecided. It never looks at how quorum computed its own answer. It builds its own, then compares, over four rulebooks, every argument in every state, not a sample:

Two and a quarter million checks, by a solver that shares no code with quorum, and not one disagreement. The check also carries a self-test: corrupt one label on purpose and the run must then fail, because a comparison that cannot fail is not a comparison.

What CaDiCaL cannot see

CaDiCaL checks the solver. It starts from the framework the compiler already built. That is its blind spot.

If the compiler read a rule wrongly, or turned the rule into the wrong arguments, CaDiCaL would check those wrong arguments perfectly and find no fault. The step it cannot see is the one from the rulebook text to the arguments. That is exactly the step a human is most likely to get wrong when writing the compiler.

The second independent check: a second reading of the language

To cover that step, quorum has a second implementation of the rulebook language. It is a tool called refcheck, about 300 lines of Python. The point is that it was written from the documentation, not from the compiler's source. It is a fresh reading of the same rules by the same documents a user would read.

It builds no framework and uses no gates. It evaluates the rules directly to a settled answer, then compares its decision with the compiler's in every state. It was run over:

• every rulebook in the repository;
• 3,000 random rulebooks, across six seeds, about 510,000 states, after the fix described below. That figure is from the quorum README.

To prove the second reading can actually catch a mistake, it carries six deliberate breaks, switched on by a setting. Each break makes it misread one rule: ignore severity, read "any" as "all", have a doubt read a discarded value, ignore a preference, and so on. Each of the six must be noticed, and all six are. A checker that cannot fail on a planted mistake is not a checker.

The bug it found

On its first random run, the second reading disagreed with the compiler. The disagreement was a real compiler bug, fixed on 2026-10-14.

The bug was in how a doubt reads its evidence. The documented rule is that a doubt reads its evidence raw, whatever else discards that reading. One place this matters is the consequent of an implies rule, a reading that one rule concludes and another doubt is meant to read raw. When one doubt discarded a reading that another doubt was meant to read raw, the compiler landed the discarding attack on the raw reading itself. So the second doubt saw the discarded value, against the documented rule. Worse, the answer depended on a detail of where a line was written in the source. On the reduced case, this meant the safe action was not chosen when it should have been.

The repository keeps the smallest rulebook that shows the bug, as a regression fixture. With three readings present, one doubt discards a reading, but the consistency doubt for the implies rule is meant to read that same reading raw. Done right, the reading counts, a claim holds, and the safe action is chosen. The compiler used to land the discard on the raw reading, so the safe action was passed over and an idle action was chosen instead.

The fix splits such a reading into a raw form and a usable form, and makes every discarding attack land on the usable form, however the source is written.

What the fix did not change

The fix is reassuring in a way that matters for anyone already running a board.

After the fix, 3,000 random rulebooks, about 510,000 states, showed zero differences between the compiler and the second reading. And no rulebook on a board changed. The pump and the tank compile to identical images, byte for byte. Two drafted fixtures each gained one internal argument and still decide all of their states exactly as before. The bug had been dormant in the shipped rulebooks and showed up only once a fresh reading went looking across random inputs.

What quorum does not claim

The checks are strong, and the limit is real.

• The same developer wrote both implementations, from documentation that the same developer wrote. A second reading from the same source makes a shared misreading less likely. It does not remove it, and it is not the same as review by someone outside the project.
• quorum has not had outside review. It is source-available, and anyone may read and re-run these checks, but it has not been assessed against a safety standard and no plant runs it.
• CaDiCaL and the certificate checker both start from the compiler's framework, so only the second reading covers the step from text to arguments. That step is now cross-checked, not proven correct.
• These are checks that can fail, not a proof of correctness. Their value is that they are independent and that they are shown to fail on planted mistakes. One of them found a real bug, which is the clearest evidence they are worth running.

To see what the every-situation check itself proves, read checking every situation. The full list of what is claimed and what each test does not cover is in the safety case.