Comment by mike_hearn

This is the fantasy that has always driven proof systems research. Nobody is going to run software that has never been tested. Would ride a rollercoaster that had never actually been tested before, only "proven" safe? I wouldn't!

So this stuff is always going to be additive and concerned with edge cases, as almost by definition, stuff that isn't edge cases will be found by comprehensive enough testing procedures.

And yet most software doesn't really need to be correct under edge cases, outside of security and data loss issues. People can tolerate a lot of incorrectness in other areas because it's just annoying, not critical.

Security is a case where formal methods could help, but I don't think LLMs will change the industries lack of interest. If anything it'll reduce it even further. Historically security took place in a fog of war. You don't know your enemies capabilities and may not be able to easily match them. But now LLMs are better at finding security bugs than most (all?) humans and ~everyone has access to them, so, from a liability perspective, all you have to do is point a frontier LLM at your codebase and let it fix as many bugs as it can find. Your enemies don't have access to anything better, so once it's done you can tick the box and say security is good enough. Meaning, nobody will fire you if there are still attacks possible.

So in the end I don't see LLMs changing the adoption formal methods.