Flexiana Decision Lab (Rainbow)
Proving the decision logic that testing can't reach
An allocation rule can pass every test and still break a capacity limit, a contract or an exclusivity clause on the one input no test tried.
What we did
We built Rainbow, a theorem prover in Clojure with a small trusted kernel, and put it to work on our catalogue of operations-research algorithms.
Dependent types · Proof certificates · Clojure
Result
Kernel-checked theorems about all 222 algorithms in our OR catalogue.
Formally proved
Say a solver assigns your staff to projects. It passes every test. Then it meets an input no test drew and books someone beyond capacity, or breaks an exclusivity clause. If that decision moves money or has contract risk, that one input can cost you a lot.
What Rainbow does
Rainbow proves the rule holds for every input. A fast engine finds the proof and a small kernel checks it. The kernel is the only part you have to trust, and it is short enough to audit. Rainbow Pro generates certified, correct code from the specification.
In production
You prove the model once. After that, each decision comes with a small certificate that is quick to check, so formal proof stays affordable in production.
