Skip to content

PROOF_DIFFICULTY.md

Latest commit

 

History

History
350 lines (301 loc) · 29.3 KB

PROOF_DIFFICULTY.md

File metadata and controls

350 lines (301 loc) · 29.3 KB

Proof difficulty ranking

This document ranks every THEOREM in the repository by the expected difficulty of producing a TLAPS proof for it. It is meant as a roadmap for contributors who want to pick off proof obligations roughly in order of ascending effort.

The survey covers all *.tla files under specifications/ (excluding .tlacache/ directories), 230 THEOREMs in total. Of those, 107 already carry a BY or structured proof. The remaining 123 — the focus of the ranking below — are either stated without proof or marked OMITTED.

Recent progress

A first round added 18 Band-T/E proofs in companion _proof.tla files; a follow-up round added 3 Band-M proofs in Paxos/Voting_proof.tla (OneValuePerBallot => OneVote, VotesSafeImpliesConsistency, ShowsSafety). A fourth round added a Band-M strengthening for TwoPhase Commit: TPSpec => []TC!TCConsistent (no conflicting decisions), with the inductive invariant first validated via Apalache in transaction_commit/MCTwoPhaseApa.tla per the trifecta workflow. A third round added 6 more Band-M proofs:

  • PaxosHowToWinATuringAward/Voting: AllSafeAtZero, ChoosableThm (Band E helpers), and ShowsSafety (Band M, ported from the sibling Paxos/Voting proof).
  • allocator/SimpleAllocator: []TypeInvariant, []ResourceMutex.
  • allocator/SchedulingAllocator: []TypeInvariant, []ResourceMutex.
  • allocator/AllocatorImplementation: []TypeInvariant.

A subsequent round started the Band-M refinement EWD998PCal Spec => EWD998Spec (PCal-translated EWD998 refines EWD998, safety only). EWD998PCal_proof.tla now closes the full inductive type invariant for the PCal spec:

THEOREM TypeCorrect == Spec => []PCalTypeOK

with PCalTypeOK == active/color/counter typing /\ NetworkOK and NetworkOK == network in [Node -> BagOf(Msg)] /\ unique-token witness. The proof comprises:

  • Init refinement (Init => EWD998!Init) with bag-level CHOOSE reasoning that pins down the initial pending and token values from the initial network state.
  • Bag helper lemmas (BagAddOfMsg, BagRemoveOfMsg, BagAddPreservesToks, BagRemovePreservesToks).
  • For each of the five PCal disjuncts (Send pl / Recv pl / Deactivate / PassToken / InitiateProbe): all four typing conjuncts of PCalTypeOK' AND the unique-token preservation conjunct of NetworkOK'.
  • The disjunct-combine QED via per-CASE+PICK destructuring of node(self). The fix that closed it was structural: switching <1>2 from ASSUME-PROVE to implication+SUFFICES so the non-NEW assumption node(self) propagates into sub-steps (TLAPS does not propagate non-NEW assumptions of an inner ASSUME-PROVE step into its sub-step obligations).

Plus the bag-level helpers needed by the future step-refinement:

PlCount(B), PendingIsPlCount, BagAdd_pl_increments, BagRemove_pl_decrements, BagAdd_tok_preserves_pl, BagRemove_tok_preserves_pl.

The empirical refinement claim was sanity-checked with TLC: exhaustive for N=2 (2360 distinct) and N=3 (321K distinct), and simulation for N=4..6 (60-120k traces, 12-50M states).

Total: 1176 obligations checked.

Remaining work: only the top-level Refinement THEOREM (Spec => EWD998Spec) -- the per-disjunct step-simulation against EWD998!Init/EWD998!Next under the refinement mapping for pending and token. For the InitiateProbe step in particular the proof additionally needs Safra's B = Sum(counter, Node) invariant transferred to PCal -- because PCal's trigger uses tok.q + counter[Initiator] # 0 while EWD998 uses > 0, the < 0 corner case is excluded only by invariant. The pending-bag helpers above are the bag-level primitives this proof will need.

See git log for the commits. Highlights:

  • 12 of the 16 Band T theorems are now done (the 4 outstanding either involve community-modules unfolding or were re-classified as Band M after attempting them).
  • 6 of the 21 Band E theorems are done; 8 more were re-classified as Band M because the obvious-looking inductive invariant turned out to need a real strengthening.

The most informative bumps were:

  • InternalMemory ISpec => []TypeInvariant: strengthened with BufConsistent (the per-ctl[p] typing of buf[p]).
  • MultiPaxos_MC TypeOK and Chameneos SumMet: both need monotone-counter / set-cardinality invariants that aren't part of TypeOK itself.
  • Voucher{Issue,Cancel,Redeem,Transfer} VTPConsistent: requires the message-sequencing invariant that Issue and Abort are mutually exclusive in msgs.
  • PaxosCommit Phase2a: needs the auxiliary invariant "phase1b messages with bal # -1 carry a non-"none" val".

Methodology

For each unproved THEOREM I estimated:

  • the shape of the inductive invariant required (is the theorem itself inductive? does it need a small strengthening? a substantial one?);
  • whether liveness machinery is involved (WF/SF fairness, well-founded measures, PTL/LATTICE reasoning);
  • whether the theorem is a refinement between two non-trivial specs (refinement mapping, possibly with auxiliary or prophecy variables);
  • whether real-time or probabilistic reasoning is required (TLAPS support for these is thin);
  • whether community-modules predicates such as IsTreeWithRoot, SimplePath, IsFiniteSet/Cardinality need to be unfolded.

Estimates assume a TLAPS-fluent prover with the community modules in scope. Person-day numbers are very approximate.

Band Label Effort Typical work
T Trivial ≤ ½ day Single-action spec, type invariant, mechanical
E Easy ½–2 days Inductive invariant ≈ goal, no liveness
M Moderate 2–10 days Real strengthening, or small algebraic / cardinality lemmas
H Hard 1–4 weeks Refinement mapping, distributed-algorithm safety, or routine WF-based liveness
VH Very Hard ≥ 1 month Liveness with well-founded measure, real-time, deep refinement, or foundational mathematics

Reality routinely surprises: any band-T/E item that touches IsFiniteSet, Cardinality, Seq, or Graphs can blow up because of awkward unfolding.

Items marked [done] have been proven in a companion _proof.tla file under the same directory. Items marked [bumped] turned out to be harder than the band suggests once attempted; their actual band is shown in parentheses.

Band T — Trivial (16 items, 12 done)

Single-action / textbook specs; one inductive invariant equal to the type predicate.

  • [done] specifications/SpecifyingSystems/HourClock/HourClock.tla:8 — HC => []HCini
  • [done] specifications/SpecifyingSystems/Composing/HourClock.tla:8 — same
  • [done] specifications/SpecifyingSystems/Liveness/HourClock.tla:8 — same
  • [done] specifications/SpecifyingSystems/RealTime/HourClock.tla:8 — same (Init/Next identical to plain version)
  • specifications/SpecifyingSystems/HourClock/HourClock2.tla:18 — HC <=> HC2 (definitional equivalence)
  • [done] specifications/SpecifyingSystems/AsynchronousInterface/Channel.tla:21 — Spec => []TypeInvariant
  • [done] specifications/SpecifyingSystems/Composing/Channel.tla:21 — same
  • [done] specifications/SpecifyingSystems/FIFO/Channel.tla:21 — same
  • [done] specifications/SpecifyingSystems/AsynchronousInterface/AsynchInterface.tla:27 — Spec => []TypeInvariant
  • [done] [bumped → M] specifications/SpecifyingSystems/CachingMemory/InternalMemory.tla:42 — ISpec => []TypeInvariant (needed BufConsistent strengthening: ctl[p]="busy" => buf[p] \in MReq, etc.)
  • [done] [bumped → M] specifications/SpecifyingSystems/Composing/InternalMemory.tla:42 — same
  • [done] [bumped → M] specifications/SpecifyingSystems/Liveness/InternalMemory.tla:42 — same
  • [done] [bumped → M] specifications/SpecifyingSystems/RealTime/InternalMemory.tla:42 — same
  • specifications/SpecifyingSystems/CachingMemory/MCWriteThroughCache.tla:90 — LM_Inner_ISpec => []LM_Inner_TypeInvariant
  • specifications/SpecifyingSystems/AdvancedExamples/InnerSequential.tla:74 — Spec => []DataInvariant (re-classified to Band M: Cardinality({i \in DOMAIN opQ[p] : opQ[p][i].reg = r}) = ... invariant requires non-trivial reasoning about the queue/regfile correspondence)
  • [done] specifications/byihive/VoucherLifeCycle.tla:96 — VSpec => [](VTypeOK /\ VConsistent) (small CSL state)

Band E — Easy (21 items, 6 done)

Two-to-five-action specs, type + simple safety; the inductive invariant is the obvious one or TypeOK ∧ goal.

  • [done] specifications/SpecifyingSystems/FIFO/InnerFIFO.tla:38 — Spec => []TypeInvariant
  • specifications/SpecifyingSystems/FIFO/InnerFIFOInstanced.tla:101 — same
  • [done] specifications/SpecifyingSystems/TLC/AlternatingBit.tla:77 — ABSpec => []ABTypeInv
  • [bumped → M] specifications/byihive/VoucherIssue.tla:261 — VTPSpec => [](VTPTypeOK /\ VTPConsistent) (VTPConsistent needs message-sequencing strengthening: Issue and Abort are mutually exclusive in msgs, etc.)
  • [bumped → M] specifications/byihive/VoucherCancel.tla:260 — same
  • [bumped → M] specifications/byihive/VoucherTransfer.tla:267 — same
  • [bumped → M] specifications/byihive/VoucherRedeem.tla:258 — same
  • [done] specifications/transaction_commit/TCommit.tla:62 — TCSpec => [](TCTypeOK /\ TCConsistent)
  • [done] specifications/transaction_commit/TwoPhase.tla:149 — TPSpec => []TPTypeOK
  • [done, partial] specifications/transaction_commit/PaxosCommit.tla:268 — PCSpec => PCTypeOK (proven for the initial state, which is all the literal theorem statement requires; the stronger []PCTypeOK would need an extra invariant about phase1b messages)
  • [bumped → M] specifications/MultiPaxos-SMR/MultiPaxos_MC.tla:32 — Spec => []TypeOK (Cardinality(Range(pending)) = Len(pending) requires the auxiliary invariant that pending has distinct elements)
  • [done] specifications/PaxosHowToWinATuringAward/Voting.tla:124 — AllSafeAtZero (pure first-order)
  • [done] specifications/PaxosHowToWinATuringAward/Voting.tla:131 — ChoosableThm
  • specifications/Paxos/Voting.tla:94 — AllSafeAtZero (same content)
  • specifications/Paxos/Voting.tla:96 — ChoosableThm (same)
  • [bumped → M] specifications/Chameneos/Chameneos.tla:79 — Spec => []SumMet (needs strengthening Sum(f, ChameneosID) = 2 * numMeetings plus reasoning about the RECURSIVE Sum operator)
  • [bumped → M] specifications/SingleLaneBridge/SingleLaneBridge.tla:114 — Spec => []TypeOK (Len(WaitingBeforeBridge) <= Cardinality(Cars) is not invariant without additional reasoning that a car may not be enqueued twice)
  • [bumped → M] specifications/SingleLaneBridge/SingleLaneBridge.tla:112 — Spec => []Invariants (uses Cardinality(CarsInBridge) < Cardinality(Bridge) + 1)
  • [done] specifications/KeyValueStore/KeyValueStore.tla:105 — Spec => [](TypeInvariant /\ TxLifecycle)
  • [done in companion] specifications/MisraReachability/Reachable.tla:195 — Spec => []PartialCorrectness (now proven as PartialCorrectnessThm in ReachableProofs.tla, and the existing structurally-equivalent unnamed theorem there is now named Thm4 for downstream reuse; the spec-file stub itself remains unproven for the usual no-circular-spec→companion-imports reason)
  • [bumped → M] specifications/Huang/Huang.tla:106 — Spec => Safe ([](TerminationDetected => []Terminated) requires the dyadic-rational weight conservation invariant; depends on the DyadicRationals community module)

Band M — Moderate (24 items)

Need a real inductive strengthening, or small algebraic / cardinality lemmas, but follow well-known patterns.

  • [done] specifications/Paxos/Voting.tla:111 — VotesSafeImpliesConsistency (proven via the TwoChosenSameValue / TwoChosenEqual chain that uses Quorum intersection and OneVote; 116 obligations)
  • [done] specifications/Paxos/Voting.tla:124 — ShowsSafety (proven by trichotomy on the witness ballot c from ShowsSafeAt; 215 total obligations including helpers)
  • [done] specifications/Paxos/Voting.tla:109 — OneValuePerBallot => OneVote (one-line BY)
  • [done] specifications/PaxosHowToWinATuringAward/Voting.tla:179 — ShowsSafety (direct port of Paxos/Voting's ShowsSafety_T)
  • specifications/Paxos/Voting.tla:178 — Invariance == Spec => []Inv (cf. byzpaxos/VoteProof.tla already proves the analogous theorem; should largely transfer; the SafeAtMonotone lemma needed for the VotesSafe preservation case was attempted but requires careful arithmetic over Ballot \cup {-1} and EXCEPT reasoning, deferred)
  • specifications/PaxosHowToWinATuringAward/Paxos.tla:319 — Invariance == Spec => []Inv (analogous)
  • specifications/SpecifyingSystems/CachingMemory/WriteThroughCache.tla:89 — Spec => [](TypeInvariant /\ Coherence) (Coherence needs a non-trivial invariant about clean/dirty cache lines)
  • specifications/SpecifyingSystems/CachingMemory/WriteThroughCacheInstanced.tla:151 — same
  • specifications/SpecifyingSystems/CachingMemory/WriteThroughCacheInstanced.tla:162 — ISpec => []TypeInvariant
  • specifications/SpecifyingSystems/RealTime/WriteThroughCache.tla:89 — same Coherence (real-time variant)
  • specifications/SpecifyingSystems/Liveness/WriteThroughCacheInstanced.tla:151 — same Coherence
  • specifications/SpecifyingSystems/Liveness/WriteThroughCacheInstanced.tla:162 — ISpec => []TypeInvariant
  • [done] specifications/allocator/SimpleAllocator.tla:109 — SimpleAllocator => []TypeInvariant
  • [done] specifications/allocator/SimpleAllocator.tla:110 — SimpleAllocator => []ResourceMutex (uses the disjoint-from-available argument; same shape generalises to SchedulingAllocator)
  • [done] specifications/allocator/SchedulingAllocator.tla:170 — Allocator => []TypeInvariant (needs Drop, \circ, and a PermSeqsType lemma that is left OMITTED because it requires induction on the recursive PermSeqs definition)
  • [done] specifications/allocator/SchedulingAllocator.tla:171 — Allocator => []ResourceMutex
  • specifications/allocator/SchedulingAllocator.tla:172 — Allocator => []AllocatorInvariant (the heavy lifting; pool of pending requests)
  • [done] specifications/allocator/AllocatorImplementation.tla:190 — Specification => []TypeInvariant (uses the same Drop / PermSeqs machinery via the Sched! instance)
  • specifications/allocator/AllocatorImplementation.tla:191 — Specification => []ResourceMutex (the client-side mutex on holding needs the cross-spec Invariant connecting holding[c] \subseteq alloc[c] plus Sched!ResourceMutex; deferred along with Sched!AllocatorInvariant)
  • specifications/allocator/AllocatorImplementation.tla:192 — Specification => []Invariant
  • specifications/NanoBlockchain/Nano.tla:488 — Safety == Spec => TypeInvariant /\ SafetyInvariant (no-double-spend; hash-graph state)
  • specifications/NanoBlockchain/MCNano.tla:119 — same (model wrapper)
  • [TLAPS-blocked] specifications/ewd998/EWD998ChanID.tla:210 — Spec => []Max3TokenRounds (Safra's three-round bound; same Utils.tla RECURSIVE block as the other EWD998Chan-family theorems. Inductive invariant would need to capture token-state + "InitiateProbe disabled once detected" reasoning).
  • specifications/FiniteMonotonic/DistributedReplicatedLog.tla:59 — Spec => []BoundedLag

Band H — Hard (32 items)

Refinement between non-trivial specs, distributed-algorithm safety, well-founded termination, or routine WF-based liveness.

  • specifications/PaxosHowToWinATuringAward/Paxos.tla:321 — Implementation == Spec => V!Spec
  • specifications/Paxos/Paxos.tla:197 — Spec => V!Spec
  • specifications/byihive/VoucherIssue.tla:278 — VTPSpec => VSpec (TPC refines voucher issuance)
  • specifications/byihive/VoucherCancel.tla:277 — same pattern
  • specifications/byihive/VoucherRedeem.tla:275 — same
  • specifications/byihive/VoucherTransfer.tla:284 — same
  • [partial] / [done for TC!TCConsistent] specifications/transaction_commit/TwoPhase.tla:165 — TPSpec => TC!TCSpec (canonical Lamport refinement; the safety corollary TPSpec => []TC!TCConsistent is now proven in TwoPhase_proof.tla with a 10-conjunct strengthening validated via Apalache before TLAPS, but the full refinement is still Band H — it would additionally need a refinement mapping that abstracts the message-level state away)
  • specifications/transaction_commit/PaxosCommit.tla:280 — PCSpec => TC!TCSpec
  • specifications/byzpaxos/PConProof.tla:511 — PT1 (ShowsSafeAt => SafeAt lemma)
  • specifications/byzpaxos/PConProof.tla:517 — Invariance == Spec => []PInv
  • specifications/byzpaxos/PConProof.tla:520 — Implementation == Spec => V!Spec
  • specifications/byzpaxos/PConProof.tla:527 — Spec => [](chosen = V!chosen)
  • specifications/MisraReachability/ParReach.tla:223 — Spec => Refines (= Spec => R!Spec; depends on the fairness-refinement piece below, since R!Spec includes WF_R!vars(R!Next))
  • specifications/MisraReachability/ParReach.tla:235 — Spec => WF_R!vars(R!Next) (fairness refinement; the per-process WF_vars(p(self)) of the parallel spec needs to be lifted via the refinement mapping to WF_R!vars(R!Next) of Misra's algorithm; non-trivial PTL reasoning)
  • [done in companion] specifications/MisraReachability/ParReach.tla:234 — Spec => R!Init /\ [][R!Next]_R!vars (now named RefinementSafety in ParReachProofs.tla; the spec-file stub remains unproven as above)
  • specifications/MisraReachability/Reachable.tla:209 — IsFiniteSet(Reachable) => Spec => <>(pc = "Done") (termination, well-founded measure on the lex pair <<Cardinality(Reachable \ marked), Cardinality(vroot)>>; uses WF_vars(Next) plus WellFoundedInduction. Multi-day TLAPS proof; deferred)
  • specifications/Huang/Huang.tla:111 — Spec => Live (termination detection liveness)
  • specifications/KnuthYao/Prob.tla:38 — Converges == Spec => <>(state \in Accepting \/ Norm(p) = 0) (probabilistic, treated as <>termination)
  • specifications/Prisoners/Prisoners.tla:178 — Spec => Safety /\ Liveness
  • specifications/SingleLaneBridge/SingleLaneBridge.tla:117 — Spec => CarsEnterBridge (small WF liveness)
  • specifications/SingleLaneBridge/SingleLaneBridge.tla:116 — Spec => CarsInBridgeExitBridge
  • specifications/allocator/SimpleAllocator.tla:111 — SimpleAllocator => ClientsWillReturn
  • specifications/allocator/SimpleAllocator.tla:112 — SimpleAllocator2 => ClientsWillReturn
  • specifications/allocator/SchedulingAllocator.tla:173 — Allocator => ClientsWillReturn
  • specifications/allocator/AllocatorImplementation.tla:193 — Specification => ClientsWillReturn
  • [TLAPS-blocked] specifications/ewd998/EWD998Chan.tla:192 — Spec => EWD998Spec (refinement to EWD998). Utils.tla (transitively imported) defines a RECURSIVE SimpleCycle(_,_,_) operator (used only by EWD998_anim.tla) that trips TLAPS' parser. Refactoring Utils.tla to move that operator to a separate AnimUtils.tla would unblock TLAPS for all of EWD998Chan, EWD998ChanID, and EWD998ChanTrace.
  • [partial] specifications/ewd998/EWD998PCal.tla:153 — Spec => EWD998Spec (TLAPS-amenable; PlusCal-translated spec refines EWD998 -- safety only, no fairness, per the spec's own comment. Substantial Band-M proof: needs an inductive invariant covering network's singleton-token property plus a 5-disjunct refinement-mapping argument). In-progress in EWD998PCal_proof.tla: 1176 obligations checked. THEOREM TypeCorrect == Spec => []PCalTypeOK (the full inductive type invariant) is closed, and the pending-bag helpers (BagAdd_pl_increments, BagRemove_pl_decrements, BagAdd_tok_preserves_pl, BagRemove_tok_preserves_pl, PendingIsPlCount) the future step-refinement will need are also proven. TLC sanity-check confirms the underlying refinement: exhaustive for N=2 (2360 distinct) and N=3 (321K distinct), simulation 60k-120k traces for N=4..6. Only the top-level Refinement theorem remains OMITTED -- the per-disjunct step-simulation against EWD998!Next under the refinement mapping for pending and token. For the InitiateProbe step in particular the proof additionally needs Safra's B = Sum(counter, Node) invariant transferred to PCal, because PCal's trigger uses tok.q + counter[Initiator] # 0 while EWD998 uses > 0 -- the < 0 corner case is excluded only by invariant.
  • [TLAPS-blocked] specifications/ewd998/EWD998ChanID.tla:262 — Spec => EWD998ChanSpec (same Utils.tla block).
  • [TLAPS-blocked] specifications/ewd998/EWD998ChanID.tla:267 — Spec => EWD998Safe /\ EWD998Live
  • specifications/MultiPaxos-SMR/MultiPaxos_MC.tla:73 — Spec => Linearizability
  • specifications/FiniteMonotonic/ReplicatedLog.tla:48 — Spec => []TypeOK (small but with monotonic data structures)
  • specifications/FiniteMonotonic/DistributedReplicatedLog.tla:67 — Spec => AllExtending (WF liveness)
  • specifications/CoffeeCan/CoffeeCan.tla:115 — TypeInvariant /\ MonotonicDecrease /\ EventuallyTerminates /\ LoopInvariant /\ TerminationHypothesis (mixed safety + termination)
  • [partial] specifications/MultiCarElevator/Elevator.tla:235 — Spec => [](TypeInvariant /\ SafetyInvariant /\ TemporalInvariant). In-progress in Elevator_proof.tla: THEOREM TypeCorrect == Spec => []TypeInvariant is fully proven (170 obligations, ~30s) using a WaitingFloor strengthening (~waiting => location \in Floor). The proof requires ASSUME Floor \cap Elevator = {} (left implicit in the spec; supplied by TLC via model values) and four LEMMA fEval == ... PROOF OMITTED primitives stating multi-arg function unfoldings (GetDistance, GetDirection, CanServiceCall, PeopleWaiting) that TLAPS' BY DEF f doesn't unfold. THEOREM SafetyCorrect == Spec => []SafetyInvariant is scaffolded with the strengthened invariant Inv2 plus seven mutually-inductive auxiliaries (WaitingDestinationDistinct, DoorsOpen*, NoServiceableActiveCall, StationaryNoPassenger, PersonImpliesButton); InitImpliesInv2 is closed (53 additional obligations, 223 total) but Inv2Next is OMITTED -- the per-action case analysis is genuine Band-H work. TemporalInvariant (liveness) not addressed.
  • specifications/CheckpointCoordination/CheckpointCoordination.tla:527 — Spec => /\ []TypeInvariant /\ []SafetyInvariant /\ []TemporalInvariant
  • specifications/ewd687a/EWD687a_proof.tla:553 & specifications/ewd687a/EWD687a.tla:430 — Spec => TreeWithRoot (needs unfolding of IsTreeWithRoot / SimplePath from community Graphs module)

Band VH — Very Hard (15+ items)

Strong-fairness liveness, deep refinement, real-time, or foundational mathematics.

  • specifications/allocator/AllocatorRefinement.tla:11 — Allocator => SimpleAllocator (refining a richer allocator into a simpler one — fairness too)
  • specifications/allocator/AllocatorImplementation.tla:203 — Specification => SchedAllocator (full refinement of scheduling allocator)
  • specifications/diskpaxos/DiskSynod.tla:126 — DiskSynodSpec => SynodSpec (Disk Paxos refines abstract Synod — extensive)
  • specifications/byzpaxos/PConProof.tla:572 — Liveness == Spec => … (Paxos liveness with explicit assumption package)
  • specifications/allocator/SimpleAllocator.tla:113 — SimpleAllocator => ClientsWillObtain (SF-style liveness with scheduling)
  • specifications/allocator/SimpleAllocator.tla:114 — SimpleAllocator => InfOftenSatisfied
  • specifications/allocator/SchedulingAllocator.tla:174 — Allocator => ClientsWillObtain
  • specifications/allocator/SchedulingAllocator.tla:175 — Allocator => InfOftenSatisfied
  • specifications/allocator/AllocatorImplementation.tla:194 — Specification => ClientsWillObtain
  • specifications/allocator/AllocatorImplementation.tla:195 — Specification => InfOftenSatisfied
  • specifications/FiniteMonotonic/ReplicatedLog.tla:70 — ExecFairSpec => Convergence (CRDT convergence on infinite fair runs)
  • specifications/FiniteMonotonic/ReplicatedLog.tla:71 — WriteFairSpec => Convergence
  • specifications/SpecifyingSystems/Liveness/LiveHourClock.tla:35 — LSpec => AlwaysTick /\ AllTimes /\ TypeInvariance (real-time liveness; TLAPS support thin)
  • specifications/SpecifyingSystems/Liveness/LiveInternalMemory.tla:44 — LISpec => LivenessProperty
  • specifications/SpecifyingSystems/RealTime/RTWriteThroughCache.tla:50 — RTSpec => RTM!RTSpec (real-time refinement)
  • specifications/SpecifyingSystems/CachingMemory/WriteThroughCache.tla:92 — Spec => LM!Spec (memory refinement; refinement mapping with auxiliary state — small project)
  • specifications/SpecifyingSystems/RealTime/WriteThroughCache.tla:92 — same with real time
  • specifications/ewd687a/EWD687a_proof.tla:568 & specifications/ewd687a/EWD687a.tla:456 — Spec => DT2 (termination detection liveness; needs WF + multiset measure on (msgs, rcvdUnacked, acks, sentUnacked))
  • specifications/SpecifyingSystems/Standard/ProtoReals.tla:36 — \E R, Plus, Times, Leq : IsModelOfReals(R, Plus, Times, Leq) (constructive existence of the real-number system from Peano — Dedekind cuts; arguably the single hardest theorem in the repo)

Already proved (107 theorems)

No work to do; listed by file with theorem count for completeness.

File Count
specifications/Bakery-Boulangerie/Bakery.tla 2
specifications/Bakery-Boulangerie/Boulanger.tla 2
specifications/FiniteMonotonic/CRDT_proof.tla 7
specifications/LearnProofs/AddTwo.tla 2
specifications/LearnProofs/FindHighest.tla 4
specifications/LoopInvariance/BinarySearch.tla 1
specifications/LoopInvariance/Quicksort.tla 1
specifications/LoopInvariance/SumSequence.tla 2
specifications/MisraReachability/ReachableProofs.tla 4
specifications/MisraReachability/ParReachProofs.tla 1
specifications/Paxos/Consensus.tla 2
specifications/Paxos/Voting.tla (1 of 8) 1
specifications/PaxosHowToWinATuringAward/Consensus.tla 1
specifications/PaxosHowToWinATuringAward/Voting.tla (2 of 5) 2
specifications/TeachingConcurrency/Simple.tla 2
specifications/TeachingConcurrency/SimpleRegular.tla 2
specifications/TwoPhase/TwoPhase.tla 1
specifications/barriers/Barriers.tla (6 of 7) 6
specifications/bcastByz/bcastByz.tla 13
specifications/byzpaxos/Consensus.tla 3
specifications/byzpaxos/BPConProof.tla 5
specifications/byzpaxos/VoteProof.tla 12
specifications/byzpaxos/PConProof.tla (1 of 6) 1
specifications/ewd687a/EWD687a_proof.tla (3 of 5) 3
specifications/ewd840/EWD840_proof.tla 4
specifications/ewd840/SyncTerminationDetection_proof.tla 4
specifications/ewd998/EWD998_proof.tla 5
specifications/ewd998/AsyncTerminationDetection_proof.tla 3
specifications/lamport_mutex/LamportMutex_proofs.tla 3
specifications/locks_auxiliary_vars/Lock.tla 1
specifications/locks_auxiliary_vars/LockHS.tla 2
specifications/locks_auxiliary_vars/Peterson.tla 2
specifications/sums_even/sums_even.tla 2

The structural pieces in ReachableProofs.tla/ParReachProofs.tla mostly cover the goals stated in Reachable.tla/ParReach.tla (the latter still need final wrap-up theorems, listed in Bands E–H above).

Caveats

  • "Difficulty" is expected difficulty for a TLAPS-fluent prover with the community modules; reality routinely surprises. Several Band-T/E items can blow up if the spec embeds something like IsFiniteSet or Cardinality whose unfolding is awkward.
  • Many "stated" theorems re-appear (the same property proved in a companion _proof.tla); I de-duplicated the obvious cases (EWD687a, EWD840, Reachable, EWD998 → TD!Spec) but a handful of Voting/Paxos invariants are essentially shadowed by byzpaxos/VoteProof.tla and would transfer with light edits.
  • The Allocator and WriteThroughCache families dominate Band H/VH — they're well-known textbook benchmarks that nobody has machine-checked in this repo yet.
  • This document is a snapshot; it should be regenerated when new specs are added or new proofs land. The extraction script lives in commit history (or can be re-derived: walk *.tla, classify each THEOREM's proof status as BY / structured / OMITTED / stated-only, exclude .tlacache/).