Toward a Verified Relational Database Management SystemMalecha, Morrisett, Shinnar & Wisnesky present a verified RDBMS formalized in Coq, covering the relational model, SQL compiler/execution engine, and B+ tree implementation with separation logic.research-paperdatabasesformal-methodscoq