I've worked with using formal verification systems to secure smart contracts. It's less useful than you would think, for two reasons: 1. It's extremely hard to

I've worked with using formal verification systems to secure smart contracts. It's less useful than you would think, for two reasons: 1. It's extremely hard to come up with the correct rules for expected behavior. It's like making a safe wish versus an evil genie. It's also surprisingly easy to make a rule that doesn't check anything, or what you think it does. 2. In the areas that deal with the most money, DeFi, there may be thirty program involved, most of which were not made by you or under your control. Current formal methods can just handle a single program. The common way to handle networks of contracts is to test each in isolation, making assumptions about what the other contracts can do. But it's really easy to make a wrong assumption here.