Right, it says "convincing argument that the C implementation does the same thing as the mathematical specification" and "Assuming that we didn’t accidentally program the same “bug” into our Cryptol spec".
My understanding is it's another way of white-box testing the code against specified behaviour, but just that using a (proven?) mathematical specification for algorithms is probably easier than writing unit tests that have to capture all edge cases. (In essence, it sounds like verification software is probably set up to detect such edge cases, which I do think is a good idea, because you only have to program such software once.)
