Zero-Downtime Database Migration Verified with PlusCal

This blog post details how the author used PlusCal, a DSL for TLA+, and formal verification to ensure the correctness of a zero-downtime database migration. A PlusCal model was built simulating user Upsert, Delete, and Get operations on a database, along with a background migration process. By simulating a system without migration and one with migration, and verifying the consistency of Get operation results across all states, the author ensured the correctness of the migration algorithm. Formal verification helped in early detection of flaws, such as improper handling of TOMBSTONES, and highlighted the importance of atomic operations, like the atomicity of checking and inserting data during migration.