Volume 1 Logical Foundations: serves as the entry-point to the series. It covers functional programming, basic concepts of logic, computer-assisted theorem proving,and Coq.

Volume 2 Programming Language Foundations: surveys the theory of programming languages, including operational semantics, Hoare logic, and static type systems.

Volume 3 Verified Functional Algorithms: shows how a variety of fundamental data structures can be mechanically verified.

Volume 4 QuickChick: Property-Based Testing in Coq introduces tools and techniques for combining randomized property-based testing with formal specification and proof in the Coq ecosystem.