Specify and verify the system with TLA+

[losfair]

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