Open-source formal verification tool for all Starknet developers

Horus employs various Satisfiability Modulo Theories (SMT) solvers to ensure that your smart contract’s implementation meets specifications written in a simple assertion language. The Horus alpha release currently supports Cairo 0.10.1.

Smart contract security is more important than ever. In 2022, a total of $3.78 billion of total value locked (TVL) was lost from the crypto ecosystem due to exploits. As Ethereum scales and becomes more interoperable, the amount of TVL at risk and potential attack vectors will only increase. To secure the Ethereum and Starknet ecosystems, Nethermind has partnered with StarkWare to develop the Horus formal verification tool for Starknet smart contracts. What began as a modest prototype Python script, has grown to support many complex Starknet smart contract features. By leveraging Horus specifications, developers can detect software bugs that could lead to exploits and value losses before the contract is even deployed.

Horus streamlines the formal verification process for Starknet smart contracts, enabling developers to express assertions about their code using a straightforward assertion language. This language is similar to Cairo, making it especially user-friendly.

The heavy-lifting is built into Horus’s design. The tool allows developers to add preconditions and postconditions to Starknet functions, as well as other assertions that apply at various points in the code. It then verifies that for each annotated function, the postcondition remains valid after a non-faulting call to the function, assuming the precondition was met before the function was called. Horus achieves this by running the contract through a control-flow analysis and utilizing the resulting control-flow graph (CFG) to simplify the verification task. Instead of checking the entire contract, it focuses on verifying that individual "modules" meet specific specifications. A module, in this case, is a basic block annotated with a specification. The verification process for each module is then reduced to an SMT query, optimized and handled by various SMT solvers like Z3 and CVC5.

Our goal is to make formal verification more accessible for Cairo developers, fostering broader adoption and decentralization of the Starknet ecosystem.