Liquidity

Liquidity is a high-level typed smart-contract language for Tezos that strictly complies with Michelson security restrictions. A formal verification framework for it is under development. A formal-method framework for Liquidity is under development, to prove the correctness of smart-contracts written in Liquidity. The Liquidity language provides the following features: full coverage of the Michelson language: Anything that can be written in Michelson can be written in Liquidity; local variables instead of stack manipulations: values can be stored in local variables; high-level types: types like sum-types and record-types can be defined and used in Liquidity programs. Liquidity already covers 100% of the Michelson features, and contracts generated with Liquidity can be submitted on the current mainnet and zeronet.