On: How SQLite is tested

[cwzwarich]

There are no automatically provable invariants that would cover SQLite's functionality. How does a tool automatically prove that a query compiler is correct, for example? I don't see an easy way, barring writing SQLite in Coq.