There's tooling like Cryptol and SPARK to make this a lot easier than it was in the past. Cryptol can generate software or hardware that implements the high-lev

There's tooling like Cryptol and SPARK to make this a lot easier than it was in the past. Cryptol can generate software or hardware that implements the high-level spec of the algorithm. Far as practical use, certainly not just one even though still extremely rare. Here's some more: Altran/Praxis Correct-by-Construction for a cert authority http://www.sis.pitt.edu/jjoshi/Devsec/CorrectnessByConstruction.pdf http://www.sis.pitt.edu/jjoshi/Devsec/CorrectnessByConstruct... Same company ports Skein from C to SPARK, finds trouble http://www.skein-hash.info/sites/default/files/SPARKSkein.pdf http://www.skein-hash.info/sites/default/files/SPARKSkein.pd... SPARK Ada is available under GPL and commercial licenses. The book below is quite easy to read compared to most stuff with formal methods. The companies building stuff like this usually also have tools to generate tests (property-based testing) from contracts/specs and can automatically turn anything you can't prove into runtime checks. Shocked it's not used more often in areas like smart contracts or cryptocurrency protocols. https://www.amazon.com/Building-High-Integrity-Applications-SPARK/dp/1107656842/ref=sr_1_1?ie=UTF8&qid=1538687861&sr=8-1&keywords=high+integrity+applications https://www.amazon.com/Building-High-Integrity-Applications-... Galois built Cryptol for NSA but open sourced it. https://www.cryptol.net/ https://www.cryptol.net/ Rockwell Collins built SHADE and some other tools for high-assurance crypto. They build stuff for the defense sector mainly funded by NSA. They even have a separation-preserving, verified CPU. http://www.csl.sri.com/users/shankar/VGC05/Hardin.pdf http://www.csl.sri.com/users/shankar/VGC05/Hardin.pdf