Formal Verification (FV) refers to the use of static analysis methods to verify a design. Within Arm, I have mostly used a technique known as model checking, in which requirements of a design are expressed in a formal mathematical language (usually SystemVerilog Assertions), and tools are used to analyse whether there is any way that a given model of the design can fail to satisfy the requirements. FV is a static testing, differently from simulation, and it doesn't require any stimulus. The big advantage of FV is that it can give exhaustive proofs, meaning that the written property is always true for all the possible cases.