Neat! I worked on a similar formal verification of Ghostferry, which is a zero downtime data migration tool that powers the shard balancing tool at Shopify, also using TLA+:
I also was able to find an concrrency bug before a single line of code was written with the TLC which saved a lot of time. It took about 4 weeks to design and verify the system in spec and about 2 weeks to write the initial code version, which mostly survived to this day and reasonably resembles the TLA+ spec. To my knowledge (I no longer work there) the correctness of the system was never violated and it never had any sort of data corruption. Would be a much harder feat without TLA+.
Neat! I worked on a similar formal verification of Ghostferry, which is a zero downtime data migration tool that powers the shard balancing tool at Shopify, also using TLA+:
https://github.com/Shopify/ghostferry/blob/main/tlaplus/ghos...
I also was able to find an concrrency bug before a single line of code was written with the TLC which saved a lot of time. It took about 4 weeks to design and verify the system in spec and about 2 weeks to write the initial code version, which mostly survived to this day and reasonably resembles the TLA+ spec. To my knowledge (I no longer work there) the correctness of the system was never violated and it never had any sort of data corruption. Would be a much harder feat without TLA+.