On April 2016 slock.it starts a venture capital DAO, called The DAO. Two months later an attacker exploits a recursive calling vulnerability and steals $55 million from The DAO in front of anyone who cares and cannot be stopped. From that moment on, security and verification in smart contracts becomes a central topic.
WhatI employed colored petri networks to model and verify two smart contracts. The first contract is Pyramid: an example of a fraudolent pyramidal scheme. The second contract is WETH9: a contract which allows to convert ETH in wETH tokens.
HowColored Petri Networks have been implemented with CPN-tools and the verification code has been written in ML.