M

Mi-Cho-Coq

A specification of Michelson in Coq to prove properties about smart contracts in Tezos.