For anyone that thought this doesn't feel comprehensive the Prior Work sections covers why -

"The WireGuard handshake protocol has undergone rigorous formal verification of desired properties using the Tamarin proof system [2]. Many of the cryptographic primitive implementations have also been formally verified as correct. The remaining implementations have been carefully fuzzed against the verified implementations to ensure correctness."

So all put together the simplicity goal really paid off for WireGuard.