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 ?
It is not clear to me from the article why QUIC Crypto was rejected. The slides mention that anti-replay didn't work, but was that just an implemention bug? Why was it rejected?
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.
https://dl.acm.org/citation.cfm?id=3284854
Pluggable encryption has been scoped out of QUIC v1, but will likely make a return soon after (and Noise seems one of the more likely candidates).