[anon291]

Formal verification (i.e., automated theorem proving) relies on only admitting 'total' programs, which usually requires that any potential sources of 'bottom' (i.e., non-termination) come equipped with a proof that that never happens (usually based on well ordering of some structural decomposition in the recursion).

Thus, most theorem provers are not turing complete and explicitly ban any turing complete structures.

So, the various things they show and prove cannot be said to encompass all programs.