user2236: 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?

user4023: According to Wikipedia a Formal Verification is:

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.

Thus, the principles on which the operation of the Ouroboros protocol is built have been mathematically proven, or formally verified. As we all know, Cardano is based on peer-reviewed academic research. You are absolutely right.
For details on Ouroboros, read this IOHK paper.

2236: <p>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:</p>
<hr />
<p>Formal verification has 2 aspects:</p>
<ol>
<li>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.</li>
<li>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.</li>
</ol>
<p>If the implementation matches the theoretical model, then we can say the code is formally verified.</p>
<hr />
<p>Is this explanation correct? How accurate is my explanation? What's missing? How can I improve it?</p>
 4023: <p>According to Wikipedia a <em><strong><a href="https://en.wikipedia.org/wiki/Formal_verification" rel="nofollow noreferrer">Formal Verification</a></strong></em> is:</p>
<blockquote>
<p>In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.</p>
</blockquote>
<p>Thus, the principles on which the operation of the Ouroboros protocol is built have been mathematically proven, or formally verified. As we all know, Cardano is based on peer-reviewed academic research. You are absolutely right.</p>
<p>For details on Ouroboros, read this <em><strong><a href="https://iohk.io/en/research/library/papers/ouroborosa-provably-secure-proof-of-stake-blockchain-protocol/" rel="nofollow noreferrer">IOHK paper</a></strong></em>.</p>
