[simonw]

I think formal verification has never looked better.

The main reason formal verification has never really taken off is that it's difficult.

LLMs are significantly more familiar with Lean and Rocq and TLA+ than most software engineers.

I think the cost of trying to build systems that adopt formal verification may have just dropped low enough that companies will consider them when previously the ROI didn't look like it was there.

[msylvest]

I have had a lot of sympathy for this statement, LLMs could lower the bar to use of formal methods. But thinking it over in the context of BDD-driven development I am no longer really that sure. Compare two scenarios: A) from a specification an AI agent develops a usual piece of code along with a BDD-style testsuite passed and B) same AI also delivers a formal test (Lean/Rocq..) and successfully executes and passes it.

Will human judgment really consider scenario B) more credible than A) ? By so much that it is worth the effort ?

[gilbetron]

The first reason formal verification has never taken off is that it's difficult. The second reason, that most people don't get to because of the first reason, is that formal verification is really brittle. It is only verified under the very specific setup of the problem. Close doesn't count in math.

The first reason prevents humans from engaging with them, the second reason is what will make it difficult even for LLMs. I mean, I'm glad we are trying, but I'm dubious they will be the panacea some people proclaim.

[js8]

Close can count in math - fuzzy logic and probability are a thing.

But I think you have it backwards. Close doesn't count in IT security. "Almost secure" means unsecure. Security is the compelling argument for formal verification.