A WhyML library for reasoning about state machine specifications and
distributed systems. This is V2 of the
why3-do library: the same
inductive-invariant and specification-refinement methodology, with
proof management moved from Why3 proof sessions to
why3find. The repo carries the
why3find proof certificates (proof.json) alongside every example,
recording which prover or tactic combination closes each goal, so
the whole library replays with a single command and no interactive
sessions are required.
The methodology is described in:
- Cláudio Belo Lourenço and Jorge Sousa Pinto. Auto-active verification of distributed systems and specification refinements with Why3-do. Science of Computer Programming, 247, 2026.
- Cláudio Belo Lourenço and Jorge Sousa Pinto. Why3-do: The Way of Harmonious Distributed System Proofs. ESOP 2022, LNCS 13240.
Relative to V1, the networkModels library is gone: network
semantics are no longer a separate theory, but are modeled
per-example as refinement layers over an abstract machine -- see the
channel layers LamportNet.mlw, RicartAgrawalaNet.mlw and
raftNet.mlw, which refine fused send/receive steps into explicit
messages in flight.
| Folder | Description |
|---|---|
| stateMachineModels/ | Base library (inductive invariants, refinement) |
| examples/counter/ | Concurrent counter using a lock, by refinement |
| examples/twoPhase/ | Two-phase handshake protocol, by refinement |
| examples/mutualExclusionConcurrent/ | Concurrent mutual exclusion (Peterson, Bakery, filter) |
| examples/mutualExclusionDistributed/ | Distributed mutual exclusion (Lamport, Ricart-Agrawala, Suzuki-Kasami) |
| examples/mutualExclusionNeighbors/ | Dijkstra self-stabilizing ring and bidirectional array (neighbor communication), delivering mutual exclusion via tokenMutex |
| examples/leaderElection/ | Chang-Roberts and Bully leader election, by refinement |
| examples/dynamicBully/ | Dynamic Bully leader election with crash/recovery |
| examples/waitFreeRegister/ | Simpson's 4-slot wait-free register, by refinement |
| examples/paxosNoRefinement/ | Paxos consensus (stand-alone, no refinement) |
| examples/paxos/ | Paxos consensus, two-step refinement |
| examples/raft/ | Raft leader election, three-step refinement chain |
| examples/controlledFlooding/ | Controlled flooding broadcast |
| examples/spanningTree/ | DIM self-stabilizing spanning tree (stable phase, closure property) |
Cross-file dependencies in why3find are resolved through installed
packages, not folder loadpaths. Every .mlw file is registered as a
why3find package by setup.sh, so cross-file use and clone
references resolve through the installed packages. See why3find.json
for the full package list.
Requires Why3 1.8+,
why3find 1.3+, and at least one SMT
prover (CVC5, Alt-Ergo, Z3). See why3find.json for the exact prover
versions and tactics used.
eval $(opam env)
./setup.sh # install packages from repo sources (run once)
why3find prove -r . # replay all proofswhy3find prove . # update proof certificates
why3find prove -r . # replay proofs (no changes)
why3find prove -f . # force rebuild all proofs
why3find prove -i file.mlw # launch Why3 IDE on failed goals
why3find prove --goals . # per-goal breakdownEach .mlw file has a matching proof.json certificate in a
subdirectory of the same name (e.g. counter.mlw -> counter/proof.json).
These are JSON files recording which prover (or tactic + prover
combination) closes each goal. The .why3find/ cache directory is
gitignored.