Skip to content

Experiment with Claude Opus 4.7 and TLAPS. #211

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
lemmy wants to merge 29 commits into
base: master
Choose a base branch
from
Open

Experiment with Claude Opus 4.7 and TLAPS. #211

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
29 commits
Select commit Hold shift + click to select a range
81ef2fc
Proof subset of EWD687a theorems
Apr 23, 2026
fa37a36
ewd687a: prove DT1FromInv2 (Spec => []DT1Inv now complete)
lemmy Apr 23, 2026
e95971b
docs: add PROOF_DIFFICULTY.md ranking unproved theorems by difficulty
lemmy Apr 24, 2026
e702adf
SpecifyingSystems: TLAPS proof of HourClock HCini invariant
lemmy Apr 24, 2026
f04ab3a
SpecifyingSystems: TLAPS proofs of Channel and AsynchInterface TypeIn…
lemmy Apr 24, 2026
c392cc5
SpecifyingSystems: TLAPS proof of InternalMemory TypeInvariant
lemmy Apr 24, 2026
5b66239
SpecifyingSystems: TLAPS proofs of AlternatingBit and InnerFIFO TypeI…
lemmy Apr 24, 2026
b771a0d
byihive: TLAPS proof of VoucherLifeCycle TypeOK and Consistent
lemmy Apr 24, 2026
d280cac
transaction_commit: TLAPS proofs of TCommit, TwoPhase, PaxosCommit in…
lemmy Apr 24, 2026
7cfd223
KeyValueStore: TLAPS proof of TypeInvariant and TxLifecycle
lemmy Apr 24, 2026
a4939b2
Name the previously-anonymous ASSUMEs in PaxosCommit and EWD687a
lemmy Apr 26, 2026
2e0c6e6
Reuse Inv in three Spec => [](TypeOK /\ Safety) theorem statements
lemmy Apr 26, 2026
dd0cadb
docs: PROOF_DIFFICULTY.md - mark three Paxos M-band proofs done
lemmy Apr 26, 2026
ca6338e
PaxosHowToWinATuringAward: TLAPS proofs of Voting AllSafeAtZero, Choo…
lemmy Apr 26, 2026
a68e60e
allocator/SimpleAllocator: TLAPS proofs of TypeInvariant and Resource…
lemmy Apr 26, 2026
0961d00
allocator/SchedulingAllocator: TLAPS proofs of TypeInvariant and Reso…
lemmy Apr 26, 2026
2b51555
allocator/AllocatorImplementation: TLAPS proof of TypeInvariant
lemmy Apr 26, 2026
fc2bef3
docs: PROOF_DIFFICULTY.md - mark third-round M-band proofs done
lemmy Apr 26, 2026
2ade526
transaction_commit/TwoPhase: TLAPS proof of []TC!TCConsistent (Band M)
lemmy Apr 26, 2026
ef4ecd3
MisraReachability: name unnamed companion theorems and add PartialCor…
lemmy Apr 26, 2026
893baae
ewd687a: drop TypeOK/Counters from Inv2 and simplify proof structure
lemmy Apr 26, 2026
61963bc
transaction_commit/PaxosCommit: TLAPS proof of []PCTypeOK
lemmy Apr 27, 2026
eaf3459
SpecifyingSystems: simplify LosePreservesType in AlternatingBit proof
lemmy Apr 27, 2026
100e1b0
TwoPhase: split TLAPS proof into TwoPhase_proof module
lemmy Apr 27, 2026
60a475e
ewd998: move RECURSIVE SimpleCycle from Utils.tla to EWD998_anim.tla
lemmy Apr 27, 2026
6f1ec2f
ewd998/EWD998PCal: TLAPS proof of Init refinement and []PCalTypeOK
lemmy Apr 27, 2026
9233964
MultiCarElevator: TLAPS proof of Spec => []TypeInvariant
lemmy Apr 27, 2026
beb5d26
MultiCarElevator: SafetyInvariant scaffold + Init proof
lemmy Apr 27, 2026
c94e899
docs: PROOF_DIFFICULTY.md - mark MultiCarElevator partial
lemmy Apr 27, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
350 changes: 350 additions & 0 deletions PROOF_DIFFICULTY.md
View file
Open in desktop

Large diffs are not rendered by default.

14 changes: 7 additions & 7 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,12 +38,12 @@ Here is a list of specs included in this repository which are validated by the C
| [The Die Hard Problem](specifications/DieHard) | Leslie Lamport | ✔ | | | ✔ | ✔ |
| [The Prisoners & Switches Puzzle](specifications/Prisoners) | Leslie Lamport | ✔ | | | ✔ | |
| [The Prisoners & Switch Puzzle](specifications/Prisoners_Single_Switch) | Florian Schanda | ✔ | | | ✔ | |
| [Specs from Specifying Systems](specifications/SpecifyingSystems) | Leslie Lamport | ✔ | | | ✔ | ✔ |
| [Specs from Specifying Systems](specifications/SpecifyingSystems) | Leslie Lamport | ✔ | (✔) | | ✔ | ✔ |
| [The Tower of Hanoi Puzzle](specifications/tower_of_hanoi) | Markus Kuppe, Alexander Niederbühl | ✔ | | | ✔ | |
| [Missionaries and Cannibals](specifications/MissionariesAndCannibals) | Leslie Lamport | ✔ | | | ✔ | ✔ |
| [Stone Scale Puzzle](specifications/Stones) | Leslie Lamport | ✔ | | | ✔ | |
| [The Coffee Can Bean Problem](specifications/CoffeeCan) | Andrew Helwer | ✔ | | | ✔ | ✔ |
| [EWD687a: Detecting Termination in Distributed Computations](specifications/ewd687a) | Stephan Merz, Leslie Lamport, Markus Kuppe | ✔ | | (✔) | ✔ | |
| [EWD687a: Detecting Termination in Distributed Computations](specifications/ewd687a) | Stephan Merz, Leslie Lamport, Markus Kuppe | ✔ | ✔ | (✔) | ✔ | |
| [The Moving Cat Puzzle](specifications/Moving_Cat_Puzzle) | Florian Schanda | ✔ | | | ✔ | ✔ |
| [The Boulangerie Algorithm](specifications/Bakery-Boulangerie) | Leslie Lamport, Stephan Merz | | ✔ | ✔ | ✔ | |
| [Misra Reachability Algorithm](specifications/MisraReachability) | Leslie Lamport | | ✔ | ✔ | ✔ | ✔ |
Expand All @@ -61,14 +61,14 @@ Here is a list of specs included in this repository which are validated by the C
| [Dijkstra's Mutual Exclusion Algorithm](specifications/dijkstra-mutex) | Leslie Lamport | | | ✔ | ✔ | |
| [The Echo Algorithm](specifications/echo) | Stephan Merz | | | ✔ | ✔ | |
| [The TLC Safety Checking Algorithm](specifications/TLC) | Markus Kuppe | | | ✔ | ✔ | |
| [Transaction Commit Models](specifications/transaction_commit) | Leslie Lamport, Jim Gray, Murat Demirbas | | | ✔ | ✔ | ✔ |
| [Transaction Commit Models](specifications/transaction_commit) | Leslie Lamport, Jim Gray, Murat Demirbas | | (✔) | ✔ | ✔ | ✔ |
| [The Slush Protocol](specifications/SlushProtocol) | Andrew Helwer | | | ✔ | ✔ | |
| [Minimal Circular Substring](specifications/LeastCircularSubstring) | Andrew Helwer | | | ✔ | ✔ | |
| [Snapshot Key-Value Store](specifications/KeyValueStore) | Andrew Helwer, Murat Demirbas | | | ✔ | ✔ | |
| [Snapshot Key-Value Store](specifications/KeyValueStore) | Andrew Helwer, Murat Demirbas | | ✔ | ✔ | ✔ | |
| [Chang-Roberts Algorithm for Leader Election in a Ring](specifications/chang_roberts) | Stephan Merz | | | ✔ | ✔ | ✔ |
| [MultiPaxos in SMR-Style](specifications/MultiPaxos-SMR) | Guanzhou Hu | | | ✔ | ✔ | |
| [Einstein's Riddle](specifications/EinsteinRiddle) | Isaac DeFrain, Giuliano Losa | | | | | ✔ |
| [Resource Allocator](specifications/allocator) | Stephan Merz | | | | ✔ | |
| [Resource Allocator](specifications/allocator) | Stephan Merz | | (✔) | | ✔ | |
| [Transitive Closure](specifications/TransitiveClosure) | Stephan Merz | | | | ✔ | |
| [Atomic Commitment Protocol](specifications/acp) | Stephan Merz | | | | ✔ | ✔ |
| [SWMR Shared Memory Disk Paxos](specifications/diskpaxos) | Leslie Lamport, Giuliano Losa | | | | ✔ | |
Expand All @@ -81,7 +81,7 @@ Here is a list of specs included in this repository which are validated by the C
| [Software-Defined Perimeter](specifications/SDP_Verification) | Luming Dong, Zhi Niu | | | | ✔ | |
| [Simplified Fast Paxos](specifications/SimplifiedFastPaxos) | Lim Ngian Xin Terry, Gaurav Gandhi | | | | ✔ | |
| [Checkpoint Coordination](specifications/CheckpointCoordination) | Andrew Helwer | | | | ✔ | |
| [Multi-Car Elevator System](specifications/MultiCarElevator) | Andrew Helwer | | | | ✔ | |
| [Multi-Car Elevator System](specifications/MultiCarElevator) | Andrew Helwer | | ✔ | | ✔ | |
| [Nano Blockchain Protocol](specifications/NanoBlockchain) | Andrew Helwer | | | | ✔ | |
| [The Readers-Writers Problem](specifications/ReadersWriters) | Isaac DeFrain | | | | ✔ | ✔ |
| [Asynchronous Byzantine Consensus](specifications/aba-asyn-byz) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | |
Expand All @@ -97,7 +97,7 @@ Here is a list of specs included in this repository which are validated by the C
| [Conway's Game of Life](specifications/GameOfLife) | Mariusz Ryndzionek | | | | ✔ | |
| [Chameneos, a Concurrency Game](specifications/Chameneos) | Mariusz Ryndzionek | | | | ✔ | |
| [PCR Testing for Snippets of DNA](specifications/glowingRaccoon) | Martin Harrison | | | | ✔ | ✔ |
| [RFC 3506: Voucher Transaction System](specifications/byihive) | Santhosh Raju, Cherry G. Mathew, Fransisca Andriani | | | | ✔ | |
| [RFC 3506: Voucher Transaction System](specifications/byihive) | Santhosh Raju, Cherry G. Mathew, Fransisca Andriani | | (✔) | | ✔ | |
| [Yo-Yo Leader Election](specifications/YoYo) | Ludovic Yvoz, Stephan Merz | | | | ✔ | |
| [TCP as defined in RFC 9293](specifications/tcp) | Markus Kuppe | | | | ✔ | ✔ |
| [B-trees](specifications/btree) | Lorin Hochstein | | | | ✔ | |
Expand Down
43 changes: 43 additions & 0 deletions specifications/KeyValueStore/KeyValueStore_proof.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
------------------------- MODULE KeyValueStore_proof -----------------------
(***************************************************************************)
(* TLAPS proof of *)
(* THEOREM Spec => [](TypeInvariant /\ TxLifecycle) *)
(* stated in KeyValueStore.tla. *)
(***************************************************************************)
EXTENDS KeyValueStore, TLAPS

Inv == TypeInvariant /\ TxLifecycle

THEOREM TypeAndLifecycle == Spec => []Inv
<1>1. Init => Inv
BY DEF Init, Inv, TypeInvariant, TxLifecycle, Store
<1>2. Inv /\ [Next]_<<store, tx, snapshotStore, written, missed>> => Inv'
<2> SUFFICES ASSUME Inv,
[Next]_<<store, tx, snapshotStore, written, missed>>
PROVE Inv'
OBVIOUS
<2>. USE DEF Inv, TypeInvariant, TxLifecycle, Store
<2>1. ASSUME NEW t \in TxId, OpenTx(t)
PROVE Inv'
BY <2>1 DEF OpenTx
<2>2. ASSUME NEW t \in tx, NEW k \in Key, NEW v \in Val, Add(t, k, v)
PROVE Inv'
BY <2>2 DEF Add
<2>3. ASSUME NEW t \in tx, NEW k \in Key, NEW v \in Val, Update(t, k, v)
PROVE Inv'
BY <2>3 DEF Update
<2>4. ASSUME NEW t \in tx, NEW k \in Key, Remove(t, k)
PROVE Inv'
BY <2>4 DEF Remove
<2>5. ASSUME NEW t \in tx, RollbackTx(t)
PROVE Inv'
BY <2>5 DEF RollbackTx
<2>6. ASSUME NEW t \in tx, CloseTx(t)
PROVE Inv'
BY <2>6 DEF CloseTx
<2>7. CASE UNCHANGED <<store, tx, snapshotStore, written, missed>>
BY <2>7
<2>. QED BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7 DEF Next
<1>. QED BY <1>1, <1>2, PTL DEF Spec, Inv

============================================================================
8 changes: 8 additions & 0 deletions specifications/KeyValueStore/manifest.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,14 @@
"features": [],
"models": []
},
{
"path": "specifications/KeyValueStore/KeyValueStore_proof.tla",
"features": [],
"models": [],
"proof": {
"runtime": "00:00:05"
}
},
{
"path": "specifications/KeyValueStore/MCKVS.tla",
"features": [],
Expand Down
2 changes: 1 addition & 1 deletion specifications/MisraReachability/ParReachProofs.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ LEMMA TypeInvariant == Spec => []Inv
<1>3. QED
BY <1>1, <1>2, PTL DEF Spec

THEOREM Spec => R!Init /\ [][R!Next]_R!vars
THEOREM RefinementSafety == Spec => R!Init /\ [][R!Next]_R!vars
<1>1. Init => R!Init
BY ProcsAssump DEF Init, R!Init, pcBar, vrootBar, ProcSet
<1>2. Inv /\ [Next]_vars => [R!Next]_R!vars
Expand Down
9 changes: 8 additions & 1 deletion specifications/MisraReachability/ReachableProofs.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -194,7 +194,7 @@ THEOREM Thm3 == Spec => []Inv3
BY <1>1, <1>2, Thm2, PTL DEF Spec


THEOREM Spec => []((pc = "Done") => (marked = Reachable))
THEOREM Thm4 == Spec => []((pc = "Done") => (marked = Reachable))
(*************************************************************************)
(* This theorem follows easily from the invariance of Inv1 and Inv3 and *)
(* the trivial result Reachable3 of module ReachabilityProofs that *)
Expand All @@ -209,6 +209,13 @@ THEOREM Spec => []((pc = "Done") => (marked = Reachable))
BY Reachable3 DEF Inv3
<1>3. QED
BY <1>1, <1>2, Thm1, Thm3, PTL

(***************************************************************************)
(* The same property restated under the spec's PartialCorrectness name, *)
(* matching the THEOREM stub at the bottom of Reachable.tla. *)
(***************************************************************************)
THEOREM PartialCorrectnessThm == Spec => []PartialCorrectness
BY Thm4, PTL DEF PartialCorrectness
=============================================================================
\* Modification History
\* Last modified Sun Apr 14 16:24:32 PDT 2019 by lamport
Expand Down
Loading
Loading