Preventing Unknown Attacks in DeFi

We describe how Morpho, EigenLayer, and Safe secured their smart contracts against potentially unknown attacks by formally proving that transactions behave as expected, assuming that the attacker calls smart contracts arbitrarily.