This page is no longer being maintained. It has not been updated since March 2020. See, instead, the Formal Methods Teaching Committee web pages.

This page collects resources for anyone considering the use of formal methods and formal tools in a classroom. The effort grew out of a discussion that was held during the Big Proof program at the Isaac Newton Institute in Cambridge, UK. A recording of the discussion is available.

There are many axes along which one can organize such a list, such as the level of expertise of the intended audience (from experts to the public at large) or disciplinary orientation (computer science, mathematics, mathematical logic, etc.). Here I have chosen to classify the material by subject matter:

  • computer science: material for teaching students to use formal methods for computational purposes, e.g. courses on software design and verification.

  • mathematics: material for teaching mathematics, e.g. courses on discrete mathematics or introductions to mathematical proof.

  • logic and formal methods: materials for teaching logic and formal methods themselves, e.g. courses on dependent type theory and automated reasoning.

If you would like add something, just send the text as you would like it to appear to, preferrably already formatted in markdown. Entries should provide a link to the relevant resources, which in turn should make use of formal tools (theorem provers, SAT solvers, model checkers, etc.) in some way.

The source for this page is here, based on a template by Karl Broman.

Computer Science


Logic and Formal Methods

  • Jon Barwise and John Etchemendy, Hyperproof

    An introduction to logic, proof, and diagrammatic reasoning.

  • Femke van Raamsdonk, Hermann Guevers, et al., Type Theory and Coq

    An introduction to logic, type theory, and metatheory, using Coq.

  • Jacques Fleuriot, Automated Reasoning

    A course on automated reasoning, using Isabelle.

  • N. Shankar, L. de Moura, H. Ruess, and A. Tiwari, Little Engines of Proof

    A course on automated deduction and decision procedures.

  • Josef Urban, Chad E. Brown, and Ondřej Kunčar, Formal Mathematics and Proof Assistants

    A course using Mizar, Isabelle, and Coq.

  • The AProS project

    Includes a web-based introductory course on Logic and Proof.

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

    An introduction to dependent type theory and Lean.