3 ms·

> 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 t

> 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.

AnimalMuppet 10mo ago
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.
- otterley 10mo ago
  You don’t use AI to perform formal verification. You give the agent access to verification tools whose output can then be fed back to the model. It’s the same design as giving LLMs the current time, since they can’t tell time themselves, either.
whatisthishere 10mo ago
[dead]
baq 10mo ago
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.
- Izkata 10mo ago
  > 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. Except I do remember reading about it on here many times in past years.
Ericson2314 10mo ago
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.

> 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.

AnimalMuppet 10mo ago

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.

otterley 10mo ago
You don’t use AI to perform formal verification. You give the agent access to verification tools whose output can then be fed back to the model. It’s the same design as giving LLMs the current time, since they can’t tell time themselves, either.

whatisthishere 10mo ago

[dead]

baq 10mo ago

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.

Izkata 10mo ago
> 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. Except I do remember reading about it on here many times in past years.

Ericson2314 10mo ago

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.