Introduction
Helmholtz is a static verification tool for a stack-based programming language Michelson, a smart contract language used in Tezos blockchain protocol. It verifies that a Michelson program satisfies a user-written formal specification.
Helmholtz accepts a Michelson program annotated
with its formal specification and hints (e.g., loop invariant) used by Helmholtz. An annotation is
surrounded by <<
and >>
.
Helmholtz works as follows.
- Helmholtz strips and preserves the annotations surrounded by
<<
and>>
and typechecks the stripped code usingtezos-client typecheck
; the simple type checking is conducted in this step. - After typechecking, it generates verification conditions using the preserved annotations.
- Then, Helmholtz discharges the conditions with
z3
and outputsVERIFIED
orUNVERIFIED
.