LibreSSL languishes on Linux

I don't think it's correct to say that "number of extension need to be kept in check". The concern was around the core primitives, you probably don't need eight different block ciphers whose main distinguishing feature is which major world power sponsored their development, you don't need to keep obsolete and arguably unsafe key exchange methods available just because it suits a few implementers, and so on. But the extensions have, if anything, multiplied.

The nice thing is that (within their assumptions†) the correctness proofs don't care about extensions. If you use certificate compression (forthcoming TLS 1.3 extension) or flags (likewise) or even Encrypted Client Hello (far more radical, but ultimately expressed as an extension) you keep all the behaviours that were proved, because the proof doesn't care.

† And there's a crack. For example the only known TLS 1.3 attack "Selfie" depends on an unstated assumption of the proof. The proof assumes PSKs are singular, if Alice and Bob each run both a TLS client and a server secured just by PSK, they actually need _two_ PSKs, the Alice->Bob key and the Bob->Alice key. But this assumption isn't spelled out. Lacking such explicit warning you might assume one Alice+Bob key will get the job done, then Mallory redirects Alice's call to Bob back to Alice, Alice's client assumes she's talking to Bob and mistakes her own answers for Bob's. Does that blow up your security? Alas RFC 8446 as written does not warn you that this would happen and what countermeasures you should use to avoid it.