Both @adamnemecek and I have said the blockchain ventures might be a good way to get money into formal methods development. Rosu’s group is wisely doing just that: using their K Framework to build a VM for blockchains both as a demo of its utility and way to possibly get funding into it. The K Framework is the tool they used to build an executable, formal semantics for C setup to work like GCC compiler. Since it uses K, Rosu et al say those developments automatically “yield an interpreter, debugger, state space search tool, and model checker ‘for free.’” Before blockchain stuff, Rosu spun off the tool into a company for static analysis of C and Java programs with the one for C claiming to catch a lot of bugs. They claim they get no false positives thanks to the semantics.

What makes me bring K up more than some tools is that the rewriting/equational tools such as Maude and K (originally done on Maude) get a lot less attention than HOL or Coq. That’s despite their model making some kinds of verifications really easy in comparison to how people typically use the others. Anyone wanting to play with a different style of formal method might want to check out Maude and/or K. Rosu also keeps a list of project ideas for K, the simplest being a new language. Rust or Nim with a translator to their C semantics would be a nice one with a lot of benefits on the language using K’s tools or output using C-oriented tools.