A new benchmark called VeriCodeBench puts large language models through a tougher test: write the code, write the formal specification that's supposed to prove it correct, then verify both - no answer key provided.
Researchers built VeriCodeBench with 400 problems spanning C, Java, Rust, and Python, breaking from prior benchmarks that handed models a ready-made specification and only asked them to generate matching code. Here the model has to produce its own specification first, then the code, then a machine-checkable proof that the two actually line up - the full pipeline, no shortcuts. The team also introduces CodeNova, a method that forces the specification to spell out constraints explicitly and uses feedback from the verifier to patch failed implementations. Across every language tested, self-generated specifications were the weak link - models that wrote more elaborate specs did not reliably verify more successfully.
That gap matters because most "AI writes verified code" demos quietly assume a human already wrote the spec, which is the hard, error-prone part of formal verification. VeriCodeBench measures whether a model can do the entire job unsupervised, which is the version of this problem that would actually let a team trust generated code without a human spec-writer checking its work.
Per the paper, CodeNova's biggest gains showed up on a model the authors call "Claude Sonnet 5" - a name that doesn't match anything Anthropic has actually shipped, since its current lineup tops out at the Claude 4.x family and Fable 5. Treat that specific result as unverified until someone reproduces it on a model that exists.