Even if formal methods could make your contracts bulletproof, they don't help at all when people don't use them. The barrier to entry in smart contract developm

Even if formal methods could make your contracts bulletproof, they don't help at all when people don't use them. The barrier to entry in smart contract development is pretty low, and lots of people don't do everything they should to minimize risk. Two projects that did use formal methods are the beacon chain deposit contract, and (iirc) Uniswap, and both have been fine.