Formal verification is not the same as a traditional security audit. With formal verification, contract code is verified at the bytecode level using tools developed based on a mathematical model of the EVM. The result is a level of assurance that traditional reviews, limited to reviewing the Solidity code itself, cannot offer with respect to the functional correctness of the code.
During a formal verification engagement, RV formalizes the requirements of the smart contract. That is, all the properties shared become mathematical theorems, proved using RV’s verifier/prover at the EVM bytecode level, making sure all corner cases are rigorously specified and verified. With respect to work allocation, the majority of tasks assigned to verification engineers do not go into the actual verification, but rather in formalizing the actual properties. Security auditors do not do this because they do not possess the required expertise or access to the necessary tools to verify the code against the specs.
RV has discovered issues in all the contracts its verified. Not always issues that can be exploited, but issues clients chose to fix because they are committed to the correctness of their contracts. Contracts that appear correct can be broken with specific inputs at particular corner cases. The human mind simply cannot keep track of all such corner cases, which is why tools based on mathematical models of the computing infrastructure, i.e. the EVM bytecode, are necessary.