You are correct that creating a program that verifies any other program is mathematically impossible. However, given some critical assumptions regarding the sco

You are correct that creating a program that verifies any other program is mathematically impossible. However, given some critical assumptions regarding the scope of the problem, we can use formal verification techniques to generate proofs for some programs. People in formal verification (https://en.m.wikipedia.org/wiki/Formal_verification https://en.m.wikipedia.org/wiki/Formal_verification) do research to find better ways of creating proofs for programs automatically.