The ProoVer Competition is an annual competition for proof checkers.

Inspired by the CADE ATP System Competition (CASC), ProoVer aims to benchmark the correctness and robustness of proof checkers within the TPTP ecosystem.

Participants submit both correct and “buggy” proofs, and their systems must determine the validity of each proof. Contestants are required to implement a proof checker that can call an external prover for some steps, while verifying specific proof steps internally within their tool.