Customized Formal Verification: The Five Step Process

This post explains CertiK's custom formal verification process for Solidity smart contracts, detailing the BISSOL specification language, translation tools to Dafny, an interactive verification workflow, and example verifications that uncovered issues such as incorrect reward calculations, underflow/overflow, potential DoS, and missing state updates; it frames the approach, tooling, and example findings rather than reporting an active security incident.