Why a safety rulebook should be checked against every situation, not tested on a few

In one minute

• A safety rulebook decides what a machine does. Testing it on a handful of scenarios leaves most situations unchecked.
• quorum's compiler, cbc, tries every combination of readings the rulebook can see. For the pump rulebook that is 16,384 situations.
• It refuses a rulebook that gives two answers at once, no answer, an answer too slowly, or has an action it can never choose. It names the exact situation that breaks it.
• The number of situations doubles with each new reading. At the 30-reading limit that is about a billion, about two minutes on an 8-core PC.
• The full check proves the rules. It does not prove the plant. Someone still has to confirm the wiring on the real machine.

Who this is for

This guide is for the plant engineer or technician who writes or signs off the safety rules for a machine: a pump, a tank, a press. You do not need to be a programmer. The point is simple. If a set of rules decides when to stop a machine, you want to know it behaves correctly in every situation, not only the ones someone thought to try.

First, two words used throughout. A reading is one thing an instrument reports, true or false: vibration is high, suction pressure is low, the bearing is hot. A situation is one combination of those readings, all of them either present or absent at the same time.

Testing a few cases is not the same as checking them all

The usual way to gain confidence in a set of rules is to test it. You pick some scenarios, run them, and check the answers. A healthy machine. A machine with a hot bearing. A machine with low suction. If the answers look right, the rules go into service.

The problem is what you did not test. Each scenario you run is one situation out of many. The ones you did not pick are not checked at all. A rule that is wrong only when three readings happen together, and only when a fourth is absent, will sit quietly through every test that did not happen to line up those four readings. It waits for the plant to produce that combination. The plant has time.

This is not a failing of the people writing the tests. It is arithmetic. A rulebook with ten readings has over a thousand situations. Nobody writes a thousand test cases by hand, and if they did, the next reading would double the number.

How the count grows

Each reading is either present or absent. With one reading there are two situations. Add a second reading and each of those two splits in two, giving four. A third gives eight. The count doubles every time you add a reading. The general figure is 2 multiplied by itself once per reading, written 2^n for n readings.

This grows fast.

The pump rulebook in the quorum repository has 14 readings, which is 16,384 situations. The README states that the compiler solves all 16,384 of them, every build. At the top of the table, 16 situations, you could check by hand. At 14 readings you cannot. At 30 readings, the compiler's limit, there are about a billion situations.

A billion sounds impossible to check. It is not, because checking one situation is cheap and a computer does them in parallel. The README's "Honest limits" section gives measured times on an 8-core i9-9900K: 21 readings take 0.2 seconds, 24 readings 1.7 seconds, 27 readings 14 seconds, and 30 readings about two minutes. Two minutes is fine when you press a button and wait. It is too slow to repeat on every keystroke, which matters later.

What the compiler checks, and what it refuses

When you run cbc on a rulebook, it does not sample. It solves every situation and then asks the same questions of all of them. The README lists what it refuses: a situation that selects two actions at once, a situation that selects no action, an action that can never be chosen in any situation, and a situation whose decision takes longer than the proven time bound.

Here is the end of a real run on the pump rulebook, from cbc casebook/pump/pump.cb:

validation over all 16384 states
  Decided         16298    99.5%
  Indeterminate      86     0.5%
  Unsatisfied         0     0.0%
  Conflicted          0     0.0%
  Faulted             0     0.0%

  OK    no state selects two actions at once
  OK    every state selects an action
  OK    the solver completes in every state
  OK    work stays inside the 2n + 2m bound
  OK    every declared action is selected in at least one state

Each OK line is a promise about all 16,384 situations, not a sample of them. "No state selects two actions at once" means there is no situation, anywhere in the input space, where the pump is told to do two contradictory things. The 86 situations marked Indeterminate are not a failure. They are situations where the evidence is genuinely ambiguous, and the honest answer is to send a human to look. The rulebook says so on purpose.

A word on that time bound. "Work stays inside the 2n + 2m bound" means every decision finishes within a proven number of steps. On the pump the worst situation takes 140 steps against a bound of 248. That matters because a safety function has to answer on time, every time, not on average.

A refusal, with the exact situation that breaks it

The useful part is what happens when a rulebook has a gap. The compiler does not shrug. It names the situation. Here is a small rulebook written to show this. Two readings, two possible faults, two repairs, and a mistake: nothing says which repair wins when both faults are supported at once.

casebook two-answers v1
source "demo for the full-check article" dated 2026-10-25 by "guide"

observe hot   "bearing temperature high"
observe noise "unusual bearing noise"

claim wear      "bearing is wearing out" needs hot
claim looseness "mounting is loose"      needs noise

action run      idle
action lubricate      when wear
action tighten  safe  when looseness
prefer run over lubricate

Run cbc on it and the full check refuses it:

  FAIL  no state selects two actions at once  (1 states)
        'lubricate' and 'tighten' are BOTH selected when hot noise
        nothing orders them, so the framework cannot choose. Add `prefer lubricate over tighten`
        (or the reverse) to say which wins, or narrow one of their conditions so they
        cannot both hold.

validation failed for /tmp/conflict.cb; no output written

The message names the situation: hot noise, both readings present. It names the two actions that collide. It tells you how to fix it. And the last line matters most: no chip image is written. A rulebook that cannot decide one situation does not become a program a machine runs. Testing on a few cases might never have produced the hot noise situation. The full check produces all of them, so it cannot miss this one.

The 30-reading limit, and the quick check

There are two limits worth knowing. First, a rulebook can have at most 30 readings. The README explains why: the compiler tracks which readings are present using a 32-bit marker, and the full check doubles in time with each reading added. Thirty readings is about two minutes on a desktop. That is the ceiling.

Second, because two minutes is too slow to run on every edit, there is a quick check. The README describes cbc --symbolic, which checks the main properties of all situations at once in milliseconds, without walking them one by one. It is a fast way to catch a mistake while you are still typing. But the README is clear that the chip image still needs the full check. The quick check is for the keyboard; the full check is what earns the right to run on a machine.

What quorum does not do

The full check is powerful and narrow. It proves things about the rules. It proves nothing about the plant.

The README's "Honest limits" states this plainly: the check proves the rules, not the plant. Whether each reading actually comes from the right instrument, whether each threshold is set where the document says, and whether the controller passes each reading through to quorum are not things the full check can see. It is reasoning about a rulebook, not measuring a machine.

That is why quorum studio prints a commissioning sheet. A person walks the real machine, loop by loop, and confirms the wiring and the setpoints match the rulebook. The README notes that no plant has done this yet. The full check removes the guesswork from the logic. It does not remove the person from the loop. See the guide on commissioning for what that check covers.

One more honesty. quorum is source-available and designed with certification in mind, but the README states it is not certified for safety-critical use and does not yet run a working machine. Use it beside your existing protections, not instead of them.