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.