I think you are spot on. Cryptocurrencies grew very fast to capture the market. They had no time to apply formal methods. But now they are rushing to do so. The

I think you are spot on. Cryptocurrencies grew very fast to capture the market. They had no time to apply formal methods. But now they are rushing to do so. There are many job offers in the formal methods, a market that was previously close to zero, and they come mostly from blockchain projects. Formal methods have been limited to industries that are very conservative and where code moves slowly. I used them in railway systems and real-time systems for avionics, more than a decade ago. Finding jobs out of that area was not easy. I'm hoping that advances in synthesis, thanks to mixing DL transformers and the already great SAT/SMT solvers, help making formal methods less costly to apply and much more popular. here are lots of interesting and practical ideas in refinement types (e.g. Liquid Haskell), theorem proving (e.g. translators from OCaml to Coq), etc. that would benefit a lot from automation.