Vampire Retains Overall Title at CASC 2026
The CADE ATP System Competition (CASC) is the annual world championship for fully automated theorem-proving systems in classical logic. It provides a rigorous public evaluation of automated theorem provers by comparing the number of benchmark problems they solve within defined time limits, the quality of the generated solutions, and their average solving time. Beyond measuring performance, CASC advances automated reasoning by encouraging research and system development, promoting robust and deployable tools, strengthening collaboration within the ATP community, and increasing awareness of automated theorem-proving technology beyond academia. The competition organizer is Geoff Sutcliffe. The competition is overseen by an independent panel of expert researchers. The 2026 edition of CASC was held as part of the FLoC Olympics at the 13th International Joint Conference on Automated Reasoning (IJCAR 2026) in Lisbon, Portugal, from 26 to 29 July 2026, within the Federated Logic Conference 2026 (FLoC 2026).
At this year’s competition, the theorem prover Vampire, developed by the FORSYTE Research Unit under the leadership of Laura Kovács, successfully defended its championship title. After making history in 2025 as the first automated theorem prover to win every competition division, Vampire repeated the achievement in 2026 by once again taking first place in all eight theorem-proving divisions.
Automated theorem provers are essential to formal verification, software and hardware assurance, cybersecurity, trustworthy artificial intelligence, and the automation of mathematics. By analysing logical statements and proving or disproving them through formal methods, these systems help establish the correctness of complex software, hardware, and AI-based systems.
Vampire is developed at TU Wien in close collaboration with the University of Manchester, the University of Southampton, and the Czech Technical University in Prague. Over more than a decade of continuous development, it has evolved into one of the world’s most advanced automated theorem provers, incorporating methods for saturation-based theorem proving, higher-order reasoning, induction, arithmetic, and AI-assisted proof search. Its consecutive clean sweeps at CASC demonstrate both its broad reasoning capabilities and its sustained international leadership.
Further reading: Paper on the Vampire theorem prover
The FORSYTE team received further recognition through VaLeaDate, a proof-verification system developed by Jonas Bodingbauer. VaLeaDate received the Most Valuable Benchmark Contributor award in its competition category. It verifies proofs written in the TPTP format by reconstructing individual inference steps with the Vampire theorem prover and combining them into complete proof files that are subsequently checked end to end in Lean. Before launching the computationally intensive verification process, VaLeaDate performs several structural checks, including confirming that all parent nodes exist, ensuring that the proof graph is acyclic, and verifying that the axioms correspond to the original problem input up to alpha-equivalence. It then processes the proof inferences in parallel with Vampire, handles skolemization, reconstructs the resulting proof, and submits the complete output to Lean for independent verification. Depending on the outcome, the system reports the proof as VerifiedGood, VerifiedBad, or Unknown.
At IJCAR 2026, Márton Hajdu, Petra Hozzová, Laura Kovács, and Eva Maria Wagner presented “Completeness of Synthesis Under Realizability Assumptions Using Superposition.” The paper introduces SUPRA, a refined superposition-based calculus for automatically synthesizing recursion-free programs from formal specifications, including specifications that contain uncomputable symbols. By combining automated theorem proving with program synthesis, the approach supports the construction of programs whose correctness follows directly from the proof process.
SUPRA extends earlier saturation-based synthesis methods with abstract unification, constrained clauses, dedicated simplification orders, and selection functions that prioritize uncomputable literals. These changes allow the calculus to reason about such literals without violating its computability requirements. The authors prove that SUPRA is sound and complete under a realizability assumption: whenever at least one computable program satisfying the specification exists, the calculus is guaranteed to derive one. The work strengthens the theoretical foundations of correct-by-construction software synthesis and provides a basis for future research on recursive program synthesis using induction.