Skip to main content

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 using tezos-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 outputs VERIFIED or UNVERIFIED.