Repository navigation

Lean spec of ccfraft and trace validation - #8382

Draft

cjen1-msft wants to merge 49 commits into

microsoft:mainfrom

cjen1-msft:lean-ccfraft-production

Commits on Sep 16, 2026

Add deterministic Lean replay for CCF Raft scenarios

Chris Jensen (Cjen1)
and
Copilot
committed
bdeed2e
Port CCF Raft safety proofs to the aligned model

Chris Jensen (Cjen1)
and
Copilot
committed
32499fc
Wire Lean trace-validation into the shallow TLA workflow

Chris Jensen (Cjen1)
and
Copilot
committed
0c162b1
simplify reduction.py
Chris Jensen (Cjen1)
committed
aa28201
Update to remove term mangling to get ccfraft and raft.h to align
Chris Jensen (Cjen1)
committed
15875ac
Clean up model definition
Chris Jensen (Cjen1)
committed
3421eb8
reorg
Chris Jensen (Cjen1)
committed
21c48bb
reorg
Chris Jensen (Cjen1)
committed
62c9af1

Commits on Sep 18, 2026

monotone
Chris Jensen (Cjen1)
committed
cda0c27

Commits on Sep 23, 2026

Port the CCF Raft model to MultiNodeTransitionSystem

cjen1-msft
and
Copilot
committed
28ffe0d
Prove CCF Raft safety for the network model by refinement

cjen1-msft
and
Copilot
committed
9ac7816
Document the network model, bump the replay schema, and format

cjen1-msft
and
Copilot
committed
173230a
Format the CCF Raft Lean package with leanfmt

cjen1-msft
and
Copilot
committed
9a15ae5
Merge remote-tracking branch 'upstream/main' into lean-ccfraft-production
cjen1-msft
committed
7e2ed55
Check Lean formatting per package

cjen1-msft
and
Copilot
committed
fd5a149
Prove the commit frontier property directly on the network model

cjen1-msft
and
Copilot
committed
f355447
Prove append-only committed logs directly on the network model

cjen1-msft
and
Copilot
committed
3b83068
State committed-log agreement over whole traces

cjen1-msft
and
Copilot
committed
e76300c
WIP: delete the abstract model and port the invariant to the network model

cjen1-msft
and
Copilot
committed
0813971
WIP: derive election safety and committed-log agreement from the ported invariant

cjen1-msft
and
Copilot
committed
677d93b
Add total-node invariant operations and delivery selection facts

cjen1-msft
and
Copilot
committed
824907f
Port handler, configuration coverage, and authority proof support to View

cjen1-msft
and
Copilot
committed
2ed2c5f

Commits on Sep 24, 2026

Port historical quorum and authority arguments to total-node views

cjen1-msft
and
Copilot
committed
528dca9
Prove initial, leader append, send, and election-start invariant preservation

cjen1-msft
and
Copilot
committed
9c6f7fc
Prove invariant preservation for term observation, promotion, and commit advancement

cjen1-msft
and
Copilot
committed
7242e97
Preserve the invariant through network frames, replies, and recorded votes

cjen1-msft
and
Copilot
committed
f2e392d
Complete View-level request and local-step invariant preservation

cjen1-msft
and
Copilot
committed
3551441
Add concrete View update facts and strengthen the invariant with joined endpoints

cjen1-msft
and
Copilot
committed
dd01950
Prove invariant preservation for every concrete internal input

cjen1-msft
and
Copilot
committed
8d18ac4
Complete the direct network-model safety proof

cjen1-msft
and
Copilot
committed
4d4edeb
Remove unused invariant proof support and document the direct proof

cjen1-msft
and
Copilot
committed
ba5d3ad
Add total concrete node lookup and replacement lemmas

cjen1-msft
and
Copilot
committed
9f51cef
State the safety invariant over concrete nodes and envelopes

cjen1-msft
and
Copilot
committed
97bb46a
Project election and committed-log safety directly from concrete facts

cjen1-msft
and
Copilot
committed
db7ba27
Port local handler and configuration support to concrete vocabulary

cjen1-msft
and
Copilot
committed
67286bd
Remove the intermediate state and message conversion modules

cjen1-msft
and
Copilot
committed
318dcf9
Port preservation frames and immutable histories to concrete state

cjen1-msft
and
Copilot
committed
1a341ee
Port quorum, authority, and leader-append preservation

cjen1-msft
and
Copilot
committed
bd71857
Port concrete sends, campaigns, and term observation

cjen1-msft
and
Copilot
committed
3d53b2e
Port promotion, commit advancement, and same-term step-down

cjen1-msft
and
Copilot
committed
8fc1061
Port network frames and acknowledgement delivery to envelopes

cjen1-msft
and
Copilot
committed
1ebc127
Port vote responses and request-reply history frames

cjen1-msft
and
Copilot
committed
3297712
Port vote decisions and AppendEntries request preservation

cjen1-msft
and
Copilot
committed
cc55528
Complete concrete vote and pre-vote delivery preservation

cjen1-msft
and
Copilot
committed
6369202
Complete concrete initialization and local preservation

cjen1-msft
and
Copilot
committed
00dc291
Prove reachability directly over concrete local and delivery steps

cjen1-msft
and
Copilot
committed
46e2d1e
Remove unused invariant definitions and proof support

cjen1-msft
and
Copilot
committed
58deae1
Remove redundant allocation evidence and document the concrete invariant

cjen1-msft
and
Copilot
committed
9a9ac20
Format the concrete invariant and preservation proofs

cjen1-msft
and
Copilot
committed
a897fe6