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.)
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.
Powered by Refinement Types
Helmholtz is based on a theory of refinement types, which can describe relationship between elements on the operand stack.