Comment Comment by jhhh There was a post recently using TLA to model this issue and (re)discover the bug: https://news.ycombinator.com/item?id=48730953. parent jhhh 2 months ago
