alt Hacker News> AI is making formal verification go mainstream.
This nonsense again. No. No it isn’t.
I’m sure the people selling it wish it was, but that doesn’t make it true.
Replies
Ericson2314 • yesterday at 5:37 PM
Formal verification is going mainstream as watercooler weakend project fodder. As someone that has been well-versed in functional programming and depedent types for over a decade, this is a vast improvement.
The hobby project to day job methodology pipeline is real.
AnimalMuppet • yesterday at 2:08 PM
LLM-style AI isn't great for formal verification, not so far as I understand. And the recent advances in AI didn't do much for the kind of AI that is useful for formal verification.
➕ show 1 reply
whatisthishere • yesterday at 2:18 PM
[dead]
You haven't been paying attention.
The fact that we're reading about it here today and have read about it in the past weeks is one piece of evidence. Another is that we hadn't been reading about it in the past months before November. Opus 4.5 and GPT 5.2 have crossed an usefulness frontier.
Anecdotally, I've been having some success (guiding LLMs) writing Alloy models in the past month and ensuring conformance with code. Making these would've been unjustifiable from ROI perspective fairy tales just this summer. The landscape has changed qualitatively.