PV3 ⊧ Helmholtzverifies properties from program annotations

Verifier for smart contracts written in the Michelson language for the Tezos blockchain.

Application domain/field

• Smart contracts
• Blockchain
• Cryptocurrency
• Static verification
• Refinement types

Type of tool

Static verifier, auto-active verifier?

Expected input

Michelson 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.

Format:

Michelson (language)

Expected output

VERIFIED if the program satisfies the specification. Otherwise, UNVERIFIED.

Internals

Uses Z3 to discharge generated verification conditions.