This repository contains a bunch of interesting and useful tools, materials, and many other stuffs that help one with doing verification with Coq.

Resources for noobs who have never ever played with Coq.

• Inria - Official Reference Manual
• Inria - Standard Library
• Coq-cheatsheet
• Software Foundations: This book is just fantastic: it teaches you how to write correct code and prove it in Coq. It gives rise to basic PL stuffs like verification techniques and types.
• VSCoq: Extension for VS Code.

Till now, you should be able to verify something non-trivial...

• Ltac / Ltac2
• Ltac2 Tutorial
• Mathematical Components: Mathematical Components is the name of a library of formalized mathematics for the Coq proof assistants.
• Verified C Compiler
• Coq formalization for Haskell
• Extraction from Coq to OCaml
• Coq Tricks: All the things that Coq manual won't teach you.
• Dependent Types: This manual teaches you how to write code in Coq for playing with dependent types like $\Pi_{n: \mathbb{N}} P(n)$
• Coq's "Standard Library": This project contains an extended "Standard Library" for Coq called coq-std++.

• ConCert: Verified Smart Contract Implementation
• CIFC: Oakland'21 Enforcing information flow control for Java-like language
• YNOT and this: Verifying a database
• Jasmin: Writing secure cryptographic code

You probably won't like them...

• Homotopy Type Theory for Coq
• MetaCoq: You can even play with Coq's core calculus and AST!
• UniMath: This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
• Category Theory: Formalized category theory in Coq.
• MathClasses
• Iris: A general proof mode for carrying out separation logic proofs (proof for languages that allow programmers to play with memory stores; for those interested, please refer to JC Reynolds's paper at CMU) in Coq.
• More dependent types and some HoTT

• Ralf Jung @ ETHz: He is also the core contributor of rust-lang.
• Tej Chajed: Proofs, logics, and verification for systems.
• Inria: People at this institute made Coq!