The new Pirouette 2 introduces formal method techniques to the verification of smart contracts; in this post we focus particularly in how incorrectness logic helps this goal.

What Happened On the morning of the 22nd of March, 2022, we were notified about the existence of an unknown critical vulnerability on one of Minswap’s contracts. Everyone here on the audit team was dismayed, since we had conducted an audit for Minswap not long before. We found…