I think this is a very relevant question and I am sad to see that it is being downvoted.

Remember that we have had two major flaws in the formally verified tls1.3 so far because the spec was not complete.