Official

• Isabelle

• Coq

• Lean Prover

• Agda

• ACL2

• HOL4

• HOL Light

Tutorials/Books

Isabelle

• Tobias Nipkow, Gerwin Klein: Concrete Semantics

• Lawrence C. Paulson: ML for the Working Programmer, 2nd Edition

• Gerwin Klein: Proof Craft

Coq

• Benjamin C. Pierce et al.: Software Foundations

• Adam Chlipala: Certified Programming with Dependent Types

Lean

• Jeremy Avigad, Leonardo de Moura, and Soonho Kong: Theorem Proving in Lean

• Kevin Buzzard and Mohammad Pedramfar: The Natural Number Game

Agda

• A List of Tutorials

HOL4

• The HOL System Description

Courses

• OPLSS(Oregon Programming Languages Summer School)

• Interactive Formal Verification

• Semantics of Programming Languages

• Advanced Topics in Software Verification

• 6.892 Interactive Computer Theorem Proving

• 15–815 Interactive Theorem Proving

• 15-815 Automated Theorem Proving(2014)

• CSE 291: Applied Automated Theorem Proving

• Theorem Proving - Principles, Techniques, Applications

• Theorem Proving with Isabelle/HOL An Intensive Course

• Automated Theorem Proving

Websites

• Machine Logic

• Isabelle Quick Access Links

• Isabelle Developers

• Proof Search

• Proof Engineering

• A Gentle Introduction to Automated Reasoning

Groups

• LRI Isabelle Club

• Chair for Logic and Verification

• Lawrence Paulson

• Matryoshka (Fast Interactive Verification through Strong Higher-Order Automation)

• Lean Forward

Competitions

• Proving for Fun

• Proof Ground

• Verify This