You can’t. The headline is missing a piece of context in that the proved it was free of runtime errors… according to a specification they chose to evaluate it a

You can’t. The headline is missing a piece of context in that the proved it was free of runtime errors… according to a specification they chose to evaluate it against. What if their specification contained an error? You could verify that specification against another specification, you could even do that formally if you want to. Eventually you have to confront Gödel’s incompleteness theorem, and accept that such a level of proof is not possible. Formal verification btw is just a formalised methodology for evaluating something against a specification. It doesn’t prove that errors don’t exist, or that the verifier hasn’t managed to independently make their own error. It’s just a rigorous PR.