We introduce RESpecBench, a multi-domain LLM benchmark with a sound and automated specification equivalence checker across multiple domains, measuring the LLM’s ability to produce precise, semantically equivalent specifications from informal natural language descriptions. We evaluate several state-of-the-art LLMs on RESpecBench and compare our sound verifier to LLM-as-a-Judge pipelines, demonstrating that LLM-as-a-Judge produces unreliable verdicts and substantially overestimates specification correctness.