Star Fork Issue

Cosette is an automated prover for checking equivalences of SQL queries. It formalizes a substantial fragment of SQL in the Coq Proof Assistant and the Rosette symbolic virtual machine. It returns either a formal proof of equivalance or a counterexample for a pair of given queries.

We will release Cosette in next few weeks.
Stay tuned and sign up on our mailing list

Checking SQL Equivalences in Cosette

You can try the Cosette demo online, or download its source code from github.

Screenshot of the cosette web UI

Cosette Web UI (click image above to visit demo website)

How does Cosette work?

Cosette compiles input queries to constraints over symbolic relations and calls Rosette to find counterexamples, which are input tables that the two input queries return different answer. Cosette also compiles input queries into expressions of K-relations, UniNomials we call, which are mathematical functions that returns multiplicity of tuples, using Coq with Homotopy Type Theory. Cosette then tries to search a Coq proof of equivalence of the two input queries given any valid input data. The architecture of Cosette is shown as below:

Cosette Architecture

Cosette System Architecture



If you have any questions, want to contribute to the project, or just want to say hi, email us at


Cosette is developed by the Database Group and the Programming Languages and Software Engineering Group at the University of Washington, the main contributors are:

Shumo Chu

Konstantin Weitz

Chenglong Wang

Daniel Li

Alvin Cheung

Dan Suciu