In this post (the sequel to “How to optimize your gas consumption without getting REKT”), we focus our attention on Solidity/Yul libraries that realize the mathematical and economic computations that lie at the heart of the DeFi world, and explain why equivalence checking is a potent tool in the hands of developers and auditors who wish to work on such code.

Developing a DeFi product is an engineering problem of deceptive depth — it is easy to write a smart contract in Solidity that (mostly) does what you want, but it is hard to do it well.

The first time that an automatic tool has found a bug in a public, open-source, Solidity library.