I asked AI coding agents to write formally verified code. Every solution passed the verifier. Then I checked what the proofs actually promised. For the smaller model, 5 of 8 specifications barely said anything . One of the methods was wrong, and its proof was green. This post is about that gap, a cheap way to detect it, and a small open-source tool that does it for any Dafny file. The experiment I'm designing a programming language meant to be written by agents and che...