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)

  • Coq'Art website: http://www.labri.fr/perso/casteran/CoqArt/index.html
  • French Version: http://www.inria.fr/sophia/members/Yves.Bertot/coqartF.pdf http://www.labri.fr/perso/casteran/CoqArt/coqartF.pdf

• Certified Programming with Dependent Types by Adam Chlipala: http://adam.chlipala.net/cpdt/

  • PDF: http://adam.chlipala.net/cpdt/cpdt.pdf
  • HTML: http://adam.chlipala.net/cpdt/html/toc.html

• 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

  ​