For years, humans have designed software (and hardware) in mostly the same way: write code, test and fix it as much as we want (or are allowed to by ambient constraints), ship it, build on top of it, and hope that we can patch anything later before it causes too much mayhem.
By this stage, we all know how critical to our lives computers are, how AI accelerates the aforementioned process, and how it makes producing software and exploiting vulnerabilities easier. More and more voices, including ours, are heralding the promises of AI-assisted formal verification – mathematically demonstrating that software correctly implements a precise specification (which hopefully captures our intentions) with a machine-checked proof – as the solution to the crisis that has beset us.
For the converted, the question is not what, but how.
