X账号：LLM让形式化验证转向规格审查

Idk who needs to hear this, but formal verification of software (mathematically checking that software is correct) is by no means done, even now that we have LLMs and the proof tedium is gone. Instead, having LLMs lets us focus on the spec, where humans remain in the loop, and where people were often sloppy in the past. By sloppy I mean they often touted “formally verified!!11”, without even mentioning the spec. And upon closer inspection, the spec often turned out to miss critical guarantees yo

u would naturally expect.

Formal verification IS hard. First, you need to figure out what behavior you even want to check: the spec. Then, you need to go through the tedium of writing a proof that your program indeed satisfies the spec.

LLMs massively speed up the second step. That’s because the proof can automatically be checked by a compiler. If the compiler is happy, the LLM did its job and you can trust the result, namely that your program satisfies the spec, without reading the proof yourself. (Ofc assuming you don't hit a compiler bug.)

But the first step is still there: What’s the spec? Writing the spec is still tedious and error-prone, and while LLMs help, a human needs to remain in the loop, at least to some extent, to assess whether the spec matches with the programmer's intention and the user's expectation. If you vibe that part, that’s where the bugs will creep back in.

Also: not all specs are equal. Don't trust "formally verified" without checking the spec. If the spec only says "the program doesn't crash", that is much less useful than a spec that reflects in detail the intended and expected functionality of the program.

So, humans are not leaving the loop, we're just moving up a level. With the proof tedium gone, we can finally focus our attention on the spec!