Specs (and proof checkers) can have bugs too!

Specs (and proof checkers) can have bugs too!

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.