LLM hunt finds bugs in Tamarin security prover

Nadim Kobeissi reports that an LLM-assisted search turned up critical bugs in Tamarin, the open-source symbolic prover widely used to analyze cryptographic protocols. He has published artifacts and a forthcoming paper, and says the findings were disclosed to the Tamarin developers.

Maintainer Felix Linker confirmed that two of the reported cases were real defects and that both have been fixed. In one family of examples, user input could mention an internal-only keyword that the tool did not reject thoroughly enough. In another, Tamarin accepted a model that deserved at least a clear warning. Linker rejected other examples as non-bugs, arguing that apparent proofs of false claims depended on auxiliary results that were themselves never established.

The sharper dispute is classification. Kobeissi calls the confirmed defects soundness bugs: the prover could treat unsafe input as fine for induction-related checks, which is exactly the kind of failure formal tools are supposed to prevent. Linker has said it is debatable whether a soundness bug occurred because no proof rule changed, described a related change as defensive programming, and has declined to settle the label. Kobeissi counters that someone on the project will eventually have to, because the wording in release notes will decide whether users who relied on the affected patterns must re-check models after they upgrade.

The exchange sits in a wider pattern: automated proof assistants are increasingly stress-tested by machine-generated proofs, and small gaps in input validation or safety checks can let a false result look verified. For protocol designers who treat a green Tamarin run as assurance, the practical question is less the taxonomy than whether past analyses need another look once the fixes ship.