There's an excellent online book that introduces Coq and how to use it for verification of programs: https://softwarefoundations.cis.upenn.edu/ https://software

There's an excellent online book that introduces Coq and how to use it for verification of programs: https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/. There's also a more advanced book, http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/, that goes into more detail. In comparison, Lean has little teaching material for formal verification of programs.