My point is, the "national formal verifier" doesn't enter the picture. The entity in the role of a formal verifier in this story gave the correct answer and it didn't help.