A paper posted to arXiv on November 5 examines what “verified” means for code generated by large language models. It separates three checks: whether a verifier accepts code, whether its proof is bound to a specification, and whether that specification reflects the original requirement.
In one test, the authors report 99.1% verifier acceptance on HumanEval, but only 1.9% of samples had a certificate tied to a spec-defined predicate or function. In a separate Rust pipeline designed to ensure that binding, 11.48% of structurally verified MBPP-Rust samples and 14.82% on a VeriContest slice still failed hidden tests.
Why it matters
For teams using proof-checking to assess generated code, the results show that verifier acceptance alone may not establish either a meaningful link to requirements or correctness on hidden tests.
