Skip to main content

Helmholtz

Verifier for Tezos Smart Contracts

Verification for Michelson

Helmholtz is designed to be a static verifier for Michelson, the smart contract language running on the Tezos blockchain platform. (It is named after Hermann von Helmholtz, who was a thesis advisor of Albert Michelson.)

Fully Automated

All you have to do is to annotate your contract with its functional specification (such as pre- and post-conditions, loop invariants); Helmholtz will automatically generate verification conditions and discharge them by using an SMT solver such as Z3.

{ x : T | φ }

Powered by Refinement Types

Helmholtz is based on a theory of refinement types, which can describe relationship between elements on the operand stack.