We actually don’t know how to prove programs correct in any kind of large scale way. And in addition, and this is from my professor who specializes in formal methods for his entire career, proving a program correct does not prove a program right.