Two VeriFIT victories at SMT-COMP 2026: Z3-Noodler and Amaya

How can we determine which software tool is best at tackling complex logical and mathematical problems? SMT-COMP, a prestigious international competition, seeks to answer this question by testing the capabilities of so-called SMT solvers (Satisfiability Modulo Theories) – programmes used, for example, in automated proof, analysis and formal verification of software – on various types of tasks each year. Using sets of challenging problems, the competition tests not only whether they can find the correct solution, but also how quickly and efficiently they can tackle the problem.

An SMT solver can also be described as a tool that automatically determines whether a complex logical statement—composed, for example, of arithmetic, text or other common elements—can be true. And if it is true, it finds an example that proves it. SMT solvers are used, for example, to verify that safety-critical software does not contain serious errors; to check that the code cannot be circumvented by malicious input; to prove that optimisations in the compiler do not alter the programme’s behaviour; and to automatically generate test cases for a given piece of code.

At this year’s SMT-COMP, researchers from FIT VUT achieved significant success. Two tools developed by the faculty’s research group VeriFIT took part in the competition: Z3-Noodler and Amaya. The results listed below relate to the main competition category, the Single Query Track.

Z3-Noodler

Z3-Noodler is an extension of the well-known automata-based SMT solver Z3. The tool is designed to handle so-called string (text) constraints – that is, constraints used, for example, when checking whether a web application securely validates user input, or when considering resource access policies. Competing against solvers deployed in the cloud security industry, Z3-Noodler won the QF_Strings division in all evaluated categories: overall performance, parallel performance, and performance on both positive and negative decision tasks. At the same time, it was more than an order of magnitude faster in total solution time than the second-best solver, OSTRICH. And that is precisely the difference that matters in practical applications. Furthermore, Z3-Noodler was recognised for making the greatest unique contribution in this division, as it solved problems that none of the other participating solvers could handle.

Z3-Noodler is being developed by Vojtěch Havlena, Juraj Síč, David Chocholatý, Lukáš Holík, Ondřej Lengál, Michal Hečko and Michal Šedý from the VeriFIT research group, together with students Marek Effenberger, Jan Hranička, Ondřej Koumar, Jakub Ráček, Michal Šebesta and Martin Valluš, who contributed to the tool as part of their bachelor’s or master’s theses or project placements. The success of Z3-Noodler builds on the group’s long-term research into decision procedures for automaton-based string constraints.

Amaya

Amaya is a solver for linear integer arithmetic formulas with unrestricted quantifiers. For example, when analysing computer systems, such formulas can describe the system’s state (remaining energy, speed, available resources, number of queued tasks, etc.) and the rules governing how these values change. It is then possible to investigate, for example, whether certain requirements hold for all possible cases of the system’s execution or whether there is a way to control the system to ensure they are met.

Such formulas find application in areas such as the formal analysis and synthesis of both software and hardware systems. Amaya solves them in an unusual way: instead of the algebraic methods used by most existing solvers, it utilises techniques from automata theory. It translates arithmetic conditions into descriptions of sets of possible states and analyses their properties using automata. As a research prototype, Amaya is not yet optimised to match, in every respect, the raw speed of mature, thoroughly engineered solvers such as Z3.

Amaya was declared the winner of the official SMT-COMP ‘Largest Contribution Ranking’ – that is, an award covering the entire competition, not limited to a single division – based on two evaluation criteria (sequential and parallel performance). This award is given to the tool that solves the largest proportion of tasks that no other solver can solve. Amaya’s automata-based approach enables it to succeed precisely in those problems where conventional algebraic solvers reach their limits. This is also a direct result of research by the VeriFIT group, which focuses on the combination of automata theory and algebraic reasoning in arithmetic.

Amaya is being developed by Vojtěch Havlena, Michal Hečko, Lukáš Holík and Ondřej Lengál. The project builds on the group’s paper from the CAV’24 conference, “Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic”.

The full results are available on the official SMT-COMP 2026 results page.

We congratulate the members of the VeriFIT research group on their continued success on the international stage.