Door Verification

Small Lean example showing an implementation checked against a specification.

The specification has two visible states:

closed --opened--> open
open   --closed--> closed

The implementation has extra internal states:

closed --τ--> opening --opened--> open
open   --τ--> closing --closed--> closed

Lean checks that the implementation preserves the specification's visible behavior, allowing silent τ steps.

Run:

lake build

Main file:

Door.lean