Flexiana Decision Lab (Rainbow)
When testing is not enough: proving the decision logic
For a decision rule that must never violate a hard constraint — a capacity, a contractual limit, an exclusivity — tests sample the input space but cannot close it. The residual risk is exactly the case the tests did not draw.
The intervention
We built Rainbow, a Clojure-native dependent-type theorem prover with a 1,200-line trusted kernel, and used the operations-research algorithm catalogue as its proving curriculum — machine-checking algorithms rather than merely testing them.
Dependent types · Proof-carrying certificates · Content-addressed proof data
Result
All 222 catalogued OR algorithms carry machine-checked proofs — zero pending, zero refuted; the prover checks signed rationals, finite vectors, Bellman/value-iteration and gradient methods natively.
The covered set and the gap are published together. A proof covers what it covers — it complements testing rather than replacing it.
Formally proved
The problem with “it passed the tests”
A solver that allocates staff to projects can be green on every test and still, on an input no test drew, assign someone beyond their capacity or break an exclusivity clause. For most software that residual risk is acceptable. For a decision that moves money or carries contractual exposure, it is the whole risk.
The approach
Rainbow separates a small trusted kernel (about 1,200 lines) from everything else. An untrusted, optimised engine searches for a proof. The kernel independently checks the resulting term. This “proof-carrying” design scales far better than implementing a whole solver inside a prover, and it makes the trusted surface small enough to audit.
What is proved, and what is not
All 222 of 222 algorithms in the OR catalogue now have machine-checked proofs, with none pending and none refuted. Rainbow checks signed rationals, finite vectors, Bellman and value-iteration steps, and gradient methods natively, and turns truth tables into proof trees. It does not yet claim infinite-horizon or chaotic-relaxation asynchronous convergence, Bellman fixed-point uniqueness, terminating optimal-policy theorems, or a proved correspondence to the Clojure implementations. We publish the gap next to the result, because the gap is the honest part.
The commercial shape
The reusable pattern — prove a reformulation once, check a cheap certificate per decision — makes formal methods affordable in operation rather than only in a paper. Where a client’s decision logic is critical, this is the evidence that testing cannot provide.
