If I am not mistaken, the verification is problematic here. It's run too late.
A piece of code that satisfies a single test will most likely not be probable to adhere to the spec.
Worse, the whole spec can only be correctly implemented in total. You cannot work iteratively by satisfying one constraint after the other. The same holds for the test cases. That means that satisfying the last test or fulfilling the last constraint will take much more work than the first. The number of tests passed is not a good metric for completion of the implementation.