When we designed DCCP, I did a formal model using LTSA to prove liveness and safety properties. Mostly I did it for fun (I got landed with teaching concurrency, and the previous professor had used this tool). As formal models go, LTSA is rather simple. I was pretty surprised when it found a previously unknown deadlock state. To my chagrin, a decade or so earlier, I'd observed a very similar deadlock in the Solaris TCP stack when running SMTP, which is unusual in that it requires the server to send first.

I shared the LTSA model with a few others at the time, but no-one else seemed very interested in doing anything with it.

https://www.doc.ic.ac.uk/ltsa/

https://tools.ietf.org/html/rfc4340

Edit: I dug through my old backups, and I think this is probably the model I used:

http://nrg.cs.ucl.ac.uk/mjh/dccp.lts

It's nothing fancy, but my point is that even simple modelling can spot errors that a whole standards group of smart people miss.