技术博文:为沙箱设计经过形式化验证的分布式锁地址：scotthao.com/writing/distributed-locks

“我在 Modal 的实习即将结束。在这里，我参与了全新、可大规模扩展的沙箱架构建设，其中大部分时间都用来开发名为 “names” 的沙箱分布式锁原语。取得一个名称相当于取得一把锁，只不过沙箱会一直保留这个名称，直到自身终止。

事实证明，正确实现分布式系统非常困难。在不同假设下，有些目标甚至可以被证明无法实现。我不止一次重新设计 names：有时是遗漏了竞态，有时是需求发生变化，还有时是某项决定给下游带来了意外影响。最后，我开始学习 TLA+，用这种建立在时序逻辑之上的建模语言，对系统性质进行形式化验证。

本文将介绍沙箱名称机制背后的设计与验证过程。这也是作者的第一篇博客文章，希望它既有信息量，也足够有趣”