Proof that a rule is right for every input
A system that assigns staff to projects can pass all your tests and still, on an input you never tried, give someone too much work or break an exclusivity clause. Credit limits, exposure caps, eligibility checks and safety interlocks have the same problem. We prove the rule gives the right answer for every input, and a machine checks the proof. We use this where an error costs a lot of money, harms people's health, breaks the law or exposes private data.
What we agree with you first
We go through these questions with you before we prove anything.
-
Can we trust this rule for every input?
Tests check only the inputs someone thought of. A proof covers all of them.
-
Is a proof worth it here?
Yes, when the rule is exact, like a capacity that must never be exceeded or a limit that must always hold.
-
What exactly must be true?
A proof checks the rule as it is written down, so we write it down with you first.
-
What does a silent error cost you?
A proof is worth the most when a wrong answer that goes unnoticed costs you a lot of money.
A proof you can give to an auditor
A machine-checked proof shows the rule is right for every input, and a regulator or a business partner can check it themselves. We write the proof with Rainbow, our own prover.
For the owner
- A plain description of what is proved, and for which inputs.
- A certificate that a small, separate checker verifies a second time.
- Exact arithmetic, so a rounding error cannot break a limit that was proved.
For the technical reader
What we need to see
The code that makes the decision, the rule that must always be true, and the inputs it has to handle.
Where to start
Talk to Jiri or Ivo about the rule you need to trust. Talking to us costs nothing. If you want the scope in writing first, a short audit works out with you what must be true, for which inputs, and how we will prove it.
Questions about verification
What is Rainbow?
Our own prover, written in Clojure. The core is open source. Rainbow Pro is the paid part, and it generates certified, correct code from a specification.
Tell us about one rule
Tell Jiri or Ivo about the rule that must be right for every input. We will tell you how we would prove it.