Confluence Competition

FLoC Olympic Games

This year CoCo was part of the FLoC Olympics. The CoCo Progress Award went to CONFident for solving the most problems tagged as interesting, counted across all categories; a problem is tagged as interesting if there is at least one year where the problem was scheduled during a full run and no tool was able to solve it. The CoCo Secret Problem Award went to infChecker, this year's participant that solved the most problems tagged as secret problem in previous editions of CoCo, counted across all categories.

CoCo 2026 Results

Combined Yes and No Results

category 1st place 2nd place 3rd place
COM FORT-h CeTA-Prover
CSR CONFident
CTRS CONFident CO3
GCR FORT-h
INF infChecker nonreach+CeTA-Prover Natto
LCTRS crest CRaris
NFP CSI FORT-h
SRS CSI CONFident CeTA-Prover
TRS CSI Hakusan AProVE
UNC CSI FORT-h
UNR CSI FORT-h

Yes Results

category 1st place 2nd place 3rd place
COM CeTA-Prover FORT-h
CSR CONFident
CTRS CONFident CO3
GCR FORT-h
INF infChecker Natto nonreach+CeTA-Prover
LCTRS crest CRaris
NFP CSI FORT-h
SRS CSI CONFident CeTA-Prover
TRS CSI Hakusan AProVE
UNC CSI FORT-h
UNR CSI FORT-h

No Results

category 1st place 2nd place 3rd place
COM FORT-h
CSR CONFident
CTRS CO3 CONFident
GCR FORT-h
INF infChecker nonreach+CeTA-Prover
LCTRS crest CRaris
NFP CSI FORT-h
SRS CSI CONFident
TRS Hakusan CSI CONFident
UNC CSI FORT-h
UNR CSI FORT-h

Detailed results are available. The same holds for the LiveView of CoCo 2026 upon completion.

Certification Results

category 1st place 2nd place 3rd place
CERTIFICATION CeTA FORTify
RELIABILITY FORT-h CSI CeTA-Prover

In the CERTIFICATION category, certifiers are ranked based on the number of certificates that are validated. In the RELIABILITY category, tools are ranked based on the number of generated certified proofs.


Problem Selection

The problems were selected using the following ARI-COPS queries. Here s is the number 401 composed of the three random digits 4 (Thiago Felicissimo), 0 (Keisuke Nakano), 1 (Vincent van Oostrom) provided by the panel members.


categories   queries
COM 1630 or 1631
limit:98,s 1..1628 2trs
CSR limit:100,s 1..1628 {cstrs or csctrs}
CTRS limit:100,s 1..1628 ctrs type3 oriented
GCR limit:100,s 1..1628 !srs {trs or mstrs}
INF 1635 or 1636
limit:98,s 1..1628 infeasibility
LCTRS limit:100,s 1..1628 lctrs
NFP limit:100,s 1..1628 trs !CR:YES
SRS limit:100,s 1..1628 srs
TRS 1629 or 1632 or 1633 or 1634 or 1637 or 1638
limit:94,s 1..1628 trs !srs
UNC limit:100,s 1..1628 trs !CR:YES
UNR limit:100,s 1..1628 trs !CR:YES