If you look around, the problem touted here was that formal verification was done, but independently for two different parts of the standard, in isolation.

The layman answer that is formal verification should've been done on those systems after integration. I'm not sure how much that would've helped though, since the proofs for each of those was complex enough. And then actual code written tends to sway far away from what protocol implementers (also crypto folks) think it should look like.

So I'd say more formal verification, but also make it easier and accessible for normal developers without a Math PhD. And verification of actual code would be ideal.

Something I've come across recently is formal verification of cryptographic implementations not on paper (i.e. mathematically) but in plain C using tools and languages developed recently.

For example, a three part series on how SAW and Crytol were used to formally verify s2n (AWS's TLS lib):

https://galois.com/blog/2016/09/verifying-s2n-hmac-with-saw/

https://galois.com/blog/2016/09/specifying-hmac-in-cryptol/

https://galois.com/blog/2016/09/proving-program-equivalence-...

PS(A) for the adventurous: I've also come across a github repo that lists related stuff

https://github.com/enzet/symbolic-execution