A 1,200-line kernel that proves operations-research algorithms

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 is open source. The repository, examples and kernel are linked above.