Ashlee Vance explains how formal verification and theorem provers like Lean can mathematically prove software is unhackable, even against superintelligent AI. The approach uses AI-assisted synthesis to create code that's provably secure by mathematical impossibility rather than obscurity.
What if you wanted to prove that the software couldn't be hacked? Even if you had a super intelligent AI that was trying to hack your software, I have a mathematical proof now that the software cannot be hacked no matter how smart you are. It just can't be hacked in certain ways. It's mathematically impossible. Super intelligence can't get around a mathematical impossibility no matter how intelligent it is. So that's this idea of formally verifying software. So now we're thinking, okay, Lean, which we thought was just a pure math project in some sense, actually might be really important. What if we could formally verify and have defense-dominant cybersecurity? Things could not be hacked in the limit because if you can have AI to prove that the software can't be hacked or synthesize the software and prove that it can't be hacked, software becomes defense-dominant. So now we're thinking a lot about should we go into formal methods, formal verification of software rather than just thinking about this as math. That's because we're worried that obviously that when AI gets advanced, people are going to be hacking right and left and our societal infrastructure is going to be very vulnerable.
