Consensus protocol implementations drift from their specifications as optimizations accumulate. This benchmark re-injects classic drift, missing term checks, bad vote tracking, inverted abort-safety, and asks models to recover the specification. Early N=1 runs show that implementation tasks are uniformly out of reach; only the Dafny-verified subset admits any signal.
Raft[1], Paxos, PBFT, and 2PC have decades of formal specifications behind them, TLA+ specs, Dafny[2] proofs, model-checked invariants, yet their production implementations routinely ship bugs that violate those same invariants. The pattern is consistent: an optimization lands, the formal spec is not updated, and a subtle drift opens between what the paper proves and what the code does. This benchmark mechanizes that drift: one-line mutations against classic Raft, Paxos, and 2PC implementations, scored by hidden deterministic Go test suites with fault injection (network partitions, node crashes, adversarial schedulers).
The 26 tasks span four families of correctness failure the founder cares about: spec-to-implementation drift, safety under partition, liveness under adversarial scheduling, and log-replication invariants under crash recovery. Tasks range from easy 2PC crash-recovery fixes up to hard PBFT Byzantine-quorum implementations and 5-violation Raft safety patches. A subset of tasks require Dafny proofs of protocol invariants (log compaction safety, replicated KV linearizability, 2PC atomicity) rather than code fixes, exercising the same models on machine-checked verification.
This report covers early N=1 runs for three frontier models. The headline finding is stark: every protocol-implementation task scored 0.000 across all three models. Non-zero signal is confined to the Dafny verification subset. We include full traces on the hardest task (fix_raft_safety), a representative verification task (verify_log_compaction), and a breadth example outside Raft (twopc_crash).
| Benchmark | Value | |||||
|---|---|---|---|---|---|---|
| Total tasks | 26 | |||||
| Task families | Raft, Paxos, PBFT, 2PC, CRDT, chain replication, broadcast, gossip, locks, LSM, consistent hashing, Dafny verification | |||||
| Models evaluated | 3 (N=1 each; additional models pending) | |||||
| Total episodes on disk | 77 (26 + 26 + 25) | |||||
| Overall best model mean | 0.115 (Gemini 3 Flash Preview) | |||||
| Protocol-implementation tasks with any non-zero score | 0 of 22 | |||||
| Dafny-verification tasks with at least one non-zero score | 4 of 4 | |||||
| Tasks solved at 1.000 by any model | 4 (all Dafny: verify_log_compaction, verify_replicated_kv, verify_two_phase_commit, verify_distributed_lock) | |||||
| Model | Mean score | Max score | Tasks ≥ 0.5 | Tasks at 0.000 |
|---|---|---|---|---|
| Gemini 3 Flash Preview | 0.115 | 1.000 | 3 | 23 |
| Kimi K2.5 | 0.093 | 1.000 | 2 | 22 |
| Mistral Large 3 | 0.019 | 0.500 | 1 | 25 |
| Model | fix_raft_safety | verify_log_compaction | twopc_crash |
|---|---|---|---|
| Gemini 3 Flash Preview | 0.000 | 1.000 | 0.000 |
| Kimi K2.5 | 0.000 | 1.000 | 0.000 |
| Mistral Large 3 | 0.000 | 0.000 | 0.000 |
Each task runs deterministically inside Docker (no network, no GPU). Scores are continuous in [0, 1]. Multi-gate scoring combines a compilation gate, a modification gate (agent-reverted files score 0), and a sigmoid over hidden-test pass rate. Verification tasks (Dafny) apply an additional formal-proof weighting: required lemma signatures must be present, banned keywords (assume false, etc.) are rejected, and the full proof must typecheck against Dafny's verifier. Exact weights, sigmoid centres, and anti-cheat tokens are not disclosed.
Recover a buggy Raft consensus module with five safety violations, each a missing check in a different function. The violations span the invariants that make Raft safe under adversarial partition: vote-once-per-term in RequestVote, candidate-log-at-least-as-up-to-date in StartElection, prev-log-index consistency in AppendEntries, stale-vote rejection in HandleVoteResponse, and leader-term-commit restriction in AdvanceCommitIndex. The hidden test suite injects network partitions, leader crashes, and re-election storms; a fix that plausibly compiles but violates any one of the five invariants fails the entire task (min_pass_rate = 0.4).
This is the canonical "spec drift" task: the original Raft paper specifies all five invariants. Production implementations lose them in optimization patches one at a time. An agent that truly understands Raft should recover them; an agent that pattern-matches on surface-level Go code will plausibly write all five and still fail the hidden integration tests.
sed to page through raft_safety.go, lines 110–140. Identified the HandleVoteResponse stale-vote region and the RequestVote block.
The student_strategy field reads like a correct Raft patch in prose. The scoring gate disagrees. This is the dominant failure mode on protocol-implementation tasks: the model writes confident, specification-flavoured code that plausibly addresses the bug description, then fails the hidden adversarial tests. Without visible test feedback and without the ability to reason about all five invariants interacting under partition, the agent has no way to verify whether its fix actually holds.
pass_rate=0.0, stage=below_min_pass_rate. The scoring-time hidden tests are injected from root-only storage after the agent submits and cannot be influenced by anything the agent writes into its workspace.
Kimi's run on this task was cut short by an upstream provider rate-limit error after 7 tool calls and 128K tokens. It did not reach a submission state. We include the result for completeness but treat it as infra-truncated rather than a full model failure.
| Model | Score | Tool Calls | Time (s) | Tokens |
|---|---|---|---|---|
| Gemini 3 Flash Preview | 0.000 | 29 | 289 | 157,558 |
| Kimi K2.5 | 0.000 | 7 (rate-limited) | 84 | 127,989 |
| Mistral Large 3 | 0.000 | 23 | 138 | 121,105 |
pass_rate=0.0 because the hidden tests exercise scenarios that require all five invariants to hold simultaneously. Unlike single-bug tasks, there is no partial-credit escape: the tests either all pass or almost all fail.
Write Dafny proofs of log-compaction safety for a replicated state machine: coordinated loop invariants and pre/postconditions over twelve required lemmas including AppendPreservesWellFormed, CompactPreservesCommittedReads, and AppendDoesNotAffectCommitted. The proof obligations mirror the Raft snapshot-and-compaction invariants from the TLA+ spec: the log may be truncated (compacted) at any committed prefix, but no committed read can change its answer as a result. The agent must identify the coordinated invariants across multiple functions and discharge the proof in Dafny's verifier.
Banned keywords (assume false, others) are rejected; the agent must actually prove the obligations. Exact ban list not disclosed.
Append, Commit, and Compact.
WellFormed preservation lemmas under all three state-changing operations.
Flash's strategy is the canonical Dafny pattern: lift imperative methods into functional form so they can appear inside lemma specifications, then prove preservation of the structural invariant (WellFormed) under each transition. 16 tool calls, one compile-verify loop, clean finish.
Kimi also solved this task at 1.000 in 13 tool calls and 272K tokens, twice the token budget of Flash, same terminal score. The trace shows a longer exploration of Dafny tactics early on, then convergence on the same functional-encoding strategy.
Local scoring disabled (no container image)), which caused the final recorded score to be 0.000. This is a known infra artefact on one of the three runs: we treat Mistral's verify_log_compaction data point as non-authoritative. Re-run pending.
| Model | Score | Tool Calls | Time (s) | Tokens |
|---|---|---|---|---|
| Gemini 3 Flash Preview | 1.000 | 16 | 60 | 135,612 |
| Kimi K2.5 | 1.000 | 13 | 147 | 272,004 |
| Mistral Large 3 | 0.000* | 18 | 147 | 70,038 |
*Mistral result confounded by a local-scoring infra error; re-run pending.
Recover two-phase commit with three interacting bugs: (a) vote-validation accepting malformed votes, (b) inverted decision logic that would commit on any single yes-vote instead of requiring unanimous, (c) abort-safety that loses durability across coordinator crash. All three must be fixed for the hidden test suite to pass. 2PC is included because it represents the other end of the consensus-correctness spectrum from Raft: Raft is leader-driven with majority quorums, 2PC requires unanimity and has a very different failure-mode surface (coordinator single-point-of-failure, cohort-participant indecision on crash).
If the environment only tested Raft, a model could in principle memorize the Raft specification and pattern-match. 2PC exercises a disjoint invariant set: unanimity on commit, safety of abort under crash-recovery, and the cohort-log-replay protocol. The founder's correctness-under-crash-recovery dimension lands here specifically.
RecordVote, TryDecide, Recover).
Commit decision only if ALL participants vote Commit; if any participant votes Abort, the decision is immediately set to Abort." Deleted a stale twopc_test.go that had been cached in the workspace.
Mistral Large 3 also scored 0.000 (11 tool calls, 82s): similar pattern to Flash, plausible-looking fix, failed hidden tests. Kimi K2.5 scored 0.000 in 6 tool calls (102s); its run terminated early with a brief strategy that did not reference all three bug sites. Across all three models, the recurring failure is fixing the most prominent bug (decision logic) while missing one of the other two.
| Model | Score | Tool Calls | Time (s) | Tokens |
|---|---|---|---|---|
| Gemini 3 Flash Preview | 0.000 | 11 | 66 | 50,789 |
| Kimi K2.5 | 0.000 | 6 | 102 | 125,452 |
| Mistral Large 3 | 0.000 | 11 | 82 | 48,599 |
min_pass_rate = 0.35) requires the majority of hidden tests to pass. A 1-of-3 or 2-of-3 partial fix scores zero.
min_pass_rate gate (typically 0.3–0.4).fix_raft_safety and twopc_crash, every model produced a coherent, specification-flavoured fix summary in natural language. The hidden tests, which inject partitions, crashes, and re-election storms, rejected all of them. The failure is not incoherence; it is specification-to-invariant-preservation drift. This is exactly the class of defect the benchmark is designed to detect.fix_raft_safety is a clean all-or-nothing task: five independent safety invariants, each a one-line missing check. Current models go 0/5 or 3/5 under their own self-report; the hidden tests catch whichever invariant was missed. A future model that reliably recovers all five invariants from bare-source + on-call ticket alone would be a clear capability jump.For AI labs: this environment provides verifiable feedback on whether a model understands the formal specification of consensus protocols, not just their surface-level Go idioms. For distributed-systems researchers: every scoring run is deterministic and reproducible from the Containerfile. No GPU, no network. Next-round work expands from 3 models N=1 to at least 5 models and adds N=3 reruns on the Dafny subset to tighten the error bars on the tasks that currently show signal.