Smart Contract Verification Platform

State-of-the-art formal verifier for Ethereum smart contracts, built based on the latest research, is now available to security auditors and developers as Software as a Service.

Powered By

  • SECURIFY

    Verifier for common security vulnerabilities

    Try Demo
  • VerX

    Verifier for custom safety specifications

    Try Demo

State-of-the-art formal verifier for Ethereum smart contracts, built based on the latest research, is now available to security auditors and developers as Software as a Service.

Powered By

  • SECURIFY

    Verifier for common security vulnerabilities

    Try Demo
  • VerX

    Verifier for custom safety specifications

    Try Demo
  • vulnerabilities scan

    Scans smart contracts for critical vulnerabilities using an extensive list of properietary security patterns.

  • automated

    Uses the latest advances in machine learning and program analysis to fully automated the verification process.

  • custom specifications

    Allows auditors to express custom functional specification to define the intended behavior of contracts.

  • no missed bugs

    Analyzes all behaviors of the smart contract to prove that the contract is free of bugs.

For developers

Use the verification platform as part of your development process to continuously verify your smart contracts during development.

Download Client

For enterprises

Integrate the verification platform within your product to expand the capabilities of your platform or protocol with smart contract verification.

API Docs Request License

FAQ

What functional requirements are supported?

Our platform supports functional requirements expressed in a expressive specification language that can many common requirements encountered during an audit, such as:

Access control, such as: “Only the Crowdsale can change the state of the escrow”

State-based invariants, such as: “The sum of deposits equals the Escrow’s balance while in state OPEN”

State transition invariants, such as: “After the Escrow transitions to state CLOSED, it remains in state CLOSED forever”

Invariants over aggregates, such as: “The sum of deposits equals the Escrow’s balance”

Multi-contract invariants, such as: “The Escrow is in state SUCCESS only if the amount of raised funds exceed the goal of the Crowdsale”

To ease adoption, our specification language is based on Solidity, which we have extend with temporal operators (such as, always and once) so to enable quantifying over a contracts’ states.

What guarantees does the platform provide?

If the platform verifies a functional property, then it guarantees that the property will hold for the entire lifetime of the contract, regardless of what kind and how many transactions attackers/users submit to it. This is in sharp contrast to existing bug-finding security tools, for example based on symbolic execution or fuzzing, which do not provide formal guarantees.

How does the platform differ from other security tools?

Our platform can formally verify custom functional requirements specified by auditors and developers, which makes it an indispensable tool when it comes to verifying deeper functional requirements of contracts. In contrast, remaining automated tools focus on checking generic vulnerabilities, such as reentrancy or buffer overflows, and do not provide formal security guarantees.

How can the platform verify Turing-complete contracts?

Our platform uses a novel sound abstraction technique to over-approximate the set of reachable states of the smart contracts while maintaining sufficient precision to prove the relevant functional correctness requirements.

How can I get access to the platform?

Our platform can be used as Software as a Service. The client can be downloaded from here. You will need credentials to submit your request, please contact us.