HORUS Open-source formal verification tool for all StarkNet developers
Formally verifying Cairo smart contracts
Horus is an open-source formal verification tool to formally verify your Starknet smart contracts. It provides a user-friendly way to formally verify Starknet smart contracts with respect to specifications written in a simple assertion language. Horus employs various Satisfiability Modulo Theories (SMT) solvers to ensure that your contract’s implementation meets these specifications. The Horus alpha release supports Cairo 0.10.1, with a Cairo 1.0 release coming soon.
Detect vulnerabilities before deployment
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.
Formal verification on Starknet made easy
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.
Our Formal Verification Team
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.
