Why can I verify code against a spec but not verify the spec itself?

Formal verification for smart contracts proves that code satisfies a written specification, but it cannot determine whether that specification actually captures the contract's intended behavior. A 2025 MDPI survey covering state-of-the-art automated audit tools found they detect only 8 to 20 percent of exploitable bugs found in production, while reporting over 90 percent coverage of low-level syntax patterns. The gap sits in the spec: logical errors, asset lock conditions, and oracle assumptions almost never appear in specs because engineers do not know how to enumerate them before an exploit demonstrates the need. The NDSS 2025 PropertyGPT paper states directly that the community still lacks automated generation of comprehensive properties for effective formal verification. Every audit that clears a contract against an incomplete spec produces a false confidence floor rather than a safe