Experiment with Claude Opus 4.7 and TLAPS.#211

Open

lemmy wants to merge 29 commits intomasterfrom

mku-tlaips

Commits on Apr 26, 2026

Proof subset of EWD687a theorems

authored and
lemmy
committed
ewd687a: prove DT1FromInv2 (Spec => []DT1Inv now complete)

lemmy
and
claude
committed
docs: add PROOF_DIFFICULTY.md ranking unproved theorems by difficulty

lemmy
and
claude
committed
SpecifyingSystems: TLAPS proof of HourClock HCini invariant

lemmy
and
claude
committed
SpecifyingSystems: TLAPS proofs of Channel and AsynchInterface TypeInvariant

lemmy
and
claude
committed
SpecifyingSystems: TLAPS proof of InternalMemory TypeInvariant

lemmy
and
claude
committed
SpecifyingSystems: TLAPS proofs of AlternatingBit and InnerFIFO TypeInvariant

lemmy
and
claude
committed
byihive: TLAPS proof of VoucherLifeCycle TypeOK and Consistent

lemmy
and
claude
committed
transaction_commit: TLAPS proofs of TCommit, TwoPhase, PaxosCommit invariants

lemmy
and
claude
committed
KeyValueStore: TLAPS proof of TypeInvariant and TxLifecycle

lemmy
and
claude
committed
Name the previously-anonymous ASSUMEs in PaxosCommit and EWD687a

lemmy
and
claude
committed
Reuse Inv in three Spec => [](TypeOK /\ Safety) theorem statements

lemmy
and
claude
committed
docs: PROOF_DIFFICULTY.md - mark three Paxos M-band proofs done

lemmy
and
claude
committed
PaxosHowToWinATuringAward: TLAPS proofs of Voting AllSafeAtZero, ChoosableThm, ShowsSafety

lemmy
and
claude
committed
allocator/SimpleAllocator: TLAPS proofs of TypeInvariant and ResourceMutex

lemmy
and
claude
committed
allocator/SchedulingAllocator: TLAPS proofs of TypeInvariant and ResourceMutex

lemmy
and
claude
committed
allocator/AllocatorImplementation: TLAPS proof of TypeInvariant

lemmy
and
claude
committed
docs: PROOF_DIFFICULTY.md - mark third-round M-band proofs done

lemmy
and
claude
committed
transaction_commit/TwoPhase: TLAPS proof of []TC!TCConsistent (Band M)

lemmy
and
claude
committed
MisraReachability: name unnamed companion theorems and add PartialCorrectnessThm

lemmy
and
claude
committed
ewd687a: drop TypeOK/Counters from Inv2 and simplify proof structure

lemmy
and
claude
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Experiment with Claude Opus 4.7 and TLAPS.#211

Experiment with Claude Opus 4.7 and TLAPS.#211
lemmy wants to merge 29 commits intomasterfrom
mku-tlaips

Commits on Apr 26, 2026

Proof subset of EWD687a theorems

ewd687a: prove DT1FromInv2 (Spec => []DT1Inv now complete)

docs: add PROOF_DIFFICULTY.md ranking unproved theorems by difficulty

SpecifyingSystems: TLAPS proof of HourClock HCini invariant

SpecifyingSystems: TLAPS proofs of Channel and AsynchInterface TypeInvariant

SpecifyingSystems: TLAPS proof of InternalMemory TypeInvariant

SpecifyingSystems: TLAPS proofs of AlternatingBit and InnerFIFO TypeInvariant

byihive: TLAPS proof of VoucherLifeCycle TypeOK and Consistent

transaction_commit: TLAPS proofs of TCommit, TwoPhase, PaxosCommit invariants

KeyValueStore: TLAPS proof of TypeInvariant and TxLifecycle

Name the previously-anonymous ASSUMEs in PaxosCommit and EWD687a

Reuse Inv in three Spec => [](TypeOK /\ Safety) theorem statements

docs: PROOF_DIFFICULTY.md - mark three Paxos M-band proofs done

PaxosHowToWinATuringAward: TLAPS proofs of Voting AllSafeAtZero, ChoosableThm, ShowsSafety

allocator/SimpleAllocator: TLAPS proofs of TypeInvariant and ResourceMutex

allocator/SchedulingAllocator: TLAPS proofs of TypeInvariant and ResourceMutex

allocator/AllocatorImplementation: TLAPS proof of TypeInvariant

docs: PROOF_DIFFICULTY.md - mark third-round M-band proofs done

transaction_commit/TwoPhase: TLAPS proof of []TC!TCConsistent (Band M)

MisraReachability: name unnamed companion theorems and add PartialCorrectnessThm

ewd687a: drop TypeOK/Counters from Inv2 and simplify proof structure

Commits on Apr 27, 2026

transaction_commit/PaxosCommit: TLAPS proof of []PCTypeOK

SpecifyingSystems: simplify LosePreservesType in AlternatingBit proof

TwoPhase: split TLAPS proof into TwoPhase_proof module

ewd998: move RECURSIVE SimpleCycle from Utils.tla to EWD998_anim.tla

ewd998/EWD998PCal: TLAPS proof of Init refinement and []PCalTypeOK

MultiCarElevator: TLAPS proof of Spec => []TypeInvariant

MultiCarElevator: SafetyInvariant scaffold + Init proof

docs: PROOF_DIFFICULTY.md - mark MultiCarElevator partial