mvSQLite has stacked a lot of logic on top of FoundationDB. The *design* of these logic should be verified for correctness. Some specific subsystems that would benefit from verification: - The commit path - Garbage collection