This repo contains OneBit algorithm from Chapter 4 from A Science of Concurrent Programming formalized in rocq. It uses coq-tla library as underlying TLA embedding in rocq.
Supported Coq version: 8.18.0.
git submodule update --init --recursive
make
Safety property (safety_theorem) is formalizaed. Liveness property is work-in-progress.