alt Hacker NewsWhere does this leave formal verification? Are we just shit-out-of-luck at this point? You can formally verify everything about an airplane's code, but if any of that is wrong, ChatGPT might decide that the best way to help you win the Nobel Prize is to take down the airplane your chief rival for the prize is currently in.
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.