HORUS Open-source formal verification tool for all StarkNet developers

Smart contract security is more important than ever. In 2022, a total of $3.78 billion of TVL was lost from the crypto ecosystem due to exploits. As Ethereum scales and increases in interoperability, the amount of TVL at risk and the number of potential attack vectors will follow. To secure the Ethereum and StarkNet ecosystems, Nethermind has partnered with StarkWare to develop the Horus formal verification tool for StarkNet smart contracts. Starting as a simple prototype python script, it has grown to support many complex StarkNet smart contract features. Using Horus specifications, developers can detect software bugs that lead to exploits and value losses before the contract is even deployed.

Horus simplifies the process of formally verifying StarkNet smart contracts, allowing developers to express various assertions about the behavior of their code using a simple assertion language. This assertion language is similar to that of Cairo, making it particularly easy to use.

The heavy-lifting is built into Horus’s design. The tool allows developers to annotate StarkNet functions with preconditions and postconditions, along with other assertions that hold at intermediate points in the code. It will then verify that for each annotated function, the postcondition holds after a terminating call to the function that doesn't fault - assuming that the precondition held before the function was called. Horus performs this by putting the contract through a so-called control-flow analysis and using the resulting control-flow graph (CFG) to reduce the problem of verifying that the contract satisfies the annotated specifications to simply verifying that individual “modules” satisfy specific specifications. A module here is a basic block annotated with a specification. The verification process of individual modules is now reduced to an SMT query to be optimized and discharged using a variety of SMT solvers, such as Z3 and CVC5.

By making formal verification more accessible for Cairo developers we aim to positively contribute to the wider adoption and decentralization of the StarkNet ecosystem.

The Horus development team at Nethermind is made up of experts in formal verification, type theory and logic. The team formally verifies smart contracts and develops a variety of formal verification tools, particularly for EVM-compatible chains and StarkNet.

Find out more about our Formal Verification work.

Formal Verification at Nethermind

 

Disclaimer: Horus is currently in the alpha stage and no guarantee is being given as to the accuracy and/or completeness of any of the outputs the tool may generate. More information can be found here.