There are ways to prove the program will reach certain outputs within a certain envelope of inputs under a certain set of constraints. This in itself is rather

There are ways to prove the program will reach certain outputs within a certain envelope of inputs under a certain set of constraints. This in itself is rather limited. For example, a formal prover would know nothing about something like rowhammer, and would happily accept code that seems to work as intended but also executes a rowhammer attack on the side which completely changes the output. Ignoring that, this definition of correct is entirely divorced from the level where requirements exist, which is as envisioned. An error in requirements or an error in design can still very well yield formally 'correct' code. There's no way around this today, and there's a pretty strong argument that this is an inherent problem to which no solution exists. This is precisely why NASA has lost missions despite being one of the most prolific users of formal provers. They proved the code works as designed, but that says nothing of the design being correct, which says nothing of the intent of the design being correct. Also see: https://en.wikipedia.org/wiki/Instrumental_convergence#Paperclip_maximizer https://en.wikipedia.org/wiki/Instrumental_convergence#Paper...