The "formal" specification is the goal, but the starting point is a rather informal specification. So it is an iterative process where you discover a bug and then have to figure out whether the bug is in the implementation or the interpretation of the presentation (i.e. the test).