Passing tests shows a program worked on the cases tried, not every case. A formal verifier, a tool that checks mathematical claims about code, can help, but acceptance alone may not show that those claims describe the intended requirement.
The work separates three checks: whether the verifier accepts the code, whether its proof connects to a written specification (a precise statement of required behavior), and whether that specification matches the original request. It audits code-generation pipelines using Dafny, a tool.
On one coding benchmark, 99.1% of samples passed the verifier, but only 1.9% had proofs connected to a specification. In another pipeline, some code passed structural checks yet failed hidden tests. A verifier pass alone can therefore overstate how much confidence it provides.