QUIC Crypto and simple state machines

Unfortunately I know nothing about Cryptography(Theoretical or Practical) but what benefits does QUIC bring to the table, also will it be subject to some form of formal verification ?

Not an implementation bug, a thinko. Adam Langley's strike register is supposed to prevent replays. In practice this, and other attempts in the same direction, all work fine for toy systems (e.g. one Apache no load balancer no failover) where you don't care but don't work for a real system. So the outcome was don't build any of them into TLS or QUIC and just warn implementors that Replay is a thing in 0RTT modes.

Unlike QUIC Crypto, TLS 1.3 is a product of a modern approach where you start by getting the mathematicians to prove the idea works, then you implement the idea. That article might give you almost the opposite impression, but not so.