The problem is scale. The program is the specification, but it is far too big to affordably prove arbitrary interesting properties about it. A program like Comp

The problem is scale. The program is the specification, but it is far too big to affordably prove arbitrary interesting properties about it. A program like CompCert is among the biggest programs verified end-to-end, and it is less than 1/5 of jQuery in size. Even then, it took world experts years. Plus, saying "zero bugs" is misleading. What you can get is proofs of your assertions about the program -- or a bunch of theorems. You know that those assertions are true.