anomalyco_opencode/packages/opencode/specs/simulation-research/paper-analyses.md

Paper Analyses For Simulation Architecture

This document extracts implementation-relevant lessons from the local paper corpus. The focus is opencode's proposed simulation system: real TUI-driven execution, narrow foundational layer replacement, WebSocket control, trace recording, model-based/property-based exploration, and generated deterministic tests.

2016: Mysteries of Dropbox

Main idea: stateful PBT can find bugs in real, black-box, nondeterministic distributed systems by generating action sequences, recording observations, and checking whether the observation trace has some valid explanation under a small model.

Useful techniques:

• Generate commands separately from observed effects.
• Model hidden nondeterministic events explicitly, even when the SUT does not expose them.
• Accept traces if there exists a sequence of hidden events that makes observations valid.
• Maintain possible model states, not a single expected state.
• Make quiescence explicit with a STABILIZE command.
• Re-run flaky failures during shrinking when nondeterminism cannot be fully controlled.

Pitfalls:

• Quiescence detection can lie.
• A model that is too permissive can explain away real bugs.
• Timing-dependent failures need either scheduler control or repeated validation.
• Raw happens-before modeling can become elegant but impractical.

Implications for opencode:

• Do not compare raw transcripts only. Compare observed behavior against allowed abstract outcomes.
• Represent hidden runtime transitions like prompt promotion, session wake, provider turn continuation, tool completion, retries, interrupt delivery, and event projection.
• Add a drainUntilIdle or stabilize simulation command with strict checks.
• Record all generated commands, UI actions, backend events, provider scripts, tool results, and snapshots in an append-only trace.
• Shrinking should preserve semantic validity and revalidate nondeterministic failures.

2019: Coverage Guided, Property Based Testing

Main idea: plain random generators often fail when valid inputs have sparse semantic preconditions. Coverage-guided PBT keeps interesting inputs and mutates structured values to explore deeper states.

Useful techniques:

• Maintain a corpus of inputs that improve coverage.
• Mutate typed structures rather than raw bytes.
• Keep both successful seeds and promising discarded seeds.
• Fall back to random generation when mutation stalls.
• Use coverage and progress counters, not only binary edge coverage.

Pitfalls:

• Instrumenting irrelevant framework code hurts performance.
• Generic mutators can explode in search space.
• Expert handwritten generators still outperform generic mutation but are expensive.

Implications for opencode:

• Preserve interesting Scenario and Trace seeds.
• Add structured mutators for prompts, tool calls, provider chunks, permission decisions, filesystems, config, interrupt timing, crash/restart points, and scheduler actions.
• Track semantic novelty: event types, session states, tool outcomes, permission branches, replay/recovery paths, and UI routes.
• Avoid byte fuzzing as the core; use it only inside fields that are naturally bytes/text.

2021: Model-Based Testing In Practice

Main idea: MBT works in industrial E2E systems when models are pragmatic, visible, and integrated into normal automation. Graph-like models are useful because actions and assertions are explicit and coverage is understandable.

Useful techniques:

• Model nodes as states/checkpoints and edges as actions.
• Split large systems into small composable models.
• Use traversal strategies, weights, and stop conditions.
• Report paths, coverage, and model transitions.

Pitfalls:

• Heavy formal models reduce adoption.
• Auto-inferred models can be noisy and costly to clean up.
• Coverage metrics must be live and inspectable.

Implications for opencode:

• Start with a small simulation DSL, not a complete formal model.
• Model domains separately: session lifecycle, prompt admission, queue/steer, tool execution, permissions, interrupts, compaction, crash/restart.
• Track command coverage, transition coverage, property coverage, and failure-mode coverage.
• Keep generated failure output readable: model path, user inputs, app observations, violated invariant.

2022: Property-Based Testing For Metamorphic Testing

Main idea: metamorphic testing helps when exact expected outputs are unavailable. It checks relations between multiple executions or transformed inputs.

Useful techniques:

• Generate source cases, derive follow-up cases, and compare related outputs.
• Use generators and shrinkers that preserve relation validity.
• Combine multiple metamorphic relations.

Pitfalls:

• Weak metamorphic relations miss real faults.
• Naive shrinkers can break validity.
• Reimplementing production logic in the oracle makes the test useless.

Implications for opencode:

• Use metamorphic relations for nondeterministic model behavior.
• Examples:
  • Same prompt ID and same delivery mode should reconcile exactly on retry.
  • Queueing independent prompts should preserve durable admission order.
  • Interrupt/resume should not duplicate promoted user messages or orphan tool results.
  • Crash after durable admission should not invent provider work unless recovery explicitly permits it.
  • Fake renderer and visible renderer should agree on semantic action results.
  • Two app versions should satisfy the same semantic invariants for the same trace.

2022: Climbing The Stairway To Verification

Main idea: PBT becomes stronger when it mirrors a refinement/specification structure. The test asks whether implementation behavior refines an executable abstract model.

Useful techniques:

• Generate one canonical test case and project it into abstract and concrete worlds.
• Compare implementation output to a finite set of model-allowed outcomes.
• Keep models abstract and observable.
• Use executable specs as cheaper, incremental versions of formal proofs.

Pitfalls:

• The model can become a second implementation.
• Strong preconditions plus random generation cause excessive discarded tests.
• Overly abstract nondeterminism can explode.

Implications for opencode:

• Build simulation around scenario -> model outcomes -> real app run -> relation check.
• The model should represent visible session, message, tool, provider, permission, event, status, and filesystem effects.
• The model must not reimplement SessionRunner, provider streaming, tool registry, or Effect scheduling.
• Generate concrete scenarios and derive abstract model inputs from them.

2023: QuickerCheck

Main idea: PBT and shrinking can be parallelized, especially for expensive properties, if workers have isolated state and reproducible seeds.

Useful techniques:

• Give each worker its own PRNG seed and size schedule.
• Stop all workers after the first counterexample.
• Run cleanup/finalizers for interrupted effectful properties.
• Use greedy parallel shrinking when deterministic minimality is less important than speed.

Pitfalls:

• Shared filesystem/global state breaks parallel PBT.
• Cancellation can leave processes, files, sockets, or locks behind.
• Parallel shrinking can be slower for cheap properties.

Implications for opencode:

• Design simulation workers as isolated from the start: workspace, DB, ports, fake providers, random seeds, trace buffers.
• Use (campaignSeed, workerID, caseIndex) for reproducibility.
• Separate fast local runs from long parallel campaigns.
• Add cleanup boundaries for every case.

2024: Can Large Language Models Write Good Property-Based Tests?

Main idea: LLMs can synthesize useful PBTs, but generated tests must be validated for validity, soundness, and property coverage. Two-stage prompting outperforms monolithic generation.

Useful techniques:

• First extract properties, then generate tests for one property at a time.
• Classify failures as invalid test, unsound property, weak property, or real bug.
• Use mutation/property coverage to check whether a property actually detects violations.

Pitfalls:

• Passing generated tests can be weak.
• LLMs overgeneralize documentation and miss implicit preconditions.
• Mutation coverage can be noisy if mutants are invalid or equivalent.

Implications for opencode:

• Treat model-generated simulation properties as candidates.
• Store property lifecycle: proposed, executable, validity-checked, soundness-checked, coverage-scored, accepted, rejected.
• Generate small focused properties, not one huge “test opencode” property.
• Expose enough observations for a model to validate its own property assumptions.

2024: Property-Based Testing In Practice

Main idea: experienced developers use PBT in a small number of high-leverage patterns. The hardest parts are writing useful properties, writing generators, shrinking, and knowing whether passing tests mean anything.

Useful techniques:

• High-leverage patterns include differential testing, model-based tests, round trips, catastrophic failure properties, and invariants.
• Developers validate PBT effectiveness through mutation testing, example inspection, code coverage, property coverage, and supplementary example tests.
• Passing tests need inspectable generated examples and distribution feedback.

Pitfalls:

• Derived generators can create false confidence.
• Shrinkers can violate invariants.
• Slow PBTs get removed.

Implications for opencode:

• Provide built-in property families instead of requiring every contributor to invent properties.
• Show generator stats: action distribution, trace length, discarded cases, transition coverage, example traces.
• Make failure output a concise, reviewable artifact.
• Support “promote minimized trace to normal test.”

2026: Agentic PBT

Main idea: an agentic loop can generate better PBTs than one-shot prompting by inspecting code/docs, proposing evidence-backed properties, running tests, triaging failures, refining false alarms, and reporting only reproducible bugs.

Useful techniques:

• Use a structured loop: inspect, propose, execute, triage, refine, report.
• Prefer high-value property patterns: invariants, round trips, inverse operations, multiple implementations, laws, confluence, metamorphic relations, and no-crash parser entrypoints.
• Keep an evidence chain for every property.

Pitfalls:

• Intent ambiguity is the main false-positive source.
• Internal helpers often have implicit preconditions.
• Extreme generated inputs can be unrealistic.

Implications for opencode:

• The simulation system should be friendly to model-driven exploration, not just batch tests.
• Store prompts, observations, selected actions, available actions, traces, refinements, and final classifications.
• Add a triage workflow before surfacing model-generated failures as bugs.

2026: Evolution Of Python Tests Into PBT

Main idea: existing example and parameterized tests often evolve naturally into PBTs. Generated deterministic tests and PBTs should be connected, not treated as separate worlds.

Useful techniques:

• Convert constants/parameter tables into generators.
• Keep explicit examples for known edge cases.
• Adjust generators/settings over time as tests mature.

Pitfalls:

• Coverage can be inflated by harness/generator code.
• PBTs can fail early and cover fewer later assertions.
• Slow PBTs are removed.

Implications for opencode:

• Use existing tests as simulation corpus seeds.
• Convert minimized simulation traces into normal deterministic tests.
• Keep SUT coverage separate from simulation harness coverage.
• Store generated regressions as explicit fixtures.

2026: Natural Language To Executable Properties For Mobile Apps

Main idea: natural-language app properties can become executable UI properties if the system first performs semantic grounding of UI elements.

Useful techniques:

• Decompose property synthesis into UI semantic grounding and executable property synthesis.
• Represent properties as precondition, interaction scenario, postcondition.
• Enrich each widget with text, ID, type, semantic label, functionality, screenshot/crop, and provenance.

Pitfalls:

• Similar widgets cause grounding errors.
• Free-form natural language is less reliable than structured Given/When/Then descriptions.
• Incorrect preconditions/postconditions are more common than incorrect interactions.

Implications for opencode:

• Expose semantic TUI state, not just screen text and coordinates.
• Elements/actions should have stable IDs, roles, labels, capabilities, focus/click/edit metadata, visibility, and provenance.
• Generated properties should use a precondition/action/postcondition structure.

2026: PropGen Mobile App Testing

Main idea: properties can be generated from runtime behavioral evidence. The loop is exploration, evidence collection, property synthesis, executable translation, testing, feedback, and refinement.

Useful techniques:

• Record condition-action-outcome traces.
• Use functionality-guided exploration plus random exploration fallback.
• Refine imprecise properties by classifying whether the problem is precondition, interaction, or postcondition.

Pitfalls:

• Single traces cause overfitting.
• Generated properties can assert incidental UI details.
• Refinement can overfit unless anchored to original evidence.

Implications for opencode:

• Record rich traces with before-state, action intent, concrete action, model/provider/tool effects, after-state, state diff, and outcome label.
• Let models derive properties from observed behavior, then validate and refine them.
• Use both model-guided goals and stochastic action exploration.