The work of turning a technical document into something automated provers can work on is often revealing when it comes to logical flaws which is itself a valuable product.
However, even when this appears to be successful and the proof tool verifies your design has the properties you wanted, there can be hidden assumptions in the proof which do not match the human understanding of the technical document.
TLS 1.3 was proved this way before the RFC was signed off. We know TLS 1.3 does what it says on the tin, assuming the constituent elements work as specified (e.g. AES is a working block cipher, SHA256 is a working cryptographic hash function, Elliptic Curve Diffie Hellman is a working key agreement protocol). However, it turns out they proved something slightly different from what humans would have understood from the document.
The result is the Selfie attack. NB This applies specifically to Pre-shared Key authentication, stuff like your web browser isn't affected. Here's how it goes: Alice and Bob are using a PSK to communicate securely, but their Cat would like to manipulate them. Based on their understanding of the pre-errata RFC document, Alice and Bob agreed a single Pre-shared Key, let's call that ABA, which the Cat doesn't know, and they use TLS 1.3.
0. Bob feeds the cat before leaving for work
1. Alice wakes up, notices the Cat's food bowl is empty and sends an encrypted message to Bob, Encrypt(ABA, "Did you feed the cat?")
2. The Cat intercepts Alice's encrypted message and sends it back to her. The Cat can't read the message, nor tamper with it, but just sends it unaltered and trusts that will have the desired effect.
3. Alice receives an authentic message encrypted with the ABA key, which she presumes is from Bob, it says "Did you feed the cat?"
4. Alice sends an encrypted reply, Encrypt(ABA, "No")
5. The Cat intercepts this message too and sends it back to Alice again
6. Alice receives the reply, which she presumes is from Bob, it says "No".
7. Alice feeds the cat again. The cat has now been fed twice. Attack successful.
How did this attack sneak part the proof? Well, the proof says Alice and Bob should agree two keys, an Alice->Bob key (let's calls this AB1) and a Bob->Alice keys (call it BA1). When Alice receives her own message encrypted with AB1, she can see she sent it, not Bob, and so she detects the Cat's attack. So the proof is fine.
The person writing the proof assumed this is what was meant in the human readable document describing TLS 1.3, but the other humans working from this document assumed it would be fine for Alice and Bob to agree a single key ABA. It's certainly not highlighted in the original document that this is a concern and you must agree two keys.
[ There are also lots of other things you could do, if you're careful and know about this attack, but for some reason can't just agree twice as many keys. However the correct basic design to explain in the document is to just make separate keys for each direction ]
That's why you need to prove the whole chain end to end. From spec to C code. Hand-translating a proof to working C code will most likely introduce bugs. There are now proof tools that can prove the complete chain from spec to machine code (!)
However, even when this appears to be successful and the proof tool verifies your design has the properties you wanted, there can be hidden assumptions in the proof which do not match the human understanding of the technical document.
TLS 1.3 was proved this way before the RFC was signed off. We know TLS 1.3 does what it says on the tin, assuming the constituent elements work as specified (e.g. AES is a working block cipher, SHA256 is a working cryptographic hash function, Elliptic Curve Diffie Hellman is a working key agreement protocol). However, it turns out they proved something slightly different from what humans would have understood from the document.
The result is the Selfie attack. NB This applies specifically to Pre-shared Key authentication, stuff like your web browser isn't affected. Here's how it goes: Alice and Bob are using a PSK to communicate securely, but their Cat would like to manipulate them. Based on their understanding of the pre-errata RFC document, Alice and Bob agreed a single Pre-shared Key, let's call that ABA, which the Cat doesn't know, and they use TLS 1.3.
0. Bob feeds the cat before leaving for work
1. Alice wakes up, notices the Cat's food bowl is empty and sends an encrypted message to Bob, Encrypt(ABA, "Did you feed the cat?")
2. The Cat intercepts Alice's encrypted message and sends it back to her. The Cat can't read the message, nor tamper with it, but just sends it unaltered and trusts that will have the desired effect.
3. Alice receives an authentic message encrypted with the ABA key, which she presumes is from Bob, it says "Did you feed the cat?"
4. Alice sends an encrypted reply, Encrypt(ABA, "No")
5. The Cat intercepts this message too and sends it back to Alice again
6. Alice receives the reply, which she presumes is from Bob, it says "No".
7. Alice feeds the cat again. The cat has now been fed twice. Attack successful.
How did this attack sneak part the proof? Well, the proof says Alice and Bob should agree two keys, an Alice->Bob key (let's calls this AB1) and a Bob->Alice keys (call it BA1). When Alice receives her own message encrypted with AB1, she can see she sent it, not Bob, and so she detects the Cat's attack. So the proof is fine.
The person writing the proof assumed this is what was meant in the human readable document describing TLS 1.3, but the other humans working from this document assumed it would be fine for Alice and Bob to agree a single key ABA. It's certainly not highlighted in the original document that this is a concern and you must agree two keys.
[ There are also lots of other things you could do, if you're careful and know about this attack, but for some reason can't just agree twice as many keys. However the correct basic design to explain in the document is to just make separate keys for each direction ]