Specs (and proof checkers) can have bugs too! [LWN.net]

Specs (and proof checkers) can have bugs too!

Posted Apr 25, 2026 2:17 UTC (Sat) by DemiMarie (subscriber, #164188)
In reply to: What about the price? by cypherpunks2
Parent article: Firefox: The zero-days are numbered

Formal verification checks that your code meets your spec. It doesn’t check that your spec matches your intent.

Also, proof checkers can have bugs too, including ones allowing false proofs.

to post comments

Specs (and proof checkers) can have bugs too!

Posted Apr 26, 2026 4:52 UTC (Sun) by cypherpunks2 (guest, #152408) [Link] (1 responses)

> Formal verification checks that your code meets your spec. It doesn’t check that your spec matches your intent.

That's true, but those kinds of mistakes wouldn't be considered a software bug than an LLM would find anyway.

Specs (and proof checkers) can have bugs too!

Posted Apr 27, 2026 9:17 UTC (Mon) by farnz (subscriber, #17727) [Link]

The thing that makes LLM-based security analysers interesting is that they're good at finding what amount to "bugs in the specification", where it's implausible that the human intended something that they wrote.

This is in contrast to formal verification, where an error in the spec results in verification passing, but the software not functioning as intended. An LLM looking at your code will do the equivalent of "there's no plausible sequence of tokens that would represent a specification for this code that a human would write", where a formal verifier does not look to see if the specification is plausibly human written.

Specs (and proof checkers) can have bugs too!

Posted Apr 26, 2026 10:33 UTC (Sun) by jch (guest, #51929) [Link]

> Also, proof checkers can have bugs too, including ones allowing false proofs.

I'm not a specialist, but from what I've gathered, at least Rocq is able to produce a proof in a core language (the logic with no syntactic sugar). There is then a second program, the proof verifier, that checks the proof. The verifier is as simple as possible and has been written independently of the proof assistant, so it's fairly improbable that both the proof assistant and the verifier have the same bug.

Again, this is just what I've gathered from conversations with specialists, but as far as I know most bugs turn out to be in the extraction module (the code that takes a Rocq proof and produces an executable program).