Background: I do believe that ARM VFP was formally verified. Is that correct?
A simple question: which formalism / theorem prover was used to formally verify ARM VFP?
Extra: where is to find more details about ARM VFP formal verification?
I do believe that ARM VFP was formally verified. Is that correct?
Most likely formal verification was used.
Which formalism / theorem prover was used to formally verify ARM VFP?
TL;DR - Many.
I think you have a misconception that formal verification verifies everything. Just as compiler warning do not guarantee correct code, neither does formal verification. Formal verification starts with requirements engineering. That is the specific properties of a system that need to be fulfilled. A requirement like 'Its got to be good' is not a formal requirement. Each tool may have a specification language to state the requirements to be verified.
Some tools can only verify certain properties. Often the requirements may have some defect. In the case of a requirement defect, the formal verification will not catch it. Because of these issues, multiple tools are used. Ie, a tool for verifying an architecture is not the same as a tool to verify verilog code.
Where is to find more details about ARM VFP formal verification?
Almost certainly a different tool would be used to verify the mathematical accuracy versus the bus timing. Also as you move from high level design to actually silicon implementation, there are various issue that crop up and you need to 're-verify' the properties of the higher level are still constant. So 'high level model -> verilog -> simulation -> synthesis -> volume manufacturing' probably each have there own set of tools to ensure consistency between the layers.