Skip to content

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

Open
lemmy wants to merge 21 commits into
masterfrom
mku-tlaips_tcp
Open

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

Commits

Commits on May 12, 2026