QuickChick/QuickChick
Randomized Property-Based Testing Plugin for Coq
{ "createdAt": "2014-04-03T22:36:19Z", "defaultBranch": "master", "description": "Randomized Property-Based Testing Plugin for Coq", "fullName": "QuickChick/QuickChick", "homepage": "", "language": "Rocq Prover", "name": "QuickChick", "pushedAt": "2025-11-23T21:27:26Z", "stargazersCount": 276, "topics": [ "coq", "testing" ], "updatedAt": "2025-11-23T21:27:31Z", "url": "https://github.com/QuickChick/QuickChick"}QuickChick
Section titled “QuickChick”
Description
Section titled “Description”- Randomized property-based testing plugin for Coq; a clone of [Haskell QuickCheck]
- Includes a [foundational verification framework for testing code]
- Includes a [mechanism for automatically deriving generators for inductive relations]
[Haskell QuickCheck] !: https://hackage.haskell.org/package/QuickCheck
[foundational verification framework for testing code] !: http://prosecco.gforge.inria.fr/personal/hritcu/publications/foundational-pbt.pdf
[mechanism for automatically deriving generators for inductive relations] !: https://lemonidas.github.io/pdf/GeneratingGoodGenerators.pdf
Tutorial
Section titled “Tutorial”- Small tutorials on Basic Usage and Automation can be found under
tutorials/ - An extended introduction can be found in [QuickChick: Property-Based Testing in Coq][sfqc] (Software Foundations, Volume 4)
[sfqc] !: https://softwarefoundations.cis.upenn.edu/qc-current/index.html
Installation
Section titled “Installation”From OPAM
Section titled “From OPAM”# Add the Coq opam repository (if you haven't already)opam repo add coq-released https://coq.inria.fr/opam/releasedopam update# Install the coq-quickchick opam packageopam install coq-quickchickSimple Examples
Section titled “Simple Examples”examples/Tutorial.vexamples/RedBlackexamples/stlcexamples/ifc-basic
Running make tests in the top-level QuickChick folder will check and execute all of these.
If successful, you should see “success” at the end.
Documentation
Section titled “Documentation”The public API of QuickChick is summarized in QuickChickInterface.v.
Top-level Commands
Section titled “Top-level Commands”QuickCheck cSample gDerive Arbitrary for cDerive Show for cDerive ArbitrarySizedSuchThat for (fun x => p)Derive DecOpt for pDerive EnumSizedSuchThat for (fun x => p)Derive ArbitrarySizedSuchThat for (fun x => let (x1,x2...) := x in p)QuickCheckWith args cMutateCheck c pMutateCheckWith args c pMutateCheckMany c psMutateCheckManyWith args c ps
More resources
Section titled “More resources”Here is some more reading material:
- Our PLDI 2022 paper on a mechanism for automatically deriving generators, enumerators, and checkers for inductive relations
- Our POPL 2018 paper on a mechanism for automatically deriving generators for inductive relations
- Our ITP 2015 paper on Foundational Property-Based Testing
- Our PLDI 2023 paper on a mechanism for merging multiple inductive relations into one
- Leo’s invited talk at CLA on Random Testing in the Coq Proof Assistant
- Catalin’s internship topic proposals for 2015
- Catalin’s presentation at CoqPL 2015 workshop (2015-01-18)
- Zoe’s thesis defense at NTU Athens (2014-09-08)
- Maxime’s presentation at the Coq Workshop (2014-07-18)
- Catalin’s presentation at the Coq Working Group @ PPS (2014-03-19)
Developer’s corner
Section titled “Developer’s corner”Build dependencies
Section titled “Build dependencies”Dependencies are listed in [coq-quickchick.opam]!(./coq-quickchick.opam).
# To get the dependencies, add the Coq opam repository if you haven't alreadyopam repo add coq-released https://coq.inria.fr/opam/releasedopam updateopam install . --deps-onlydune buildRun tests
Section titled “Run tests”dune runtestRun extra tests for quickChick tool
Section titled “Run extra tests for quickChick tool”dune install coq-quickchick # Makes QuickChick available globallydune build @cram