Maybe you haven't noticed but I actually wrote a theorem about a hypothetical verify_certificate() function in my previous comment. Maybe you also haven't noticed, but I didn't need a formal description of how certificate validation needs to be done to write that theorem.
And I assure you, if the implementation of verify_certificate() is anything except absolute garbage, it would be very easy to prove the theorem to be correct. I actually have some experience doing this, you know? I'm not just parroting something I read, I've proved code to be 100% correct multiple times using formal verification (i.e. theorem proving) tools. That is, according to certain basic and reasonable assumptions, of course, like e.g. the hardware is not faulty or buggy while running the code, and that the compiler itself is not buggy, which would be a lot more rare than a bug in my code -- and even then, note that compilers and CPUs can be (and have been) formally verified.
Maybe you don't agree with my approach but I think it's the most realistic one for a project such as this and I am absolutely confident it would be practical, would completely eliminate most (i.e. more than 50%, at least) existing bugs with minimal verification effort (which almost anyone would be capable of doing with minimal training), and would steadily become more and more bug-free with additional, incremental verification (i.e. theorem proving) and refactoring effort.