The Ukrainian Catholic University (UCU) is establishing the Center of Excellence for Formal Methods and Verification—a new academic and applied research hub that will combine cutting-edge research, education of the next generation of specialists, and collaboration with the technology industry. The Center will advance formal methods and their applications in mathematics, computer science, and artificial intelligence.
The Center was officially presented on July 24 during the International Congress of Mathematicians (ICM 2026)—the world’s largest and most prestigious mathematics conference, held every four years and hosted this year in Philadelphia, USA.
The presentation took place during the roundtable discussion “Building Ukraine’s Future in Mathematics: Center of Excellence for Formal Methods and Verification at UCU.” Participants discussed the Center’s vision and the transformative role of artificial intelligence in mathematics, theorem proving, and higher education.
The discussion featured David Spergel, Co-Chair of the Science and Innovation Fund for Ukraine Council and President of the Simons Foundation, and Jeremy Avigad, Director of the Hoskinson Center for Formal Mathematics at Carnegie Mellon University.
David Spergel is a distinguished American astrophysicist, Professor Emeritus at Princeton University, and one of today’s leading scientific figures. As President of the Simons Foundation, he oversees global funding strategies for breakthrough research shaping the future of fundamental mathematics, theoretical physics, and computational sciences.
Professor Jeremy Avigad is one of the world’s leading experts in formalized mathematics and interactive theorem proving. His work has made major contributions to the adoption of the Lean proof assistant and programming language for the formal verification of mathematical knowledge and AI research.
Formal Methods and Verification
Formal verification is a mathematically rigorous approach to proving that software, algorithms, protocols, or mathematical proofs are correct. For decades, the field remained largely academic because constructing formal proofs required substantial human effort and time, even for relatively small problems.
Artificial intelligence is rapidly changing this landscape. Modern language models are already capable of generating source code, mathematical reasoning, and potential solutions to complex problems. At the same time, formal verification systems—most notably the Lean proof assistant and its ecosystem—can automatically verify the correctness of such outputs against precisely defined formal rules.
This creates new opportunities not only for fundamental mathematics but also for critical real-world applications, including software verification, communication protocols, smart contracts, networked systems, and AI-enabled technologies—any domain where errors may have significant consequences.
UCU’s Position in the Field
The Faculty of Applied Sciences at the Ukrainian Catholic University has developed strong expertise at the intersection of mathematics, computer science, and artificial intelligence. Research at the faculty spans algorithms, data analysis, machine learning, mathematical modeling, and reliable software engineering, while faculty members actively participate in international research projects and collaborate with universities and industry partners worldwide.
The establishment of the Center of Excellence for Formal Methods and Verification represents a natural continuation of these efforts. The Center will integrate research in proof theory, formal systems, and the mathematical foundations of programming with educational initiatives and applied research addressing challenges relevant to today’s technology industry.
The Center’s activities will develop along three interconnected directions.
Education
The educational program will include student seminars, a certificate program, and university courses ranging from the fundamentals of Lean and formal logic to software verification and AI system verification.
Research
The research agenda will cover formalized mathematics, set theory, geometry, proof theory, and formal methods in computer science. The Center also plans to organize research seminars, international summer schools, and host visiting scholars and lecturers.
Industry Collaboration
The applied direction will focus on industrial applications of formal verification. The Center aims to build partnerships with technology companies through joint research projects, educational initiatives, and collaboration on practical challenges related to the security and reliability of digital systems.
The Center’s Academic Director will be Oleksii Ignatenko, Professor at UCU, Doctor of Physical and Mathematical Sciences, and researcher specializing in game theory, machine learning, and complex systems.
Oleksii Ihnatenko
The establishment of the Center has been made possible through a grant from the Science and Innovation Fund for Ukraine, founded by the U.S. National Academy of Sciences. The Fund supports Ukraine’s scientific community and the development of a long-term innovation ecosystem built on research excellence, international collaboration, and commercialization of scientific results.
“Mathematical proofs have always been the foundation of reliable knowledge. Today, as artificial intelligence generates increasingly sophisticated reasoning and solutions for critical systems, a new challenge emerges: verifying their correctness with mathematical rigor. It is precisely at the intersection of mathematics, computer science, and artificial intelligence that we are building this new Center at UCU,” said Yaroslav Prytula, Senior Vice Rector of the Ukrainian Catholic University.
Yaroslav Prytula
“At the Science and Innovation Fund for Ukraine, we believe that strengthening science is essential to Ukraine’s long-term future. The launch of this Center reflects our commitment to building sustainable scientific capacity, fostering international collaboration, and supporting Ukrainian leadership in an important and rapidly evolving field. We look forward to seeing the Center become a catalyst for innovation and partnership in Ukraine and beyond,” said Vaughan Turekian, Executive Director of the Office of International Affairs, Partnerships, and Security at the U.S. National Academies of Sciences, Engineering, and Medicine.
David Spergel, Co-Chair of the Science and Innovation Fund for Ukraine Council and President of the Simons Foundation, emphasized the Foundation’s commitment to supporting mathematics and the natural sciences worldwide.
“At the beginning of Russia’s full-scale invasion, our focus was on supporting scientists who had become refugees. As it became clear that many researchers wanted to remain in Ukraine, our mission evolved. We needed to address the risk of brain drain by supporting scientists where they are and providing opportunities for them to continue their work. The UCU Summer School in Data Science was among the first steps in that direction.
David Spergel
During my visits to Lviv, Kyiv, and Kharkiv last year, I witnessed an extraordinary determination to rebuild and innovate. Lviv, in particular, has the potential to become a European hub for innovation and a natural gathering place for the global formal methods community.
The International Congress of Mathematicians marks a turning point. Four years ago, artificial intelligence was barely part of the mathematical conversation. Four years from now, the field will look entirely different. It is remarkable that Ukraine has the opportunity to become a global leader in this emerging area from the very beginning.”
The Center welcomes collaboration with Ukrainian and international universities, research institutions, technology companies, researchers, and educators working in formal methods, the mathematical foundations of computer science, reliable software engineering, and artificial intelligence.
The Center also seeks to engage researchers and faculty members interested in developing new research directions, designing educational programs, co-supervising undergraduate and graduate research, and launching international and industry partnerships. Those interested in collaborating are encouraged to contact the Center through its application form or by reaching out directly to the Center’s Director.
