Checkers is a λ-prolog implementation of a tool for checking proofs output by theorem provers. It is based on the theory of foundational proof certificates.  Currently it has support for checking some of the proofs from classical resolution and several modal theorem provers.

The University of Luxembourg and the Laboratory of Informatics of the École polytechnique are currently investigating ways to use Checkers as a proof assistant for various modal logics.

Main contributor(s): Tomer Libal, Leon van der Torre