[unbalancedparentheses]

Adds a section to docs/TESTING.md: the techniques the best databases use (FoundationDB and TigerBeetle simulation, SQLite and BUGGIFY fault injection, AWS TLA+, SQLite test-proving, fuzzing and metamorphic testing, Jepsen, soak and chaos runs, production canaries), how each maps to spawned's stack, and where spawned is still behind with the plan for each gap.

[github-actions]

🤖 Gemini Code Review

This is a clean documentation-only change. The comparison table, anchor links, and roadmap references in docs/TESTING.md are clear and well-structured.

LGTM!

---

Automated review by Gemini · gemini-4-argon · custom prompt

[github-actions]

🤖 Grok Code Review

Docs-only change. No correctness, concurrency, or lifecycle issues.

docs/TESTING.md — the comparison is clear and the table is the right shape. A few nits:

• The in-doc anchors are fragile. #seeds-and-decision-tapes-under---cfg-spawned_sim depends on GitHub’s slug rules for backticks and --cfg. Confirm it actually resolves; a shorter explicit heading or HTML anchor is safer. Same for #planted-bug-sensitivity, #semantics-coverage, #scenario-fuzzing-fuzz, and #soak-harness.
• “23 of 24” and “47 of 50” are hard-coded next to living matrices. They will drift. Point at the matrices as the source of truth, or generate the counts from the same place those sections do.
• “one workload on every backend must give the same result” overclaims if ordering or timing can differ across tokio vs threads. Say which properties must agree.
• Plan item 2 (“continuous seeds are the cheapest way to find what is left once scheduled runs are enabled”) is hard to parse. Split the gap (CI/manual only) from the proposed fix (always-on seeded runs).
• “rank 22a” / “rank 5c” / “ROADMAP tier 3” are opaque unless those docs are linked.

CHANGELOG.md — “how databases test” matches the new heading but reads like a missing object. “database testing practices, how each maps to spawned, and remaining gaps” is clearer.

Otherwise this is a useful, scoped addition.

---

Automated review by Grok (xAI) · grok-4.7 · custom prompt

[github-actions]

🤖 Claude Code Review

Review: PR #268 (docs-only: "How databases test, and how spawned compares")

This PR only changes docs. It adds no code, concurrency, or lifecycle risk. The section is well written and useful for positioning. My comments are about accuracy, drift risk and link hygiene.

Accuracy

docs/TESTING.md, item 4 (SQLite): "100% branch coverage at the machine-code level (MC/DC)" mixes up two separate claims.

• MC/DC means Modified Condition/Decision Coverage. It is not a machine-code metric.
• SQLite claims two things:
  • 100% branch coverage, measured on the as-deployed object code.
  • 100% MC/DC.
• Suggested wording: "100% branch coverage of the deployed machine code and 100% MC/DC coverage".

Item 3 (formal specs): "Checking traces of the real code against the spec…" sits directly after the AWS sentence, so it reads as an AWS practice. Trace checking against TLA+ is best known from MongoDB's work (and Microsoft CCF). Either attribute it to MongoDB or make it clear the sentence describes the general technique.

Table, "Memory-model checking" row: the label does not fit all the tools listed.

• Loom and ThreadSanitizer are concurrency checkers.
• LeakSanitizer finds leaks.
• Kani is bounded model checking of sequential Rust. It does not explore weak-memory interleavings.
• Suggest "Concurrency and memory-safety checking", or move Kani to the formal row.

Table, "Formal specifications" row: "Apalache proofs of the safety invariants" is accurate only if these are inductive-invariant checks. If they are bounded runs (--length=N), call them "bounded checks" so the claim isn't overstated.

Intro: "Databases have the strongest testing culture in industry" is an unsourced superlative. Consider "among the strongest".

Drift risk

Hard-coded numbers: "23 of 24 realistic bugs" and "47 of 50 guarantees" will go stale as the matrices grow. These counts presumably already appear in the linked sections. Prefer linking without the numbers, or confirm a check keeps them in sync.

Unlinked internal references: "ROADMAP tier 3", "rank 22a" and "rank 5c" point to rankings that move. Link to ROADMAP.md (with anchors if available) so readers can resolve them.

Unverified CI and production claims: please confirm these match the current repo and CI config.

• The required CI checks named sim and model-sync.
• The "mainnet" Ethlambda canary claim.

Links and anchors

Anchors to verify: check that these resolve against the actual heading text, since backtick/--cfg slug generation is easy to get wrong.

• #seeds-and-decision-tapes-under---cfg-spawned_sim
• #scenario-fuzzing-fuzz
• #planted-bug-sensitivity
• #semantics-coverage
• #soak-harness

A markdown link checker in CI would catch these.

"Porcupine-style checker": add a link to the checker's location in the repo (and to Porcupine itself).

Clarity

Semantics coverage cell: "(a check that fails for 47 of 50 guarantees)" is ambiguous. Suggest "47 of 50 guarantees have a check shown to fail when the guarantee is broken".

"Where spawned is behind", item 2: "once scheduled runs are enabled" suggests scheduled fuzz/sim runs don't exist yet. State that directly ("scheduled nightly runs are not yet enabled") so the gap is explicit.

CHANGELOG

Minor: use the path docs/TESTING.md to match the other entries' specificity.

Verdict

Approve after the SQLite MC/DC fix and the anchor check. The rest are nice-to-haves.

---

Automated review by Claude · claude-opus-5-5 · custom prompt

[github-actions]

🤖 Codex Code Review

• [P2] Overstates formal verification coverage — docs/TESTING.md:145: “models of every lifecycle protocol” conflicts with the four implemented models and the planned base lifecycle model for links, monitors, and trap_exit in ROADMAP.md. Name the covered protocols and clarify that Apalache proofs apply at fixed configuration sizes.

• [P2] Unsupported mainnet coverage claim — docs/TESTING.md:152: Existing documentation describes manually run Hoodi testnet canaries. Remove “and mainnet” unless there is evidence of those runs; this overstates production validation.

This PR changes documentation only, so it introduces no runtime, concurrency, or memory-safety changes.

---

Automated review by OpenAI Codex · gpt-6.1-sol · custom prompt

[github-actions]

🤖 DeepSeek Code Review

This PR is documentation-only, so there are no Rust code, concurrency, or memory-safety issues to review. The new section is well-organized and clearly maps database testing practices to spawned’s verification layers.

Minor documentation nits:

• docs/TESTING.md, table row Proving the tests work: hardcoded numbers (23 of 24, 47 of 50) will likely drift over time. Consider linking to a live report or adding a date/commit so the numbers remain verifiable.
• docs/TESTING.md, table row Fault injection: “drop every public future at every await point” is an absolute claim. If the suite only covers representative await points, rephrase to avoid overstating the coverage.
• docs/TESTING.md, table row Deterministic simulation: PCT is not expanded on first use in this section; spell it out (e.g., probabilistic concurrency testing) or link to a definition.
• CHANGELOG.md: the new bullet is a noun phrase while surrounding entries are verb phrases. Consider “Documented database testing techniques and gaps in TESTING.md” for consistency.

No blocking issues.

---

Automated review by DeepSeek · deepseek-v4-pro · custom prompt

[github-actions]

🤖 Kimi Code Review

Findings

• docs/TESTING.md:124-126 — AWS/TLA+ claim is too strong.
  “AWS specifies systems such as DynamoDB and S3 in TLA+ before building them” implies these systems were fully specified before their original implementation, which is not generally accurate. AWS has used TLA+ to check designs and changes in systems including S3 and DynamoDB. Suggested wording:

  AWS has used TLA+ to specify and check designs in systems including DynamoDB and S3.

• docs/TESTING.md:127-129 — Branch coverage and MC/DC are conflated.
  MC/DC is a distinct coverage criterion, not “100% branch coverage at the machine-code level.” Describe the metrics separately, for example:

  extensive branch coverage and MC/DC testing of the SQLite core, together with checks that deliberately broken builds fail the suite.
  If retaining “100%,” qualify it with the exact test configuration under which SQLite reports it.

• docs/TESTING.md:147 — “Apalache proofs” may overstate the verification.
  Apalache is a model checker; checking an invariant over bounded or finite models is not automatically a general proof. Prefer “Apalache model checks of the safety invariants”, unless these checks are specifically inductive proofs covering arbitrary parameters.

Otherwise, the addition is clear and well structured. It is documentation-only, so there are no runtime, concurrency, or memory-safety implications.

---

Automated review by Kimi (Moonshot AI) · kimi-k3.1-pro · custom prompt