Q*cert - overview
Q*cert is a query compiler written using the Coq proof assistant and a platform for implementing and verifying query compilers.
Data processing is central to modern applications, and guaranteeing the correctness of consistency of the data is important. Q*cert leverages recent advances in theorem proving technology to provide correctness guarantees for the query compiler, including its optimizers.
Q*cert is an open-source project, and its source code and documentation is available on github at https://querycert.github.io