Explore the Rocq Documentation

For newcomers interested in programming languages, the Software Foundations series is an excellent introduction to using the Rocq Prover for formal verification.

For newcomers with a background in mathematics rather than computer science, this book is an introduction to the Rocq Prover and to the SSReflect proof language used in the Mathematical Components library. Accustomed Rocq users will find a substantial account of the formalization style that made the Mathematical Components library possible.

The primary audience of the manuscript are the readers with expertise in software development and programming and knowledge of discrete mathematic disciplines on the level of an undergraduate university program. The high-level goal of the course is, therefore, to demonstrate how much the rigorous mathematical reasoning and development of robust and intellectually manageable programs have in common, and how understanding of common programming language concepts provides a solid background for building mathematical abstractions and proving theorems formally. The low-level goal of this course is to provide an overview of the Rocq Prover, taken in its both incarnations: as an expressive functional programming language with dependent types and as a proof assistant providing support for mechanized interactive theorem proving.

This textbook is a foundational book that introduces readers to the Rocq Prover and its underlying formal system, the Calculus of Inductive Constructions (CIC). The book provides a comprehensive guide to interactive theorem proving, combining theory with practical applications. It covers key concepts such as inductive types, recursive functions, and proof construction, while offering numerous examples and case studies, including the formalization of algorithms and mathematical proofs. Coq'Art serves as both an introduction for beginners and a reference for experts, making it an essential resource for anyone working with Rocq or exploring formal methods.

Verified Functional Algorithms shows how a variety of fundamental data structures can be specified and mechanically verified.

Formal Reasoning About Programs (FRAP) is a book that provides a general introduction to formal logical reasoning about the correctness of programs and to using Rocq for this purpose. The main narrative of FRAP presents standard program-proof ideas, without rigorous proofs. Matching Rocq code then show how to make it rigorous. Interleaved with that narrative, there are also other lectures' worth of material, for building up more practical background on Rocq itself.

Certified Programming with Dependent Types (CPDT) is a hands-on guide to advanced programming and proving using the Rocq Prover. The book focuses on leveraging Roqc’s dependent type system to write certified programs, where correctness is formally verified alongside implementation. It introduces key concepts such as inductive types, type theory, proof automation, and advanced tactics, providing a blend of theoretical foundations and practical examples. CPDT is particularly known for its focus on proof engineering and building large-scale verified systems efficiently. Aimed at readers with some prior exposure to Rocq, it serves as an invaluable resource for those looking to master the interplay between programming and formal verification.

Floating-point arithmetic is ubiquitous in modern computing, as it is the tool of choice to approximate real numbers. Due to its limited range and precision, its use can become quite involved and potentially lead to numerous failures. One way to greatly increase confidence in floating-point software is by computer-assisted verification of its correctness proofs. This book provides a comprehensive view of how to formally specify and verify tricky floating-point algorithms with the Coq proof assistant. It describes the Flocq formalization of floating-point arithmetic and some methods to automate theorem proofs. It then presents the specification and verification of various algorithms, from error-free transformations to a numerical scheme for a partial differential equation. The examples cover not only mathematical algorithms but also C programs as well as issues related to compilation.