Solving Concurrency with (In-)formal Methods in Servo

Servo is a Web engine, and one of its goal is parallelism, which creates challenges related to concurrency which aren’t covered by the Rust compiler. TLA plus is a mathematical language for modelling concurrent algorithms, making it a useful tool to improve the correctness of Servo. Recent and practical use cases will be discussed in this talk.