No they didn't. And proving correctness of software isn't the same as solving the halting problem. You're confusing formal verification and static analysis (that doesn't mean that the latter doesn't work). Please, google Curry-Howard Isomorphism and Rice's Theorem, will ya?