It's wild to think the head of the Catholic Church understands the problems with AI better than the AI companies....

Decades ago, people tried to formally verify code. Essentially, you prove that the code is correct using math. It was an approach promoted by people like Dijkstra, who observed that “program testing can be used to show the presence of bugs, but never to show their absence” (1970). It did not work. It was too difficult. You can do it for a function, maybe a small piece of code… but for anything useful, it was just too much work, and the result was too weak. Classic examples include the seL4 microkernel, about 8,700 lines of C requiring ~200,000 lines of Isabelle proof and roughly 20 person-years of verification effort. But times are changing. So it appears that we can formally verify code these days. Or, at least, there is now a ton of startups and academic initiatives that say it is possible and maybe practical. Take your C code, have your AI prove that it is a correct implementation of the specification. Among other things, it would prove that the code is correct with respect to memory usage, but that’s the least of what it could do. The most obvious application is cryptography and anything that must be unbreakable. Have your AI prove that the system cannot be hacked. You should not get too excited. These will remain mathematical models. They have to make assumptions all over. But I am pretty excited about what this could enable. I'd love to have more formal analysis of my code. In fact, I have a few projects in mind right now, to formally verify heuristics that I have been using. Recent examples of startups: •&Truth (launched Oct 2026, ~$70M seed): Building a “universal verification machine” for any language. •Harmonic (Aristotle): Announced support (late Oct 2026) for formal verification of C software and Verilog hardware.

Decades ago, people tried to formally verify code. Essentially, you prove that the code is correct using math. It was an approach promoted by people like Dijkstra, who observed that “program testing can be used to show the presence of bugs, but never to show their absence” (1970). It did not work. It was too difficult. You can do it for a function, maybe a small piece of code… but for anything useful, it was just too much work, and the result was too weak. Classic examples include the seL4 microkernel, about 8,700 lines of C requiring ~200,000 lines of Isabelle proof and roughly 20 person-years of verification effort. But times are changing. So it appears that we can formally verify code these days. Or, at least, there is now a ton of startups and academic initiatives that say it is possible and maybe practical. Take your C code, have your AI prove that it is a correct implementation of the specification. Among other things, it would prove that the code is correct with respect to memory usage, but that’s the least of what it could do. The most obvious application is cryptography and anything that must be unbreakable. Have your AI prove that the system cannot be hacked. You should not get too excited. These will remain mathematical models. They have to make assumptions all over. But I am pretty excited about what this could enable. I'd love to have more formal analysis of my code. In fact, I have a few projects in mind right now, to formally verify heuristics that I have been using. Recent examples of startups: •&Truth (launched Oct 2026, ~$70M seed): Building a “universal verification machine” for any language. •Harmonic (Aristotle): Announced support (late Oct 2026) for formal verification of C software and Verilog hardware.