Formal Verification

Using mathematics to prove that code satisfies precise properties (specifications) for all possible inputs, rather than only the cases you test. For smart contracts it catches rare-state bugs that testing and auditing miss — but it proves the code matches the specification, so a wrong or incomplete spec, or a risk outside the verified logic (economics, oracles, other contracts), can leave a 'verified' contract exploitable. A strong rigour signal for its scope, never a standalone guarantee of safety.