It's nice to see private companies dive into the (automated) theorem proving and formal verification world, and I'm curious if throwing money at this will have a meaningful impact on the field (if that is what they're planning to do). It seems like we've slowly been getting to a point, where the tools we have available now might be combined in a way that makes some impressive progress on all this.
Turing-complete languages have an excessively broad semantics, which makes it hard to prove things about programs written with them. An alternative would be to build tools that allow engineers to develop DSLs quickly, and to then verify properties in programs written using said DSLs.
I can see some early signs of this trend in Idris, which is emphasizing DSL-building tools, or in smart contract projects, which are rushing to build contract languages with restricted semantics. There's also related work in Haskell and Racket / Scheme.
edit: It's ridiculous how you get downvoted for just asking a question in an unrelated thread. Just shows how rotten this whole space is.
But you can’t save people from bugs higher up the stack when it comes to turing complete contracts. It can definitely be better though.
Two projects that did use formal methods are the beacon chain deposit contract, and (iirc) Uniswap, and both have been fine.
And if you look at it from a technical perspective where your options are TLA+, Coq, Agda, Isabelle, etc, I think you’ll find most of the core devs are involved in blockchain somehow nowadays. At least that’s what it feels like.