Protocol Conformance with Choreographic PlusCal.

Distributed protocols, an essential part of modern computing infrastructure, are well-known to be difficult to implement correctly. While lightweight formal methods such as TLA + can be effectively used to verify abstract protocols, end-to-end validation of real-world protocol implementations remains challenging due to their complexity. To address this problem, we extend the TLA + toolset along two fronts. We propose several extensions to PlusCal – an algorithm language which compiles to TLA + – to allow writing distributed protocols as choreographies. This enables more structured and succinct specifications for role-based protocols. We also provide a methodology and toolchain for compiling TLA + models into monitors, allowing them to be used to test existing systems for conformance. The result is a lightweight testing method that bridges specification and implementation. We demonstrate its benefits with case studies of both classic and recent protocols and show it to be readily applicable to existing systems with low runtime overhead.