Skip to content

Opus 4.7 uses Apalache to search for inductive invariant candidates, then proves main theorem with TLAPS#212

Merged
lemmy merged 22 commits into
masterfrom
mku-tlaips_tcp
May 13, 2026
Merged

Opus 4.7 uses Apalache to search for inductive invariant candidates, then proves main theorem with TLAPS#212
lemmy merged 22 commits into
masterfrom
mku-tlaips_tcp

Commits

Commits on May 13, 2026