I was talking with some friends about Cardano the other day and I brought up the fact that Ouroboros is formally verified. One of my friends asked me to explain what that means and why it's significant. I did my best but I realized I wasn't confident with my grasp of the concept. Here's how I explained it:
Formal verification has 2 aspects:
- the algorithm is described in a mathematical way explaining assumptions and outcomes (like the threat model). Proofs and lemmas are provided which provide a theoretical baseline for the algorithm's properties. Then this mathematical description is transcribed into a computer language specifically designed for proof evaluation to make sure the humans who wrote the proof didn't forget/miss anything.
- Once the theoretical model has been validated it needs to be implemented in code and this implementation leaves a lot of room for error. After the developers are finished implementing the protocol in their language of choice (in this case Haskell?) the implementation is run through another piece of software (something like static analysis) which somehow evaluates all possible code paths (in a general heuristic sense, maybe not literally) and compares those code paths with the computer model created in step 1.
If the implementation matches the theoretical model, then we can say the code is formally verified.
Is this explanation correct? How accurate is my explanation? What's missing? How can I improve it?
