Exactly :) And a proof that the spec is correct.

But without formal verification both your spec and the implementation may be incorrect.