Thanks a lot! So far, we have considered only systems that are (partially) available in the open. Two of these are mainly developed commercially, namely CockroachDB and TiDB. We are glad that Cockroach Labs and PingCAP were indeed quite thankful for our testing efforts (e.g., see https://twitter.com/JordanALewis/status/1249689838686818304 for CockroachDB and https://twitter.com/PingCAP/status/1260678075714600968 for TiDB).

We will also consider testing DBMS with a DeWitt Clause in the future. For now, we have indirect evidence that our approaches could find bugs in Oracle. Specifically, we found a case in MySQL, which we consider a bug, but which was closed by the bug verifiers, partly because Oracle computes the same - we believe incorrect - result. Our bug report can be found here: https://bugs.mysql.com/bug.php?id=99182.

We believe that it is a bug, because:

* the invariants that we are testing using TLP, which is the approach that we used to find the bug, should hold for all DBMS;

* dropping the UNIQUE constraint would yield the result we would expect, and we believe that an index should never affect a query's result;

* an earlier version of MySQL computed the result we would expect;

* and DBMS that strive to support the MySQL SQL dialect, computed the result we would expect (e.g., TiDB).