• Skip to primary navigation
  • Skip to main content
  • Skip to footer

Nethermind

  • Downloads
  • Docs
  • Projects
    • Solutions
      • DeFi for Institutions
      • Smart Contracts Audits
      • Real-time Monitoring
      • Formal Verification
    • Tools
      • Nethermind Client
      • Voyager
      • Horus
      • Warp
    • Protocol Research
      • MEV
      • Account Abstraction
      • Verkle Trees
  • DeFi Research
  • CompanyWe’re hiring!
    • About us & JobsWe’re hiring!
    • Expertise
  • Contact
  • Github Github
  • Twitter Twitter
  • Linkedin Linkedin
  • Medium Medium

Join our Discord

Horus Hero Desktop
Horus Hero Mobile

HORUS Open-source formal verification tool for all StarkNet developers

Github repo for Alpha release

Go to the next section

Formally verifying Cairo smart contracts

Horus is an open-source formal verification tool for StarkNet smart contracts. It provides developers with a user-friendly way to formally verify StarkNet smart contracts with respect to specifications written in a simple assertion language. Horus utilizes a variety of Satisfiability Modulo Theories (SMT) solvers to verify that the 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.

Simplifying Formal Verification on StarkNet

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.

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.

Collaborating on this project

Julian Sutherland Julian Sutherland @Julian-Sutherland František Silváši František Silváši @František-Silváši Agustín Martinez Suñé Agustín Martinez Suñé @Agustín-Martinez-Suñé Ilia Vlasov Ilia Vlasov @Ilia-Vlasov Rodrigo Ribeiro Rodrigo Ribeiro @rodrigogeraldo

Interested in helping Ethereum grow?
Check out our Job Openings or join our Internship Program!

  • Solutions
    • DeFi for Institutions
    • Smart Contracts Audits
    • Real-time Monitoring
    • Formal Verification
  • Tools
    • Nethermind Client
    • Voyager
    • Horus
    • Warp
  • Protocol Research
    • MEV
    • Account Abstraction
    • Verkle Trees
  • Downloads
  • Docs
  • About Us & JobsWe’re hiring!
  • Expertise
  • Contact
Logo Icon

Discord Discord Github Github Twitter Twitter Linkedin Linkedin Medium Medium

Nethermind 2023 - Legal

This website uses cookies to improve your experience. Accept Reject All
Manage consent

Privacy Overview

This website uses cookies to improve your experience while you navigate through the website. Out of these, the cookies that are categorized as necessary are stored on your browser as they are essential for the working of basic functionalities of the website. We also use third-party cookies that help us analyze and understand how you use this website. These cookies will be stored in your browser only with your consent. You also have the option to opt-out of these cookies. But opting out of some of these cookies may affect your browsing experience.
Necessary
Always Enabled
Necessary cookies are absolutely essential for the website to function properly. These cookies ensure basic functionalities and security features of the website, anonymously.
CookieDurationDescription
cookielawinfo-checkbox-analytics11 monthsThis cookie is set by GDPR Cookie Consent plugin. The cookie is used to store the user consent for the cookies in the category "Analytics".
cookielawinfo-checkbox-functional11 monthsThe cookie is set by GDPR cookie consent to record the user consent for the cookies in the category "Functional".
cookielawinfo-checkbox-necessary11 monthsThis cookie is set by GDPR Cookie Consent plugin. The cookies is used to store the user consent for the cookies in the category "Necessary".
cookielawinfo-checkbox-others11 monthsThis cookie is set by GDPR Cookie Consent plugin. The cookie is used to store the user consent for the cookies in the category "Other.
cookielawinfo-checkbox-performance11 monthsThis cookie is set by GDPR Cookie Consent plugin. The cookie is used to store the user consent for the cookies in the category "Performance".
viewed_cookie_policy11 monthsThe cookie is set by the GDPR Cookie Consent plugin and is used to store whether or not user has consented to the use of cookies. It does not store any personal data.
Functional
Functional cookies help to perform certain functionalities like sharing the content of the website on social media platforms, collect feedbacks, and other third-party features.
Performance
Performance cookies are used to understand and analyze the key performance indexes of the website which helps in delivering a better user experience for the visitors.
Analytics
Analytical cookies are used to understand how visitors interact with the website. These cookies help provide information on metrics the number of visitors, bounce rate, traffic source, etc.
Advertisement
Advertisement cookies are used to provide visitors with relevant ads and marketing campaigns. These cookies track visitors across websites and collect information to provide customized ads.
Others
Other uncategorized cookies are those that are being analyzed and have not been classified into a category as yet.
SAVE & ACCEPT