Add seeded Raft simulation from marked scenarios

[cjen1-msft]

Simulation testing involves a tradeoff between reaching interesting states and not spending all of the budget livelocked (continually retrigger elections).
Our scenarios by definition are interesting states, so we can seed the simulation runs from states within these runs.

This PR adds a mark_seed,<name> to the raft driver, which gets tlc to materialise the state at that instruction.
This can then be used as the SeededInit for subsequent simulation runs.

Summary

• add mark_seed,<name> support to raft scenarios and preserve it as a trace-validation event
• export checked RaftSeeds.tla seed state from trace validation and add SeededSIMccfraft
• add CI freshness checking for the committed seed corpus and run seeded simulation in long verification
• document the operator workflow in the TLA architecture docs

Caveats

Currently this PR is only running using a couple of seeds, but we can expand that in a future PR.

[Copilot]

Pull request overview

This PR adds a mechanism to “seed” TLC simulations from interesting states encountered in existing Raft scenario traces, by introducing a mark_seed,<name> scenario instruction and exporting the corresponding state into a RaftSeeds.tla module that can be used to initialize a seeded simulation spec.

Changes:

• Add mark_seed,<name> support to the Raft scenario driver and preserve it as a trace-validation event.
• Export a checked-in seed module (tla/consensus/RaftSeeds.tla) during trace validation, and add seeded simulation spec/config (SeededSIMccfraft.*).
• Extend CI to (a) freshness-check the committed seed corpus and (b) run seeded simulation in long verification; document the workflow in the Raft TLA architecture doc.

Custom instructions used:

• .github/copilot-instructions.md
• .github/instructions/reviewing.instructions.md

Reviewed changes

Copilot reviewed 13 out of 13 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
tla/tlc.py	Adds --seed-output-dir and passes env vars to drive seed extraction during trace validation.
tla/consensus/Traceccfraft.tla	Adds a mark_seed trace event handler which serializes the current model state into RaftSeeds.tla.
tla/consensus/SeededSIMccfraft.tla	New spec that composes SIMccfraft with a seed-provided init.
tla/consensus/SeededSIMccfraft.cfg	New TLC config to run seeded simulation with existing invariants/properties.
tla/consensus/RaftSeeds.tla	Checked-in seed corpus module generated from marked scenarios.
tests/raft_scenarios/marked_startup	New scenario containing a mark_seed marker used to generate the committed seed corpus.
src/consensus/aft/test/driver.h	Adds RaftDriver::mark_seed() to emit a trace event containing marker name + state snapshot.
src/consensus/aft/test/driver.cpp	Recognizes mark_seed instruction; emits scenario command lines as valid JSON when tracing is enabled.
doc/architecture/raft_tla.rst	Documents how to mark seeds, generate RaftSeeds.tla, and run seeded simulation.
.github/workflows/long-verification.yml	Runs seeded simulation as part of long verification.
.github/workflows/ci-verification.yml	Regenerates and diffs RaftSeeds.tla to ensure the committed seed corpus is fresh.

[cjen1-msft]

Should this be pulled up into its own job?

[eddyashton]

Drive-by initial thoughts: Explicitly marking seed states might let us pick the best states, but means that expanding coverage is still a manual process. I'd be interested to see the stats for some automatic seed detection. We could try every assert line, or a few random states from each scenario, or the end of each scenario file (there's a reason to remove the manual sync cleanup states!). I'm hoping that we get some metric that N seeds is giving us far more interesting coverage-per-time than the previous single init seed (how do we measure that? I dunno!), but that eventually with too many seeds the perf starts to drop-off as we're not able to explore far around each seed, or around some of the seeds at all, or something. I'd like to explore those methodologies and metrics before committing to explicit seed marking! I'd also like to avoid a checked-in golden file for this. I guess the trace validation is currently a different job than the simulation, but surely its cheap to run the scenarios and extract their seed states every time before we do simulation?