Originally posted by

**microcode**View PostIn principle sure you can sit there in the documentation masturbating about your algorithm and using a logic proof to say that the inputs and outputs are "correct" (not fast, not secure, not good, correct) and thus the function is proven... but do you know why nobody does that? Why "Mathematically Proven" in seL4's case and generally in software means "100% code coverage"? Because if your correct output is not fast, secure, or good then you have to change the code and rewrite the proof from scratch. If your proofs are instead in tests then it's much easier to modify them, because radical changes aren't required, and the "mathematical proof" is that all branches have been hit.

## Comment