This repository was originally intended as a log of my learning of the Coq proof assistant. My interests have since grown enormously in breadth and so the document has surpassed its original scope. At this moment, I'd like this place to collect and categorise interesting and useful resources on the theory and applications of various methods of formal verification. This includes topics such as theorem proving, higher-order logic, lambda calculus, type theory, model checking, automated reasoning and so on.

During my adventures in the software verification land, I too often grieved that there was no single book or website that would concisely and eloquently describe some of the methods of the field, the software packages it employed, the jargon or connections to other fields of research. To the best of my knowledge, there is still no such book, survey article, podcast or any other resource. My vision is to fill this gap and provide a sort of signpost or handbook for readers who are new to this area and are eager to learn all of it.

I do not yet claim completeness, correctness, consistency or usefulness of any of information contained herein.

• Useful resources on Coq
  • Coq-related blogs
• Libraries and plug-ins for Coq
• Applications of Coq
  • Papers and articles using Coq
• Related languages, tools and stuff
  • Journals and book series
  • Conferences and workshops
  • Proof assistants, provers and languages
  • Model checkers
  • SAT & SMT solvers
  • Other tools
  • Formal methods in practice
  • Learning resources
• Type theory
• Copyright

Useful resources on Coq

• Official Coq documentation
  • The official documentation is OK, quite comprehensive. The description of tactics is very good, there are few undocumented points.
  • Reference Manual
  • Tutorial
    • A simple and straightforward introduction to basics of proofs using Coq
• Official wiki on GitHub
• The coq-club mailing list
• B. C. Pierce et al.: Software Foundations probably the best introduction into Coq and theorem proving available
• A. Chlipala: Certified Programming with Dependent Types an awesome book to read after Software Foundations; a bit more advanced, slightly different topics; puts forth the idea of using automation whenever possible
• I. Sergey: Programs and Proofs: Mechanizing Mathematics with Dependent Types (draft)
• /r/coq
• Coq in a Hurry
• Introduction to the Coq proof-assistant for practical software verification course notes
  • Another tutorial, slightly more interesting; possibly outdated
• Coq'Art the first ever book on Coq and CoC
  • See also Pierre Castran's page for A Tutorial on [Co-]Inductive Types in Coq and A Gentle Introduction to Type Classes and Relations in Coq
• the nLab wiki
  • its page on Coq, for instance

Coq-related blogs

• Poleiro
• Gagallium blog of the Gallium research team at Inria
• Guillaume Claret's Coq blog
• Coq en Stock
• Homotopy Type Theory blog
  • Modules for Modalities an article on Coq's module system and universe polymorphism
• The Type Theory Podcast

Libraries and plug-ins for Coq

• Ssreflect and MathComp
  • "A Small Scale Reflection Extension for the Coq system"
  • "Computing with Univalence" (2008; slides)
• CoLoR "a Coq Library on rewriting and termination"
• coq-ext-lib "a collection of theories and plugins that may be useful in other Coq developments"
• std++ an extended standard library
• Equations dependent pattern matching
• Mtac "a monad for typed tactic programming in Coq"
• coq-dpdgraph plug-in for exploring dependencies between Coq objects
• wilcoxjay/tactics some useful tactics by James Wilcox
• "A Formal Library for Elliptic Curves in the Coq Proof Assistant" (GitHub)
• Coquelicot library for real analysis
  • C. Lelay (2015): "How to express convergence for analysis in Coq"
• Coq.io and others by Guillaume Claret (GitHub)
• coq-haskell
  • Applied: coq-pipes
• CFML: Characteristic Formulae for ML verification of correctness and amortized complexity of OCaml programs
  • A series of blog posts on the Gagallium blog on verifying complexity
• Verified Software Toolchain (VST)
  • tons of articles around this
  • A. W. Appel: "Verified Software Toolchain" (2011)
  • A. W. Appel: "Verification of a Cryptographic Primitive: SHA-256" (2016)
• "Category Theory in Coq 8.5" (Bitbucket; Coq Workshop 2014)
• CH2O formalization of ISO C11 by Rober Krebbers (GitHub)
  • "Formalizing C in Coq" (CoqPL 2015)

Applications of Coq

• CompCert verified optimising compiler of a substantial subset of C99
  • X. Leroy et al.: "CompCert A Formally Verified Optimizing Compiler" (2016)
• Verasco verified static analyser
• DopCert framework for formally verifying database query optimizations; uses HoTT
  • S. Chu, K. Weitz, A. Cheung, D. Suciu: "HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics" (2016)
• JSCert: Certified JavaScript
  • "A Trusted Mechanised JavaScript Specification" (2014; slides)
• Cosa Coq-verified Shape Analysis
• "A Machine-Checked Proof of the Odd Order Theorem"
• "A Reflexive Formalization of a SAT Solver in Coq" (2008)
• "Towards an effective formally certified constraint solver" (2014; slides)

Papers and articles using Coq

• Heq: a Coq library for Heterogeneous Equality
• "Inductive-inductive definitions"
• "Gradual Certified programming in Coq"
• "An intro to (co)algebra and (co)induction"
• "Canonical Structures for the Working Coq User"
• "Foundational Property-Based Testing" QuickChick, a port of QuickCheck to Coq
• J. Gross: "Coq Bug Minimizer" (CoqPL 2015; GitHub)
• C. Doczkal, J.-O. Kaiser, G. Smolka: "A Constructive Theory of Regular Languages in Coq"
• F. Chyzak, A. Mahboubi, T. Sibut-Pinote, E. Tassi: "A Computer-Algebra-Based Formal Proof of the Irrationality of (3)"
• HAL Loria Archive, (Department 2: Formal Methods](https://hal.inria.fr/LORIA-FM/index/index)

Related languages, tools and stuff

For tools, see also page on the Coq website.

• DeepSpec: The Science of Deep Specification an NSF-funded initiative aiming to unify existing tools at the specification level and develop new ways to write "good" specifications
• Homotopy Type Theory the book and the library
  • Coq for Homotopy Type Theory a dedicated research project
• UniMath (Univalent Foundations)
• Queensland Functional Programming Lab

Related ACM Special Interest Groups: SIGPLAN, SIGLOG and SIGACT.

Journals and book series

( denotes open-access journals)

• Logical Methods in Computer Science 
• Electronic Proceedings in Theoretical Computer Science (EPTCS) 
• LIPIcs: Leibniz International Proceedings in Informatics 
• International Journal of Foundations of Computer Science
• Information and Computation
• Journal of Automated Reasoning
• Studies in Logic, Grammar and Rhetoric 
• Springer's Lecture Notes in Computer Science series

Meta

• ACM Journals/Transactions
• Elsevier journals on computer science
• Springer journals on CS
• Cambridge Journals on CS

Conferences and workshops

See the standalone file.

Proof assistants, provers and languages

• Lean a new theorem prover developed by Microsoft and CMU with automation support; based on CIC, supports HoTT as well
• Matita based on (a variant of) CoC
• Agda a (relatively) new, hip dependently-typed functional language and interactive theorem prover
  • Agda Tutorial
• Idris another new and hip "general purpose" language with dependent types, support for theorem proving and tactics; kind of like Coq-flavoured Haskell
• Dedukti proof checker based on the -calculus; tools for translation from other proof assistants available
• the PRL Project a.k.a. Nuprl
  • MetaPRL
  • JonPRL (GitHub) a reimplementation of Nuprl by Jon Sterling, Danny Gratzer and Vincent Rahli
  • Red JonPRL yet another reincarnation by Jon Sterling
• MetaPRL
• miniprl a minimal implementation of PRL in Standard ML
  • cha an implementation in Haskell
• Isabelle great Archive of Formal Proofs; small trusted meta-logical core, usually used along with HOL
  • Haskabelle
  • Isar
  • Isabelle/HOLCF paper, tutorial
  • Archive of Formal Proofs an extensive collection of proof libraries for Isabelle
• HOL by Michael Gordon et al. the original system for interactive theorem proving in higher-order logic
  • HOL Light small trusted core
  • HOL4
• MINLOG interactive proof assistant based on first-order natural deduction calculus
• ProofPower based on higher-order logic
• Mizar
• ACL2 (A Computational Logic for Applicative Common Lisp) logic for modelling systems and a complementary prover; based on first-order logic
• Milawa theorem prover for ACL2-like logic
  • The reflective Milawa theorem prover is sound (2015)
• ATS (Applied Type System) dependently typed functional languge
• E theorem prover for first-order logic
• LEGO proof assistant
• F7 extension of F#'s type system with refinement types, dependent types and -calculus-style concurrency
• F* "a new higher order, effectful programming language designed with program verification in mind"
• Eff functional language with first-class effects and native handling of all kinds of computational effects without touching monads
• Twelf
• Celf
• Abella
• Beluga
• Delphin
  • C. Schrmann, R. Fontana, Y. Liao: "Delphin: Functional Programming with Deductive Systems"
• Andromeda type theory with equality reflection
  • Andrej Bauer's Leeds workshop slides and some interesting discussion in the comments below
• Prover9 and Mace4 and automated theorem prover for FOL and searcher for counterexamples, respectively
• leanCOP tiny automated theorem prover for classical first-order logic implemented in Prolog
• PVS
• Guru
  • A. Stump, et al.: "Verified Programming in Guru"
• MMT language and system

See also: Every proof assistant series of lectures.

Coq

Coq is an interactive theorem prover and proof assistant based on an intensional intuitionistic type theory -- the Calculus of Inductive Constructions (CIC). It is a dependently-typed -calculus and (by the Curry-Howard isomorphism) an intuitionistic higher-order logic. It is written in OCaml.

Model checkers

• SPIN
• DIVINE parallel, distributed-memory explicit-state LTL checker
• UPPAAL
• TLA+
• NuSMV symbolic model checker
• Ultimate Automizer model checker based on an automata approach
• LTSmin language-agnostic
• PRISM probabilistic model checker
• MMC explicit-state model checker for -calculus
• CBMC bounded model checking
• ESBMC context-bounded model checking
• Nidhugg

SAT & SMT solvers

• MiniSat
• PicoSAT
• Z3
• CVC4
• CVC5
• Alt-Ergo (academic page)
• Yices (non-free licence)
• MathSAT 5
• Boolector
• Lingeling, Plingeling and Treengeling
• CryptoMiniSat 2
• CaDiCaL
• SONOLAR Solver for Non-Linear Arithmetic
• ABC "A System for Sequential Synthesis and Verification"
• Vampire
• zChaff
• funsat "a modern DPLL-style SAT solver" written in Haskell
• versat
  • D. Oe, A. Stump, C. Oliver, K. Clancy: "versat: A Verified Modern SAT Solver" (2011)
• "Simple SMT solver for use in an optimizing compiler"
• SAT Competitions
• Configurable SAT Solver Challenge (CSSC) 2014
• Model Checking Contest (MCC)

Other tools

• Why3 platform for deductive reasoning on programs with support for many external provers
  • Gallery of verified programs
  • "Shepherd Your Herd of Provers" (2011)
• Alloy "a language and tool for relational models"
• Boogie intermediate verification language
• Q Program Verifier collection of tools for a sourceIRIVL translation and subsequent verification
  • SMACK bounded verification via LLVM to Boogie translation
• Dafny "a language and program verifier for functional correctness"
• Vienna Verification Toolkit
• CSeq
• IKOS "library designed to facilitate the development of sound static analyzers based on Abstract Interpretation"
• Crab "language agnostic engine to perform static analysis based on abstract interpretation"
• Seahorn "fully automated verification framework for LLVM-based languages"
• rise4fun a collection of numerous tools, i.a. for program and algorithm analysis and verification, by Microsoft Research, CMU and others that you can try right on the web page
• Profound "an experiment in subformula linking as an interaction method"
  • K. Chaudhuri: "Subformula Linking as an Interaction Method" (2013)
• SE "A Platform for In-Vivo Analysis of Software Systems"
• KLEE symbolic execution VM
• CPAchecker
• Ultimate
• K Framework
• Lem

Formal methods in practice

• Muen Separation Kernel first open-source kernel verified for absence of runtime errors (Reddit discussion)
• CertiKOS "advanced development of certified OS kernels"
• Galois, Inc.
• Software Systems Research Group (SSRG) at NICTA tons of exciting projects
  • seL4 first fully verified and open-sourced OS kernel
  • Cogent cogeneration of proofs and C code in Isabelle

Learning resources

Courses, textbooks, papers, theses, competitions, influential figures in the field.

• The QED Manifesto, some more details here

• Formalizing 100 Theorems

• Verified Software Competition

• VerifyThis a competition and collection of problems in formal verification of algorithms and software

• Competition on Software Verification (SV-COMP)

• Oregon Programming Languages Summer School video recordings of awesome lectures on type theory, provers, logic, etc.; earlier editions only have lecture notes and slides published

  2016, 2015, 2014, 2013, 2012, 2011, 2010, 2009, 2008, 2007, 2006, 2005

• Type Theory Study Group 2015

Type theory

Danny Gratzer's learn-tt is a fantastic resource for those interested in type and category theory. He presents all the terrific tools, textbooks, and papers that deal with both of these in a sensible and logical way, which is a quality that my repository will never have.

I'll only list here resources which he doesn't mention and which I personally find interesting.

Check out the TYPES mailing list as well.

Dependent types

• C. McBride: Epigram: Practical Programming with Dependent Types (2010)
• A. Bove, P. Dybjer: Dependent Types at Work introduction to programming with dependent types in Agda

Observational Type Theory

• T. Altenkirch, C. McBride: "Towards Observational Type Theory" (2006)
• F. Mazzoli: "Bertus: Implementing Observational Equality" (2013)

Univalent Foundations and Homotopy Type Theory

• P. Aczel: "On Voevodsky's Univalence Axiom" (2011; slides)

Cubical Type Theory

• M. Bezen, T. Coquand, S. Huber: "A model of type theory in cubical sets" (2014)
• D. Licata: "A Cubical Type Theory" (2014; slides)
• A. Kaposi, T. Altenkirch: "A syntax for cubical type theory" (2014; slides)
• T. Coquand: "A Cubical Type Theory" (2015; slides)
• T. Coquand: "A cubical type theory" (2015; slides)
• C. Cohen, T. Coquand, S. Huber, A. Mrtberg: "Cubical Type Theory: a constructive interpretation of the univalence axiom" (2016)
  • mortberg/cubicaltt a Haskell implementation of the type theory presented in this paper

Copyright

Written in 20152020 by Matj Grabovsk

This work is licensed under a Creative Commons Attribution 4.0 International License.