That's verifying the implementation. The type system wasn't verified. It implements stuff perfectly, it has tests that prove it, but nobody formally verified that they perfectly implemented the correct algorithms