65 - Scribble
Scribble is a verification language and runtime verification tool that translates high-level specifications into solidity code. It allows you to annotate a solidity smart contract with properties (See here).
- Principles/Goals:
- Specifications are easy to understand by developers and auditors
- Specifications are simple to reason about
- Specifications can be efficiently checked using off-the-shelf analysis tools
- A small number of core specification constructs are sufficient to express and reason about more advanced constructs
- Transforms annotations in the Scribble specification language into concrete assertions
- With these instrumented but equivalent contracts, one can then use Mythril, Harvey, MythX
- Verification Tool
- ConsenSys Diligence
- Annotations -> Assertions
- Instrumented + Equivalent Contracts
- Run Harvey/Mythril/Mythx