The automatic theorem prover Vampire, developed under the leadership of Martin Suda – head of the Automated Reasoning Group at CIIRC CTU and a tenure track holder in RICAIP – achieved a remarkable success this year. At the 30th edition of the CADE ATP System Competition (CASC) 2025, it became the first system in history to win all eight competition categories – an unprecedented feat in the field.
The CASC-30 competition, held on July 30, 2025, in Stuttgart, was an exceptional event for Vampire. Not only did it defend its previous year’s victory, but this time it became the first prover ever to win every single one of the eight official divisions, including the reinstated Effectively Propositional CNF category, which returned to the competition after a five-year hiatus.
Significant performance gains were particularly evident in the categories focused on arithmetic reasoning (Typed First-order Theorems +-/) and equality reasoning (Unit Equality CNF), where optimizations developed in collaboration with colleagues from TU Wien – especially Márton Hajdu – played a crucial role. The outstanding result is the product of systematic preparation, newly developed proving strateges, and close cooperation among developers from several European institutions.
Search for strategies led by Martin Suda
Martin Suda, head of the Automated Reasoning Group at CIIRC CTU, was for the second time responsible for preparing the so-called strategy portfolio – a key component of the competition. Each problem in CASC must be solved using a limited number of pre-defined strategies that should collectively cover a broad range of difficult cases while complementing each other.
“Preparing a strategy portfolio is a bit like planning a chess tournament – each strategy plays the role of a different grandmaster and needs to fit into the overall tactics. This year, we managed to build a lineup that could handle all kinds of problems,”
says Martin Suda, Head of the Automated Reasoning Group at CIIRC CTU.
In the next development phase, the Vampire team plans to integrate machine learning techniques, expanding its strategic toolkit with neural network-guided approaches.
“Our goal for next year is to integrate neural-guided strategies into Vampire. We’ve been working on this for several years, and we’re finally starting to see real results,”
adds Suda.
Who’s behind the Vampire theorem prover?
The development of Vampire is driven by an international team of researchers from several leading European universities. This collaboration brings together experts in logic, formal verification, software engineering, and machine learning, enabling Vampire to stay at the forefront of global research.
The core team includes:
- Martin Suda, Filip Bártek, Petra Hozzová (CIIRC CTU)
- Ahmed Bhayat, Giles Reger, Andrei Voronkov (University of Manchester)
- Laura Kovács, Márton Hajdu, Matthias Hetzenberger, Jakob Rath, Robin Coutelier, Johannes Schoisswohl (TU Wien)
- Michael Rawson (University of Southampton)
More international recognition – “The Vampire Diary” wins distinguished paper award
2025 was a banner year for the Vampire team not only in competitions. At the prestigious CAV 2025 conference, the team received the Distinguished Paper Award for their paper The Vampire Diary, which chronicles the development of the prover over the past ten years.
About CASC and the CADE conference
The CADE ATP System Competition (CASC) is an annual international competition in automated theorem proving, held as part of the CADE (Conference on Automated Deduction) or IJCAR conferences. It is considered the world championship for automated reasoning systems in classical logic.
The competition aims to objectively compare the performance of different systems. Evaluation is primarily based on the number of problems correctly solved within a fixed time limit (typically 3 to 5 minutes), as well as the quality and completeness of the solutions. CASC also serves as a driver for research, the development of robust tools, and a platform for knowledge exchange within the expert community.
The 30th edition of CASC, CASC-30, took place on July 30, 2025, in Stuttgart, as part of the jubilee CADE-30 conference, held from July 28 to August 2, 2025. The competition was organized, as traditionally, by Dr. Geoff Sutcliffe (University of Miami). An independent jury – Aart Middeldorp, Cláudia Nalon, and Tjark Weber – ensured fairness and transparency throughout the event.
