TLS 1.3 has been formally proven (not an implementation, but the standard itself). To the extent the mathematicians correctly explained what the TLS 1.3 RFC says, and correctly told the machine what TLS 1.3 is supposed to do, the machine proof says this protocol does what we intended.
That work assumes a bunch of components are black boxes, they must work. If we ever lose confidence that they work, we've got to throw those out. So for example SHA-256, AES GCM, X25519, the proof doesn't say "We prove these work" it says "Assuming you're right that these do what they're designed to do the rest of your proof holds"
Anyway, one of the assumptions in that proof is a surprise to a human implementing TLS 1.3, it isn't explicitly mentioned in the TLS 1.3 document as written. And so the result is, if you didn't obey that assumption, the proof doesn't hold and sure enough you're vulnerable to an attack.
The assumption is for Pre-shared Keys (e.g. IoT devices A and B don't want to bother with certificates, so they just use pre-agreed random keys) each device pairing has its own PSK.
A person looking at the design figures hey, got two devices Alice and Bob, I can just have a single key K known to both devices, and everything is secure. But that's wrong - and the TLS 1.3 proof doesn't say this will work. Here's what bad guys can do, it's called the Selfie Attack:
Alice sends a message to Bob, maybe "Did you feed the cat?" and it's encrypted with key K. Normally Bob receives the message, maybe answers "Yes I fed the cat" also encrypted with key K and all is well.
But now Mallory is on a network able to intercept and re-route messages. Alice sends to Bob, "Did you feed the cat?" encrypted with key K. Mallory can't read or tamper with this message, it's encrypted with key K and TLS 1.3 works as designed, but Mallory just re-directs the message back to Alice, "Did you feed the cat?". The message is encrypted with key K, Alice assumes Bob sent it, and replies "No, I didn't feed the cat" also encrypted with key K, which Mallory re-directs again back to Alice, who now mistakenly believes that Bob has told her he hasn't fed the cat.
There are obviously a bunch of things you could do to fix this. First of all you could just have more PSKs. If Alice's message to Bob is always encrypted using the Alice->Bob shared key, when Alice actually receives it instead she knows something is wrong immediately. Or you could just prefix each message with To/From information, like an old-fashioned email and that works too so long as you check it.
But the important observation is that this is an assumption in a proof that nobody really surfaced until it was too late. If researchers had told the proof system "No, the PSKs can be the same" the proof fails. Or if they'd carefully explained to the TLS Working Group, "We had to spell out that the PSKs must be different" then today RFC 8446 would likely explain that you need to do that or you've got a security problem. But neither happened and this attack slipped between the cracks.
1. a non-verified approach can have many problems in the (informal) specification + implementation errors
2. the verified approach is likely to have less specification errors (because the specification had to be formally written out and matched against an implementation) and implementation errors with respect to the specification will be almost impossible (minus faults in the compiler, OS and hardware).
There's a huge jump in security guarantees between 1 and 2.
My former professor (RIP) oversaw the formal verification of the F-16 computer software and it still had significant bugs in the end where the specification itself was incomplete or in error. And that was a multi-year, team-scale effort. No one is doing that for smart contracts.