The PAC Checkers, Pacheck and Pastèque

This page provides access to the source code, benchmarks, and experiments.

The goal of Pacheck and Pastèque is to provide a checker for PAC proofs with extensions. The former provides an efficient implementation, while the latter provides maximal trust as it verified using the proof assistant Isabelle/HOL.


2020: First release of Pacheck (available here) and Pastèque (available here).


For Pacheck, ensure GMP (on linux, use your package manager) is installed and use ``./ && make''.

For Pasteque, ensure MLton is installed and use ``make''.


A small set of examples is available here

Experimental Data

[ KaufmannFleuryBiere-FMCAD20-data.tar.xz ] experimental data (21.8 MB)