Comment by 7e

I don't doubt your experience, but with X.509 having evolved substantially, and ASN.1 on billions (if not tens of billions) of devices, in practice it seems OK. And it was formally verified early.