I found this article about formal verification very helpful. There's parts that get quite technical, but I think the argument carries through even if you skim those parts.

So here's the point: AI is probably going to increase the speed and number of bugs or exploits that people find in software. This is very bad if you use software to interact with your irreversible money.

This is particularly important in the context of things like adopting new cryptographic signature schemes (which is pretty much the main solution proposed by everyone worried about quantum attacks). If Bitcoin introduces a new type of cryptography, we probably want to be pretty sure that there aren't any bugs in it.

Bugs in computer code become more scary when you put cryptocurrency into immutable onchain smart contracts from which North Korea can automatically drain all your money with no recourse if there's a bug in the code.

Bugs in computer code become even more scary when this all gets wrapped in zero-knowledge proofs, so if someone manages to hack the zero-knowledge proof system (#1480284), they can extract all the money, and we have no idea what went wrong - or worse, when something has gone wrong.

Luckily, the cryptography used by Bitcoin has been around for a good long while and there have been many people who were highly motivated to break it and so far this has not happened -- or we don't think it has happened. And what's really awesome is that even though it seems to be really difficult to break, it's relatively easy to implement.

The entire cypherpunk ethos is fundamentally based on the idea that on the internet, the defender has an advantage: it's much easier to build a digital "castle" (whether that means encryption, signatures or proofs) than to destroy one. If we lose that, then internet security can only come from economies of scale, from going all over the world to chase down possible attackers, and more generally from a binary choice between domination and doom.

But since most cryptography people interact with is implemented via computer programs and computer programs have bugs, and AI is very good at finding bugs, it starts to make people wish they had a way of making sure there weren't any bugs.

one answer that is very dear to me, is verifying correctness of computer programs, especially programs that are doing anything cryptographic or security-related. After all, a computer program is a mathematical object, and so proving that a computer program behaves in a certain way is a mathematical theorem.

Since a computer program is also a mathematical object, it might be possible (for some programs) to write a set of equations that demonstrate that the program does only what it we think it does and not anything else. This is my brutish definition of formal verification.

Formal verification, aided by AI, should be viewed not as totally new paradigm, but as a powerful accelerant of a trend and a paradigm that was already marching forward.

Formal verification is not a panacea. But it is particularly well-suited for situations where the goal is much simpler than the implementation.

However, this proving business isn't all flowers and teddy bears. While you might be able to prove that a program does a few things and only a few things, the question of how to scope the question is very tricky. And then you get people designing programs in order to be easy to prove, which might be a problem on its own.

The common pattern: designing cryptographic protocols around making them more "provable" often makes them less "natural", which makes it more likely that they break down in some situation that the designer did not even consider.

Formal verification is powerful. But regardless of the marketing that makes it sound like formal verification gives you "provable correctness", so-called "provable correctness" fundamentally does not prove that software (or hardware) is "correct".

I'm no math-head, so I'd be curious to hear from the cryptographers among us about the usefulness of formal verification.