I think you have to first figure out what "correct" even is.

Correct with regards to a formal specification?

How do we know the specification is "correct"? By definition?