[cjen1-msft]

Adds lean/ccf-raft/CCFRaft/PropertiesTLA.lean, which states Lean versions of the TLA+ safety properties LogInv and CommittedLogAppendOnlyProp as theorems, each paired with a non-vacuity witness lemma. They are proved in a self-contained CCFRaft/ProofTLA/ closure. The aim is to measure how much Lean proof these TLA+ properties need, separately from the existing Lean safety proof work.

Base. This PR targets main and is based on main at afd42aa7e, which includes the model (#8578), the Lean safety proofs (#8583) and the bundled transition-system types (#8624). No GitHub stack is used. The head is 2c2372466. The diff against main touches only ProofTLA/, PropertiesTLA.lean, Tests/ArchitectureTLA.lean, Tests/PropertiesTLA.lean, the CCFRaft.lean umbrella and the README.

Statements. The presentation follows Properties.lean. Each property is a directly stated theorem with explicit quantifiers, and each witness is a separate lemma with explicit existentials. Both are proved by exact of a ProofTLA theorem, and ProofTLA is imported privately.

• The properties are invariants of Model.transitionSystem. Each quantifies every initial membership (Finset NodeID) and node list.
• They are meant to match the TLA+ semantically, not to transliterate its temporal operators. For these safety properties, Spec => []P means P holds in every reachable state, and Spec => [][A]_vars means A holds on every enabled step from a reachable state; stuttering steps satisfy it trivially and fairness plays no part.
• The committed log is log.take commitIndex over full entries (term and content), which matches TLA+ Committed(i) == SubSeq(log[i], 1, commitIndex[i]).

The theorems and witnesses:

• log_inv (LogInv, ccfraft.tla ~1400): in every reachable state, the committed logs of any two nodes are prefix-comparable. This is the same-state property, which is weaker than committed_logs_prefix in Properties.lean.
• committed_log_append_only_prop (ccfraft.tla ~1639): on every enabled step from a reachable state, each node's committed log is a prefix of its committed log afterwards.
• abs.tla AppendOnlyProp is not stated separately. Under MappingToAbs it is the same property over entry terms only, so committed_log_append_only_prop implies it.
• log_inv_witness: a reachable state in which two distinct nodes both have nonempty committed logs.
• committed_log_append_only_prop_witness: an enabled step from a reachable state that strictly extends a nonempty committed log.

Tests/PropertiesTLA.lean checks that both claims cover every state and adjacent step of any valid finite or infinite Stream'.Seq trace.

These are statements about the Lean model. That the Lean model is equivalent to the TLA+ model is not proved; it is a trust boundary.

Proof. The proofs were ported from a snapshot of #8583's safety proof into ProofTLA and pruned to the declarations the theorems depend on. Nothing in ProofTLA or PropertiesTLA.lean imports CCFRaft.Proofs* or CCFRaft.Properties; Tests/ArchitectureTLA.lean enforces this.

• ProofTLA is 23 files and 7177 lines (6435 non-blank). The witness proofs in ProofTLA/Witnesses.lean account for 267 of those lines.
• PropertiesTLA.lean is 87 lines (74 non-blank).
• The README has the commands to reproduce these counts.

CI. CCFRaft.lean publicly imports PropertiesTLA alongside Properties, and privately imports the TLA tests, as main does for its tests. The existing Lean workflow therefore covers the new modules with lake check --inadvisably-no-sandbox, lake exe check-imports, formatting and lake lint. Tests/ArchitectureTLA.lean requires the four theorem roots to be theorems that use only propext, Classical.choice and Quot.sound. This PR does not change the workflow.

Manual testing. These checks passed locally on head 2c2372466:

• lake build --wfail (3200 jobs), which includes the canonical traces, Tests/Architecture.lean, and the Tests/ArchitectureTLA.lean independence and axiom audit
• lake exe check-imports
• lake lint
• leanfmt on the package
• scripts/ascii-checks.sh
• scripts/doc-newline-checks.sh
• prettier on the README

lake check was not run locally on this head; it runs in CI. An earlier lake check --inadvisably-no-sandbox on head 4873cffab (based on 8fb56b285) accepted the solution with only propext, Quot.sound and Classical.choice. No sandboxed kernel check has been run.

Rebasing onto afd42aa7e needed two follow-up commits. The first ports ProofTLA to the bundled TransitionSystem types from #8624, in the same way #8624 ported Proofs. The second restores the README section after main's rewrite. Intermediate commits do not build against afd42aa7e.