Coq – formal proof management system

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, the Verified Software Toolchain for verification of C programs, or the Iris framework for concurrent separation logic), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem, or homotopy type theory), and teaching.

Users generate proofs by entering a series of tactics that constitute steps in the proof. There are many built-in tactics, some of which are elementary, while others implement complex decision procedures (such as lia, a decision procedure for linear integer arithmetic). Ltac and its planned replacement, Ltac2, provide languages to define new tactics by combining existing tactics with looping and conditional constructs. These permit automation of large parts of proofs and sometimes entire proofs. Furthermore, users can add novel tactics or functionality by creating Coq plugins using OCaml.

The Coq kernel, a small part of Coq, does the final verification that the tactic-generated proof is valid. Usually the tactic-generated proof is indeed correct, but delegating proof verification to the kernel means that even if a tactic is buggy, it won’t be able to introduce an incorrect proof into the system.

Finally, Coq also supports extraction of verified programs to programming languages such as OCaml and Haskell. This provides a way of executing Coq code efficiently and can be used to create verified software libraries.

Website: coq.inria.fr
Support: Documentation, GitHub Code Repository
Developer: INRIA Formel, Coq, LogiCal, ProVal, TypiCal, Marelle, pi.r2, Ascola, Galinette projects (starting 1985),- Laboratoire de l’Informatique du Parallelisme (LIP)
associated to CNRS and ENS Lyon (Sep. 1989 to Aug. 1997), Laboratoire de Recherche en Informatique (LRI) associated to CNRS and university Paris Sud (since Sep. 1997), Laboratoire d’Informatique de l’Ecole Polytechnique (LIX) associated to CNRS and Ecole Polytechnique (since Jan. 2003). Laboratoire PPS associated to CNRS and University Paris Diderot
License: GNU Lesser General Public License v2.1

Coq is written in OCaml and Coq. Learn OCaml with our recommended free books and free tutorials.

Return to Proof Assistants Home Page


Popular series
Guide to LinuxNew to Linux? Read our Linux for Starters series. We start right at the basics and teach you everything you need to know to get started with Linux.
Free and Open Source SoftwareThe largest compilation of the best free and open source software in the universe. Each article is supplied with a legendary ratings chart helping you to make informed decisions.
ReviewsHundreds of in-depth reviews offering our unbiased and expert opinion on software. We offer helpful and impartial information.
Alternatives to Proprietary SoftwareReplace proprietary software with open source alternatives: Google, Microsoft, Apple, Adobe, IBM, Autodesk, Oracle, Atlassian, Corel, Cisco, Intuit, and SAS.
Linux Around The WorldLinux Around The World showcases events and usergroups that are relevant to Linux enthusiasts.
AudioSurveys popular streaming services from a Linux perspective: Amazon Music Unlimited, Myuzi, Spotify, Deezer, Tidal.
Saving Money with LinuxSaving Money with Linux looks at how you can reduce your energy bills running Linux.
System ToolsEssential Linux system tools focuses on small, indispensable utilities, useful for system administrators as well as regular users.
ProductivityLinux utilities to maximise your productivity. Small, indispensable tools, useful for anyone running a Linux machine.
Home ComputersHome computers became commonplace in the 1980s. Emulate home computers including the Commodore 64, Amiga, Atari ST, ZX81, Amstrad CPC, and ZX Spectrum.
Now and ThenNow and Then examines how promising open source software fared over the years. It can be a bumpy ride.
Linux at HomeLinux at Home looks at a range of home activities where Linux can play its part, making the most of our time at home, keeping active and engaged.
Linux CandyLinux Candy reveals the lighter side of Linux. Have some fun and escape from the daily drudgery.
DockerGetting Started with Docker helps you master Docker, a set of platform as a service products that delivers software in packages called containers.
Android AppsBest Free Android Apps. We showcase free Android apps that are definitely worth downloading. There's a strict eligibility criteria for inclusion in this series.
Programming BooksThese best free books accelerate your learning of every programming language. Learn a new language today!
Programming TutorialsThese free tutorials offer the perfect tonic to our free programming books series.
Stars and StripesStars and Stripes is an occasional series looking at the impact of Linux in the USA.
Share this article

Share your Thoughts

This site uses Akismet to reduce spam. Learn how your comment data is processed.