Repository navigation

EWD840 and EWD998 proofs rely on tlapm soundness bug - #250

Merged

lemmy merged 5 commits into

Oct 30, 2026

Merged

EWD840 and EWD998 proofs rely on tlapm soundness bug#250
lemmy merged 5 commits into
masterfrom
mku-gh69

Commits on Oct 30, 2026
- CI: run Apalache from the TLAPS library directory.
  
  lemmy
  and
  claude
  committed
  2781401
- EWD840: extend TLAPS to work around a tlapm bug.
  
  lemmy
  and
  claude
  committed
  ab4979e
- EWD840_proof: do not rely on instantiation distributing over WF.
  
  committed
  affe258
- EWD998: extend TLAPS to work around a tlapm bug.
  
  lemmy
  and
  claude
  committed
  61973f6
- EWD998_proof: do not rely on instantiation distributing over WF.
  
  committed
  8e320b3