The results of the 2026 edition of SYNTCOMP are in. We first list the leaders of the parity-game, LTL, and finite-word LTL tracks. We then give the detailed running times, scores, and plots, followed by the participating tools and the developments that will shape SYNTCOMP from 2026 onward.
The data below comes from the 2026 TGCC jobs. The complete result artifact, including the data and plots used here, is archived on Zenodo. The selected benchmarks are available from the SYNTCOMP benchmark repository. Congratulations to the leading tools, and thanks to every participant and benchmark contributor!
The winners
Parity-game realizability
- Realizability: Knor (477 of 483 instances)
LTL realizability
- Realizability: SemML (1397 of 1524 instances)
LTL synthesis
- Synthesis time/coverage: SemML, using
semml_fast(1248 of 1505 instances; tied for maximum coverage and fastest among the tied configurations) - Synthesis quality: SemML, using
semml_small(mean quality score 1.911; maximum possible score 2)
LTLf realizability
- Realizability: ltlfsynt (402 of 488 instances;
bfs-osanddfs-ostie)
Parity-game realizability
Knor reaches near-complete coverage: each of its four submitted configurations solves 477 of the 483 instances. The strahler-knor configuration reaches that coverage in about 360 seconds of cumulative wall-clock time.
| Solver | Configuration | Solved | Wall-clock time (s) | CPU time (s) | Memory |
|---|---|---|---|---|---|
| Knor | strahler-knor | 477 | 360 | 335 | 39,775 |
| Knor | npp | 477 | 3,751 | 3,694 | 62,283 |
| Knor | tl | 477 | 410 | 371 | 64,992 |
| Knor | tlq | 477 | 4,459 | 4,397 | 66,748 |
| ltlsynt | default | 417 | 56,332 | 55,951 | 15,028 |
LTL realizability
SemML leads this track with 1397 solved instances, 45 more than the Strix legacy baseline. It also has the lowest cumulative wall-clock time among the configurations solving more than 1300 instances.
| Solver | Configuration | Solved | Wall-clock time (s) | CPU time (s) | Memory |
|---|---|---|---|---|---|
| Acacia-Bonsai | ios-mona | 986 | 77,933 | 186,005 | 729,343 |
| Acacia-Bonsai | decomp-kdtree | 1,015 | 106,506 | 249,623 | 733,627 |
| Acacia-Bonsai | decomp-mona | 1,023 | 83,304 | 194,076 | 733,819 |
| Acacia-Bonsai | sharingtrie | 972 | 83,995 | 200,805 | 1,560,395 |
| ltlsynt | acd | 1,341 | 56,855 | 56,374 | 436,759 |
| ltlsynt | ds | 1,246 | 222,130 | 220,850 | 1,305,808 |
| ltlsynt | lar | 1,339 | 58,267 | 57,767 | 403,366 |
| SemML | default | 1,397 | 54,180 | 92,167 | 3,601,670 |
| Strix | legacy | 1,352 | 88,017 | 87,271 | 1,726,900 |
LTL synthesis
semml_fast and Strix legacy each solve 1248 instances. At equal coverage, semml_fast uses about 30.9 ks of cumulative wall-clock time, compared with 68.4 ks for Strix legacy. For quality, semml_small obtains the highest mean score, 1.911 out of 2, while solving 1240 instances: only eight fewer than the maximum coverage.
| Solver | Configuration | Solved | Wall-clock time (s) | CPU time (s) | Memory | Mean quality |
|---|---|---|---|---|---|---|
| SemML | fast | 1,248 | 30,914 | 53,809 | 2,544,440 | 1.699 |
| SemML | small | 1,240 | 32,868 | 59,313 | 2,766,660 | 1.911 |
| Strix | legacy | 1,248 | 68,384 | 67,697 | 1,309,047 | 1.862 |
| ltlsynt | acd | 1,234 | 36,105 | 35,726 | 287,024 | 1.438 |
| ltlsynt | lar | 1,232 | 47,789 | 47,336 | 294,647 | 1.411 |
| ltlsynt | ds | 1,134 | 104,000 | 103,246 | 556,569 | 1.534 |
LTLf realizability
The bfs-os and dfs-os configurations of ltlfsynt tie at 402 solved instances. The two Cosy configurations are retained in the table for completeness, but they were marked as disqualified in the supplied results and are excluded from the ranking.
| Solver | Configuration | Solved | Wall-clock time (s) | CPU time (s) | Memory |
|---|---|---|---|---|---|
| ltlfsynt | bfs-os | 402 | 26,740 | 26,543 | 119,230 |
| ltlfsynt | bfs | 393 | 29,163 | 28,883 | 129,401 |
| ltlfsynt | dfs-os | 402 | 26,950 | 26,751 | 118,655 |
| Cosy | m1 (DISQUALIFIED) | 367 | 8,068 | 7,978 | 147,286 |
| Cosy | m2 (DISQUALIFIED) | 366 | 10,137 | 10,061 | 146,889 |
| LydiaSyft | LydiaSynt | 316 | 15,796 | 15,663 | 47,721 |
What is new from 2026 onward?
A precise stopping semantics for LTLf synthesis
The finite-trace synthesis semantics now makes explicit who ends the trace and how. The controller owns a fresh output signal, AliveSig: value 1 keeps the execution alive, and the first 0 terminates it. The controller must eventually terminate every infinite input stream. The shortest terminating trace, after projecting away AliveSig, must satisfy the LTLf specification. TLSF v1.2 also distinguishes finite Mealy and Moore semantics explicitly; X[!] denotes strong next, while plain X is weak next. See the TLSF v1.2 paper.
A new alternative to syfco
tlsf-tools provides small Unix-style tools for reading and expanding TLSF 1.1/1.2 specifications. In particular, tlsf2ltl translates parameterized TLSF into solver-facing LTL. It is an alternative to the relevant functionality of syfco, not a new or incompatible specification format.
The SYNTCOMP mailing list
Calls, solver and benchmark updates, evaluation notices, and result announcements now have a persistent community channel. Subscribe to the SYNTCOMP mailing list. The rolling evaluation setup remains in place: improved tools and benchmarks can be submitted for reruns and updated rankings.
Solvers
Below are source-code, license, and citation links for the participating solver families.
| Solver | Source repository | License | Report(s) to cite |
|---|---|---|---|
| ltl(f)synt | Spot GitLab repository | GPL-3.0+ | ltlsynt paper; ltlfsynt report |
| Acacia-Bonsai | GitHub repository | GPL-3.0 | Paper |
| Knor | GitHub repository | GPL-3.0 | Paper |
| Knor (Strahler) | GitHub repository | GPL-3.0 | EMSOFT WiP letter (to appear) |
| SemML | GitLab repository | GPL-3.0 | Paper |
| Strix | GitLab repository | AGPL-3.0 | Paper |
| Cosy | TBA | TBA | Contact the authors |
We welcome new benchmarks, solvers, and model checkers. Send them whenever they are ready, and subscribe to the mailing list to follow future reruns and announcements.