Formal Methods in Practice: Using TLA+ at eSpark Learning
How do we harden a system against race conditions? When it uses a complex cache? When it requires a global state? We could blanket our system in tests, hope we’ve covered every possible edge case, and pray that nothing new happens…