One Requirement, Many Specifications: Systematic Instability in LLM Specification Autoformalization

Verified code generation rests on a hidden assumption: that the formal specification a language model writes for a requirement is the specification the developer meant. Existing work asks whether such a contract is strong enough to rule out wrong programs, and stops short of asking whether the model writes the same contract twice. We test that question directly. Holding the requirement and the method signature fixed, we sample contracts from a model repeatedly and compare each pair with a two-sided oracle that either proves equivalence with an SMT solver or exhibits a concrete input on which the two contracts accept different results. On a stratified set of Dafny tasks, a small open code model produces provably inequivalent specifications for the same requirement on half of the tasks we can measure, and a four-times-larger model on 38% of them. Neither of the comfortable explanations survives: the rate stays above a third at near-greedy decoding, and it is essentially uncorrelated with a rated measure of how ambiguous the requirement is. The disagreements are entangled with correctness, since most inconsistent tasks contain a contract the oracle proves inequivalent to the benchmark reference. Because the oracle leaves a large band of pairs undecided, every rate we report is a sound lower bound. For the model family and language we study, autoformalization behaves as a distribution over contracts, so a single sampled specification is best treated as one draw from that distribution.