The theorem prover Vampire, developed at TU Wien Informatics, won every competition category at the international CADE ATP System Competition (CASC) for the second consecutive year on July 27, 2026. In addition, the new AI system VaLeaDate won the Most Valuable Benchmark Contributor in its category.

Whether in software verification or artificial intelligence, automated theorem provers are essential wherever the correctness of complex systems must be established through mathematical proof. They can automatically analyze logical statements and prove or disprove them using formal methods, providing a crucial foundation for secure software, trustworthy AI, and formal verification.

With Vampire, the FORSYTE Research Unit, led by Laura Kovács in close collaboration with the University of Manchester, the University of Southampton, and the Czech Technical University in Prague, has developed one of the world’s most powerful automated theorem provers. The system has once again demonstrated its international leadership, winning the competition by a wide margin — just as it did last year.

Alongside this competition success, the team also introduced a new AI system. Together with UnAxiMa and PhD student Jonas Bodingbauer, the researchers developed VaLeaDate, a tool for evaluating and validating automatically generated proofs. The system received the Most Trustworthy Prover award, setting a new benchmark for trustworthy AI-assisted theorem proving.

In addition to FORSYTE’s achievements, TU Wien was also recognized for developing the best proof checker, GAPT. Developed by Fabian Achammer, Martin Riener, and Stefan Herzl, this success highlights the outstanding collaboration between TU Wien’s Faculties of Informatics and Mathematics and Geoinformation.

Dean of TU Wien Informatics Gerti Kappel congratulated the team: “These repeated successes demonstrate once again that cutting-edge research at TU Wien sets international standards. Automated Reasoning is a key technology for secure software, trustworthy AI, and a wide range of scientific applications. I warmly congratulate the entire team on these outstanding achievements and am delighted to see TU Wien Informatics further strengthening its international leadership in this forward-looking field.”

Such world-class research would not be possible without sustained investment. This success demonstrates the impact of combining outstanding research with modern research infrastructure. A key contribution came from Research Software Engineer Márton Hajdu, who transforms the latest research advances into highly optimized software. Equally important is TU Wien’s Automated Reasoning Computing Cluster, which provides the computational power required for large-scale local reasoning tasks.

Laura Kovács: “This achievement demonstrates how essential the combination of excellent fundamental research and state-of-the-art research infrastructure is, especially at the intersection of mathematics and computer science. This success is also thanks to our colleagues in the Faculty of Mathematics and Geoinformation. Together, we have once again shown that TU Wien is among the world’s leading institutions for logic, automated reasoning, and formal methods.”

Curious about our other news? Subscribe to our news feed, calendar, or newsletter, or follow us on social media.