To give an example that goes beyond what you already suggested: You can prove that your code terminates (or rather responds to events in a finite time, even if

To give an example that goes beyond what you already suggested: You can prove that your code terminates (or rather responds to events in a finite time, even if the event loop itself runs forever.) Or you can even prove that your code reacts quickly, ie within some time limit. You can also prove memory limits. > The problem here is that the browser failed to correctly implement those rules. If the chromium team cannot do that, what makes you think they can implement any other kind of "benign code" verification with zero bugs? Defense in depth. And you can have competing implementations relatively easily for this, and another way to find and report bugs. Especially if the verifier is open source. The verifier itself can be pretty simple: it's the prover that's complicated and needs smarts, but that's being run on the author's computer, not in the user's browser.