People are talking about using formal methods and more specifically formal proofs in the context of the blockchain. I just provide a few pointers for Coq: the recent developments and efforts are interesting and worth following:
- A formally verified compiler for C which is Xavier Leroy's project for several years now: http://compcert.inria.fr/ . It is a huge project with a ton of work.
- Bedrock is interesting too, it is a library of building blocks to manipulate for instance pointers, data and specifications: http://plv.csail.mit.edu/bedrock/.
- Package lists: https://coq.inria.fr/opam/www/
- It is a live and active community.
Still, in my humble opinion it is not something that is easy to understand, or to perform, even if you already have a good idea of the formal proof.
Tutorials:
- Mike Nahas: https://coq.inria.fr/tutorial-nahas
- Pierre Castéran & several authors: http://www.labri.fr/perso/casteran/index.html
Classes:
- Yves Bertot and Pierre Castéran: http://www.labri.fr/perso/casteran/CoqArt/Tsinghua/index.html
- Check Adam Chlipala book page, where there is a list of classes at the end: http://adam.chlipala.net/cpdt/
List of Books:
Coq'Art by Yves Bertot and Pierre Castéran, only the french edition is freely available (http://www.springer.com/gp/book/9783540208549)
Certified Programming with Dependent Types by Adam Chlipala: http://adam.chlipala.net/cpdt/
Software Foundations Series: https://softwarefoundations.cis.upenn.edu/ which is a recent effort on Coq and covers many other subjects: semantics, models for instance:
- Logical Foundations: https://softwarefoundations.cis.upenn.edu/lf-current/index.html
- Programming Language Foundations: https://softwarefoundations.cis.upenn.edu/plf-current/index.html
- Verified Functional Algorithms : https://softwarefoundations.cis.upenn.edu/vfa-current/index.html