How Rainbow checks the algorithms behind business decisions
Rainbow checks proofs about decision algorithms with a small trusted kernel. It has kernel-checked theorems about all 222 algorithms in our catalogue, most of them on worked examples. It is for software where one wrong decision costs a lot of money.
Note added 15 October 2026: Rainbow’s v1.0.0 release documents this more exactly than the entry does. Each of the 222 algorithms has kernel-checked theorems about its decision step; for most, the theorems check worked instances, and 48 of the 415 proof modules prove a statement for all inputs. Classical guarantees are claimed only where a theorem states them. See doc/claims.md in the repository. The entry below stands as it was written.
Note added 16 October 2026: the trusted kernel has grown since this was written. At Rainbow v1.5.3 (2 November 2026) it is 1,706 lines in the same four files; the 1,200 below is v1.0.0’s. A release test still pins its length.
Most software is trusted because it passed its tests. For a decision that moves real money, which projects to accept, how to allocate constrained capacity, when to intervene, tests sample the input space. They do not close it. A proof does.
Rainbow is a data-oriented theorem prover written in Clojure. Its trusted base is a dependent-type kernel of roughly 1,200 lines. Everything else, search, tactics, the algorithm catalogue, sits outside that boundary and must produce a proof term the kernel independently checks. A highly optimised, untrusted engine proposes; a small trusted checker disposes.
What is proved today
Rainbow’s proving curriculum is the operations-research catalogue from the book
Applied Higher Order Functions and its companion library orhof. As of this
note, all 222 catalogued algorithms have machine-checked proofs across the
optimisation, decision-making and validation series. The prover checks signed
rationals, finite vectors, Bellman and value-iteration steps, and gradient methods
natively, and compiles truth tables into proof trees.
Why “proofs as data”
Rainbow treats terms, declarations, proofs, failures and provenance as immutable, content-addressed data. A proved reformulation becomes a reusable object, not a one-off transcript. That lets an expensive parametric proof be done once and a cheap certificate be checked per decision: the pattern that makes formal methods affordable in production rather than only in a paper.
What it is not
Rainbow has explicit, documented boundaries. It complements testing rather than replacing it, and it does not prove the properties listed under Limitations. We publish the covered set and the gap together, because the gap is the honest part of the result.
Rainbow’s core is open source under Apache-2.0: the kernel and the whole Level 1 to 3 corpus, at github.com/flexiana/rainbow.
Where this doesn't apply
The catalogue is complete at 222 of 222, but a complete catalogue is not a general guarantee. Rainbow still does not claim infinite-horizon or chaotic-relaxation asynchronous convergence, Bellman fixed-point uniqueness, terminating optimal-policy theorems, or, in the open core, a correspondence between the checked terms and running Clojure (that link is Rainbow Pro, at Level 5 and not yet Level 6). Those four remain unclaimed until separately proved. Numbers are reported with their stated scope.
What it means for a business
Where a decision rule is business-critical: an allocation that must never violate a capacity, or an optimiser whose output is audited: a machine-checked proof is stronger evidence than tests. This is a hypothesis about value, not a field-tested claim, until a client engagement measures it.
Cite this
Jiri Knesl (2026). How Rainbow checks the algorithms behind business decisions. Flexiana Research. https://flexiana.com/research/rainbow-kernel-proves-or-algorithms