When Postconditions Help or Mislead: An Empirical Study of LLM Code Review

LLM code reviewers see what code does but not what it is supposed to do, so they flag correct code and miss real bugs. Postconditions state intended behavior explicitly, and LLMs can now infer them, but LLM-inferred postconditions are often incomplete. We ask two questions: do the benchmark’s validated reference postconditions help LLM code reviewers, and what happens when LLM-inferred postconditions are used instead? Using PostcondBench, we review 210 real-world Java methods, each in its bug-free original form and as three mutants. The reviewer sees the method alone, the whole source file, or the method with either the reference or the LLM-inferred postconditions. Three frontier reviewers, Claude Opus 5.5, Gemini 4 Argon and GPT-6.1 Sol, produce 17,640 reviews, which we score against the benchmark. For Claude and Gemini, adding the reference postconditions cuts false alarms by more than half, whereas adding the whole source file does not significantly change them. In our main prompt, the LLM-inferred postconditions come with the instruction “Treat them as the specification”. With it, GPT-6.1 Sol finds 16 percentage points fewer bugs; on bugs the postconditions do not cover, its rate falls from 82% to 21%. Claude’s and Gemini’s false alarms fall by 6.2 and 4.8 points, but not significantly. A follow-up experiment shows that the instruction causes GPT-6.1 Sol’s drop: without it, the same postconditions help GPT-6.1 Sol find more bugs than with no postconditions (89.5% vs. 86.3%), and its false alarms stay about the same. Some of what the benchmark counts as GPT-6.1 Sol’s false alarms are real: in 19 of the 23 cases we could check, the code breaks its reference postconditions on an input the benchmark’s tests never try. Postconditions should therefore be given to a reviewer as information, not with an instruction to treat them as the specification.