Peterson’s algorithm in Lean
A source-guided study of Gary L. Peterson’s mutual exclusion algorithms, with Lean models and proofs for two-process and finite n-process constructions.
Safety and progress have different assumptions. The interactive exploration introduces those boundaries and links to a fixed source revision.