The frustrating thing is that we know how to write absolutely secure browsers (or other executors/renderers/etc. of untrusted data) using formal methods. Unfortunately, because most of the negative externality falls on users who don't know any better, the economics don't really work out.
You can prove a TLS implementation correct up to defined assumptions (e.g. clock consistency). There are already some projects working on this, eg https://project-everest.github.io/
Unlikely... these bugs are all logic bugs. They won't be mitigated by using formal methods, because most of these bugs adhere to pre-defined specs. The problem with browses is that these specs are often in conflict with each other for new and/or obscure features.
