I worked on a blockchain that used formal methods as part of the development workflow. The development process was essentially writing a paper that formalised a

I worked on a blockchain that used formal methods as part of the development workflow. The development process was essentially writing a paper that formalised an algorithm or a protocol, an implementation in Agda that would generate Haskell (or written straight in Haskell), property based tests against the paper, and then a whole business analysis/QA side where there'd be a requirements matrix against the paper with unit/integration/end-to-end tests on the features too. So you'd end up with formally checked code, property based tests, unit tests, integration tests, end to end tests, manual checks, and a few other tools too. This was a pretty slow process but on the two major product releases I worked on, I can only remember one bug slipping through and that was patched before people realised (and not a major issue either). So I think this style of development can work if you can 1) afford it, 2) afford the time to do it, and 3) formulate the requirements in such detail upfront. Here's an example of a formal method paper that explains how a specific protocol works: https://hydra.iohk.io/build/13099985/download/1/blockchain-spec.pdf https://hydra.iohk.io/build/13099985/download/1/blockchain-s... This is a fun example of doing something similar with Coq to build a porn browser: http://www.michaelburge.us/2017/08/25/writing-a-formally-verified-porn-browser-in-coq.html http://www.michaelburge.us/2017/08/25/writing-a-formally-ver... And there are a couple companies out there that do this style of development as a consultancy - it's probably the closest to 'engineering' that software development can get (in my eyes) https://galois.com https://galois.com