PV3 ⊧ Helmholtzverifies properties from program annotationsVerifier for smart contracts written in the Michelson language for the Tezos blockchain.
- Smart contracts
- Static verification
- Refinement types
Type of toolStatic verifier, auto-active verifier?
Expected inputMichelson program annotated with a user-defined specification. The user-defined specification should be expressed in a refinement type. The user may also need to provide additional annotations such as loop invariants.
VERIFIED if the program satisfies the specification. Otherwise,