Automated formal specification synthesis has been advancing fast, with recent work reporting high verifier pass rates for LLM-generated JML specs. A new paper asks the uncomfortable follow-up question: does passing the verifier actually mean the specification is correct and complete? The answer, backed by a new evaluation framework called Spec-Harness,