diff --git a/packages/opencode/specs/simulation-research/architecture-synthesis.md b/packages/opencode/specs/simulation-research/architecture-synthesis.md
new file mode 100644
index 0000000000..3f742a1cd0
--- /dev/null
+++ b/packages/opencode/specs/simulation-research/architecture-synthesis.md
@@ -0,0 +1,270 @@
+# Architecture Synthesis For Opencode Simulation
+
+## Core Direction
+
+The simulation system should be a real-app, TUI-driven, stateful model-based testing harness. It should not be a custom app command, a forked backend, or a broad reimplementation of opencode services.
+
+The production app should run normally with one required flag:
+
+```sh
+OPENCODE_SIMULATION=1 bun run dev
+```
+
+That flag enables narrow foundational layer replacements and starts a frontend-owned simulation WebSocket server. The backend server remains the normal server; simulation-only backend controls are gated behind the flag and are only reached through the frontend control server.
+
+## Control Surface
+
+- Frontend TUI process owns the external control server.
+- Protocol: JSON-RPC 2.0 over WebSocket.
+- Bind loopback only.
+- Start at port `40900`, scan upward if occupied, and log/display the actual URL.
+- External drivers never talk directly to backend simulation routes.
+- The frontend proxies backend simulation control over the same transport the TUI already uses.
+
+Initial JSON-RPC method families:
+
+- `ui.state`: screen, elements, focus, generated executable actions.
+- `ui.action`: execute real user-level inputs through OpenTUI APIs.
+- `ui.render`: force/wait for render and return state.
+- `backend.filesystem.seed` / `backend.filesystem.write`.
+- `backend.network.register`.
+- `backend.llm.enqueue`.
+- `backend.snapshot`.
+- `trace.list` / `trace.clear` / `trace.export`.
+- `run.stabilize`: wait for TUI/backend quiescence and return observations.
+
+## Action Model
+
+Actions must stay at real user-input level. The old branch's action vocabulary is the right starting point:
+
+```ts
+type UIAction =
+ | { type: "typeText"; text: string }
+ | { type: "pressKey"; key: string; modifiers?: KeyModifiers }
+ | { type: "pressEnter" }
+ | { type: "pressArrow"; direction: "up" | "down" | "left" | "right" }
+ | { type: "focus"; target: number }
+ | { type: "click"; target: number; x: number; y: number }
+```
+
+`ui.state` should return both:
+
+- `elements`: focusable/clickable/editor renderables.
+- `actions`: generated executable actions derived from those elements.
+
+Fake OpenTUI renderer and visible terminal renderer should both adapt to this same action protocol.
+
+## Foundational Layer Replacement
+
+Simulation should plug into current `AppNodeBuilder.build(...)` and `AppNodeBuilderV1.build(...)` replacement seams.
+
+Acceptable core boundaries to swap:
+
+- `FileSystem.FileSystem` / `FSUtil.Service` where needed.
+- `HttpClient.HttpClient`.
+- `RequestExecutor` / `LLMClient` or equivalent lowest LLM boundary.
+- Process spawner.
+- Global paths / env / temp paths.
+- Clock/random later, if needed.
+- Database path or in-memory DB when simulation requires isolation.
+
+Avoid replacing application services unless a core boundary is impossible:
+
+- Do not replace `SessionPrompt`, `SessionProcessor`, `ToolRegistry`, route trees, or app-level provider abstractions as the default approach.
+- Do not add a custom `simulate` command as the primary execution path.
+- Do not implement a parallel fake app.
+
+## Trace Model
+
+The frontend simulation server owns an in-memory append-only trace log by default.
+
+Trace records should include:
+
+- Run metadata: app version, seed, renderer mode, simulation URL.
+- Initial world setup: filesystem, config, environment, backend state.
+- UI observations: screen, elements, generated actions, focused item.
+- UI actions: command sent, concrete OpenTUI action, timestamp/order.
+- Backend events: session events, provider requests, tool calls/results, permission decisions, status transitions.
+- LLM scripts consumed and provider stream chunks.
+- Filesystem and network operations/diffs.
+- Stabilization boundaries and idle checks.
+- Property checks and failures.
+- Driver/model prompts and decisions when a model is driving exploration.
+
+The trace must support:
+
+- `trace.list`: query recent records.
+- `trace.clear`: reset in-memory log.
+- `trace.export`: produce JSON suitable for replay or test generation.
+
+File writing is not required initially, but the trace schema should be JSONL-friendly.
+
+## Model-Based Core
+
+The architecture should distinguish five concepts:
+
+```ts
+type Scenario = InitialWorld & { actions: readonly Action[] }
+type Action = UIAction | BackendControlAction | DriverAction
+type Observation = UIObservation | BackendObservation | TraceObservation
+type Model = abstract state machine over observable domains
+type Property = (model, observations) => pass | fail | inconclusive
+```
+
+The model should be an executable specification, not a copy of production implementation.
+
+Good model properties:
+
+- Abstract.
+- Observable.
+- Finite nondeterminism.
+- Explicit preconditions and postconditions.
+- Valid transition relation.
+- Allows multiple valid outcomes where opencode behavior is intentionally nondeterministic.
+
+Bad model properties:
+
+- Reimplements `SessionRunner` or provider streaming.
+- Mirrors database internals exactly.
+- Uses the same branch logic as production code.
+- Requires complete knowledge of implementation scheduling.
+
+## Quiescence
+
+Quiescence is a first-class command, not a timeout hidden in tests.
+
+`run.stabilize` should check, as far as possible:
+
+- TUI render is idle.
+- No active runner for the target session.
+- No eligible durable input remains unprocessed unless intentionally queued.
+- No running tool calls remain.
+- Session status is stable.
+- Projected transcript is stable across repeated reads.
+- Backend event stream has no immediate pending event burst.
+
+If quiescence cannot be proved, the command should return structured uncertainty instead of silently sleeping.
+
+## Properties And Oracles
+
+Initial built-in properties should be simple and high-signal:
+
+- No frontend/backend crash.
+- No unknown external network unless explicitly registered.
+- No host filesystem escape.
+- No duplicated visible message IDs.
+- No orphan tool results.
+- Durable prompt admission is not lost.
+- Exact prompt retry reconciles or fails according to identity rules.
+- Queue/steer promotion preserves documented delivery semantics.
+- Interrupt/resume does not duplicate promoted inputs.
+- Stabilized sessions have coherent status and transcript.
+
+Use multiple oracle styles:
+
+- Invariant checks after every step.
+- Model/refinement checks against allowed abstract outcomes.
+- Metamorphic checks across related runs.
+- Differential checks across app versions, renderers, or storage modes.
+
+## Generation Strategy
+
+Start deterministic and structured.
+
+Inputs to generate:
+
+- Workspace filesystem shapes.
+- Config variants.
+- Auth/provider/model states.
+- Session histories.
+- Prompt text and delivery modes.
+- LLM scripts with text, tool calls, errors, chunk boundaries.
+- Tool outcomes and permission decisions.
+- UI action sequences chosen from `ui.state.actions`.
+- Interrupt/restart/crash points.
+
+Use fast-check later for the external runner:
+
+- `asyncProperty` for E2E simulation.
+- `commands` for model-based command sequences.
+- Seed/path replay.
+- Shrinking action sequences.
+
+Do not run huge property suites in CI by default. Use simulation to discover/minimize traces, then generate normal deterministic tests for CI.
+
+## Coverage Guidance
+
+The simulation server and runner should collect effectiveness signals from day one:
+
+- UI element/action coverage.
+- App route/screen coverage.
+- Backend event type coverage.
+- Session state transition coverage.
+- Tool/permission outcome coverage.
+- Network route coverage.
+- Filesystem operation coverage.
+- Error/retry/recovery coverage.
+- Discarded/precondition-failed cases.
+
+Later, preserve interesting traces as corpus seeds and mutate them structurally.
+
+## Shrinking And Test Generation
+
+Shrinking should operate on semantic trace structures:
+
+- Remove actions.
+- Reduce prompt text.
+- Reduce filesystem size.
+- Remove unrelated files/config fields.
+- Simplify LLM scripts.
+- Remove chunks while preserving tool-call validity.
+- Move or remove interrupt/restart points.
+- Reduce UI navigation before the failing action.
+
+Generated normal tests should include:
+
+- Minimal initial world.
+- Explicit UI action sequence.
+- Explicit LLM/tool/network scripts.
+- Stabilization calls.
+- Deterministic assertions over semantic observations.
+
+## LLM/Agent Driver Feedback
+
+The same WebSocket observations should support model-driven exploration.
+
+Expose enough semantic context for a model to reason:
+
+- Screen text.
+- TUI elements with roles, labels, selectors, positions, capabilities.
+- Available actions.
+- Backend snapshot summaries.
+- Recent trace records.
+- Filesystem summary/diff.
+- Network log.
+- Session/message/tool summary.
+- Property failures and uncertainty.
+
+Generated properties from models should follow a lifecycle:
+
+- Proposed from evidence.
+- Translated to executable checks.
+- Validity checked.
+- Soundness checked on normal behavior.
+- Coverage/adversarial checked where possible.
+- Accepted, refined, or rejected with reason.
+
+## First Implementation Milestone
+
+Minimal useful milestone:
+
+1. `OPENCODE_SIMULATION=1` activates simulation replacements and frontend control server.
+2. Frontend starts JSON-RPC WebSocket on `127.0.0.1:40900+`.
+3. `ui.state`, `ui.action`, `ui.render`, `trace.list`, `trace.clear`, `trace.export` work.
+4. Fake and visible OpenTUI renderers share the same action protocol.
+5. Backend simulation controls are proxied through frontend WebSocket.
+6. Backend has gated control routes only when simulation flag is enabled.
+7. In-memory trace records UI actions, observations, backend control calls, and backend snapshots.
+8. Foundational replacements cover at least LLM and network denial/registration.
+9. A simple driver can seed LLM response, type a prompt through the TUI, press enter, stabilize, and assert no crash plus response visible.
+10. The resulting trace can be exported as deterministic JSON for later replay/test generation.
diff --git a/packages/opencode/specs/simulation-research/paper-analyses.md b/packages/opencode/specs/simulation-research/paper-analyses.md
new file mode 100644
index 0000000000..ab8537678b
--- /dev/null
+++ b/packages/opencode/specs/simulation-research/paper-analyses.md
@@ -0,0 +1,290 @@
+# 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.
diff --git a/packages/opencode/specs/simulation-research/papers/.gitattributes b/packages/opencode/specs/simulation-research/papers/.gitattributes
new file mode 100644
index 0000000000..d72fd520b1
--- /dev/null
+++ b/packages/opencode/specs/simulation-research/papers/.gitattributes
@@ -0,0 +1 @@
+*.pdf binary
diff --git a/packages/opencode/specs/simulation-research/papers/2016-mysteries-of-dropbox.pdf b/packages/opencode/specs/simulation-research/papers/2016-mysteries-of-dropbox.pdf
new file mode 100644
index 0000000000..9f72209fbe
Binary files /dev/null and b/packages/opencode/specs/simulation-research/papers/2016-mysteries-of-dropbox.pdf differ
diff --git a/packages/opencode/specs/simulation-research/papers/2019-coverage-guided-pbt.pdf b/packages/opencode/specs/simulation-research/papers/2019-coverage-guided-pbt.pdf
new file mode 100644
index 0000000000..69ea69d4a0
Binary files /dev/null and b/packages/opencode/specs/simulation-research/papers/2019-coverage-guided-pbt.pdf differ
diff --git a/packages/opencode/specs/simulation-research/papers/2021-mbt-web-applications-practice.pdf b/packages/opencode/specs/simulation-research/papers/2021-mbt-web-applications-practice.pdf
new file mode 100644
index 0000000000..59a4baa4ed
Binary files /dev/null and b/packages/opencode/specs/simulation-research/papers/2021-mbt-web-applications-practice.pdf differ
diff --git a/packages/opencode/specs/simulation-research/papers/2022-pbt-for-metamorphic-testing.pdf b/packages/opencode/specs/simulation-research/papers/2022-pbt-for-metamorphic-testing.pdf
new file mode 100644
index 0000000000..50d15853b0
Binary files /dev/null and b/packages/opencode/specs/simulation-research/papers/2022-pbt-for-metamorphic-testing.pdf differ
diff --git a/packages/opencode/specs/simulation-research/papers/2022-stairway-to-verification.pdf b/packages/opencode/specs/simulation-research/papers/2022-stairway-to-verification.pdf
new file mode 100644
index 0000000000..d0521b1f2e
Binary files /dev/null and b/packages/opencode/specs/simulation-research/papers/2022-stairway-to-verification.pdf differ
diff --git a/packages/opencode/specs/simulation-research/papers/2023-quickercheck.pdf b/packages/opencode/specs/simulation-research/papers/2023-quickercheck.pdf
new file mode 100644
index 0000000000..46e60ee560
Binary files /dev/null and b/packages/opencode/specs/simulation-research/papers/2023-quickercheck.pdf differ
diff --git a/packages/opencode/specs/simulation-research/papers/2024-llms-write-good-pbt.pdf b/packages/opencode/specs/simulation-research/papers/2024-llms-write-good-pbt.pdf
new file mode 100644
index 0000000000..6731827693
Binary files /dev/null and b/packages/opencode/specs/simulation-research/papers/2024-llms-write-good-pbt.pdf differ
diff --git a/packages/opencode/specs/simulation-research/papers/2024-pbt-in-practice.pdf b/packages/opencode/specs/simulation-research/papers/2024-pbt-in-practice.pdf
new file mode 100644
index 0000000000..8f9272acb0
Binary files /dev/null and b/packages/opencode/specs/simulation-research/papers/2024-pbt-in-practice.pdf differ
diff --git a/packages/opencode/specs/simulation-research/papers/2026-agentic-pbt.pdf b/packages/opencode/specs/simulation-research/papers/2026-agentic-pbt.pdf
new file mode 100644
index 0000000000..3af5fa95f4
Binary files /dev/null and b/packages/opencode/specs/simulation-research/papers/2026-agentic-pbt.pdf differ
diff --git a/packages/opencode/specs/simulation-research/papers/2026-evolution-python-tests-to-pbt.pdf b/packages/opencode/specs/simulation-research/papers/2026-evolution-python-tests-to-pbt.pdf
new file mode 100644
index 0000000000..b22f9e4b31
Binary files /dev/null and b/packages/opencode/specs/simulation-research/papers/2026-evolution-python-tests-to-pbt.pdf differ
diff --git a/packages/opencode/specs/simulation-research/papers/2026-nl-to-executable-properties-mobile.pdf b/packages/opencode/specs/simulation-research/papers/2026-nl-to-executable-properties-mobile.pdf
new file mode 100644
index 0000000000..64625585f7
--- /dev/null
+++ b/packages/opencode/specs/simulation-research/papers/2026-nl-to-executable-properties-mobile.pdf
@@ -0,0 +1,14318 @@
+%PDF-1.7
+%
+1 0 obj
+<< /Lang (en) /Metadata 3 0 R /Names 4 0 R /OpenAction 5 0 R /Outlines 6 0 R /PageMode /UseOutlines /Pages 7 0 R /Type /Catalog /ViewerPreferences << /DisplayDocTitle true >> >>
+endobj
+2 0 obj
+<< /Author (Yiheng Xiong; Ting Su; Jingling Sun; Jue Wang; Qin Li; Geguang Pu; Zhendong Su) /CreationDate (D:20260324012303+00'00') /Creator (arXiv GenPDF \(tex2pdf:a6404ea\)) /DOI (https://doi.org/10.48550/arXiv.2603.21263) /Keywords () /License (http://creativecommons.org/licenses/by/4.0/) /ModDate (D:20260324012303+00'00') /PTEX.Fullbanner (This is pdfTeX, Version 3.141592653-2.6-1.40.28 \(TeX Live 2025\) kpathsea version 6.4.1) /Producer (pikepdf 8.15.1) /Title (From Natural Language to Executable Properties for Property-based Testing of Mobile Apps) /Trapped /False /arXivID (https://arxiv.org/abs/2603.21263v1) >>
+endobj
+3 0 obj
+<< /Subtype /XML /Type /Metadata /Length 17574 >>
+stream
+
+
+
+
+
+
+
+ Adobe PDF Schema
+ pdf
+ http://ns.adobe.com/pdf/1.3/
+
+
+
+ Trapped
+ Text
+ internal
+ Indication if the document has been modified to include trapping information
+
+
+
+
+
+ XMP Media Management Schema
+ xmpMM
+ http://ns.adobe.com/xap/1.0/mm/
+
+
+
+ DocumentID
+ URI
+ internal
+ UUID based identifier for all versions and renditions of a document
+
+
+ InstanceID
+ URI
+ internal
+ UUID based identifier for specific incarnation of a document
+
+
+ VersionID
+ Text
+ internal
+ Document version identifier
+
+
+ RenditionClass
+ RenditionClass
+ internal
+ The manner in which a document is rendered
+
+
+
+
+
+ IPTC Core Schema
+ Iptc4xmpCore
+ http://iptc.org/std/Iptc4xmpCore/1.0/xmlns/
+
+
+
+ CreatorContactInfo
+ ContactInfo
+ external
+ Document creator's contact information
+
+
+
+
+
+
+ ContactInfo
+ http://iptc.org/std/Iptc4xmpCore/1.0/xmlns/
+ Iptc4xmpCore
+ Basic set of information to get in contact with a person
+
+
+
+ CiAdrCity
+ Text
+ Contact information city
+
+
+ CiAdrCtry
+ Text
+ Contact information country
+
+
+ CiAdrExtadr
+ Text
+ Contact information address
+
+
+ CiAdrPcode
+ Text
+ Contact information local postal code
+
+
+ CiAdrRegion
+ Text
+ Contact information regional information such as state or province
+
+
+ CiEmailWork
+ Text
+ Contact information email address(es)
+
+
+ CiTelWork
+ Text
+ Contact information telephone number(s)
+
+
+ CiUrlWork
+ Text
+ Contact information Web URL(s)
+
+
+
+
+
+
+
+
+ PRISM Basic Metadata
+ prism
+ http://prismstandard.org/namespaces/basic/3.0/
+
+
+
+ complianceProfile
+ Text
+ internal
+ PRISM specification compliance profile to which this document adheres
+
+
+ publicationName
+ Text
+ external
+ Publication name
+
+
+ aggregationType
+ Text
+ external
+ Publication type
+
+
+ bookEdition
+ Text
+ external
+ Edition of the book in which the document was published
+
+
+ volume
+ Text
+ external
+ Publication volume number
+
+
+ number
+ Text
+ external
+ Publication issue number within a volume
+
+
+ pageRange
+ Text
+ external
+ Page range for the document within the print version of its publication
+
+
+ issn
+ Text
+ external
+ ISSN for the printed publication in which the document was published
+
+
+ eIssn
+ Text
+ external
+ ISSN for the electronic publication in which the document was published
+
+
+ isbn
+ Text
+ external
+ ISBN for the publication in which the document was published
+
+
+ doi
+ Text
+ external
+ Digital Object Identifier for the document
+
+
+ url
+ URL
+ external
+ URL at which the document can be found
+
+
+ byteCount
+ Integer
+ internal
+ Approximate file size in octets
+
+
+ pageCount
+ Integer
+ internal
+ Number of pages in the print version of the document
+
+
+ subtitle
+ Text
+ external
+ Document's subtitle
+
+
+
+
+
+
+ pikepdf 8.15.1
+
+ 1.7
+ application/pdf
+
+ From Natural Language to Executable Properties for Property-based Testing of Mobile Apps
+ arXiv
+
+
+ 2026-03-24T01:23:03Z
+
+
+
+
+ Text
+
+
+
+ Yiheng XiongTing SuJingling SunJue WangQin LiGeguang PuZhendong Su
+ main.tex
+
+
+ en
+
+
+ 2026-03-24T01:23:03Z
+ 2026-03-24T01:23:03Z
+ 2026-03-24T01:23:12.983420+00:00
+ arXiv GenPDF (tex2pdf:a6404ea)
+ uuid:75fd75f2-b182-4bbb-ac9b-620a88d7aeae
+ uuid:ae4cef20-5fd1-4d7a-82bb-62b1d75f7541
+ 1
+ default
+
+ China
+ xyh@stu.ecnu.edu.cn
+
+ three
+ journal
+ 1
+ 1
+ 22
+ 22
+
+ http://creativecommons.org/licenses/by/4.0/cs.SE
+
+
+
+
+endstream
+endobj
+4 0 obj
+<< /Dests 8 0 R >>
+endobj
+5 0 obj
+<< /D [ 9 0 R /Fit ] /S /GoTo >>
+endobj
+6 0 obj
+<< /Count 9 /First 10 0 R /Last 11 0 R /Type /Outlines >>
+endobj
+7 0 obj
+<< /Count 22 /Kids [ 12 0 R 13 0 R 14 0 R 15 0 R ] /Type /Pages >>
+endobj
+8 0 obj
+<< /Kids [ 16 0 R 17 0 R 18 0 R 19 0 R 20 0 R ] /Limits [ (Doc-Start) (table.caption.9) ] >>
+endobj
+9 0 obj
+<< /Annots [ 21 0 R 22 0 R 23 0 R 24 0 R 25 0 R 26 0 R 27 0 R 28 0 R 29 0 R 30 0 R 31 0 R 32 0 R 33 0 R 34 0 R 35 0 R 36 0 R 37 0 R 38 0 R ] /Contents [ 39 0 R 40 0 R 41 0 R 42 0 R ] /MediaBox [ 0 0 486 720 ] /Parent 12 0 R /Resources 43 0 R /Type /Page >>
+endobj
+10 0 obj
+<< /A 44 0 R /Next 45 0 R /Parent 6 0 R /Title 46 0 R >>
+endobj
+11 0 obj
+<< /A 47 0 R /Parent 6 0 R /Prev 48 0 R /Title 49 0 R >>
+endobj
+12 0 obj
+<< /Count 6 /Kids [ 9 0 R 50 0 R 51 0 R 52 0 R 53 0 R 54 0 R ] /Parent 7 0 R /Type /Pages >>
+endobj
+13 0 obj
+<< /Count 6 /Kids [ 55 0 R 56 0 R 57 0 R 58 0 R 59 0 R 60 0 R ] /Parent 7 0 R /Type /Pages >>
+endobj
+14 0 obj
+<< /Count 6 /Kids [ 61 0 R 62 0 R 63 0 R 64 0 R 65 0 R 66 0 R ] /Parent 7 0 R /Type /Pages >>
+endobj
+15 0 obj
+<< /Count 4 /Kids [ 67 0 R 68 0 R 69 0 R 70 0 R ] /Parent 7 0 R /Type /Pages >>
+endobj
+16 0 obj
+<< /Kids [ 71 0 R 72 0 R 73 0 R 74 0 R 75 0 R 76 0 R ] /Limits [ (Doc-Start) (cite.li2023you) ] >>
+endobj
+17 0 obj
+<< /Kids [ 77 0 R 78 0 R 79 0 R 80 0 R 81 0 R 82 0 R ] /Limits [ (cite.liang2021interactive) (cite.wei2022chain) ] >>
+endobj
+18 0 obj
+<< /Kids [ 83 0 R 84 0 R 85 0 R 86 0 R 87 0 R 88 0 R ] /Limits [ (cite.wen2023droidbot) (page.21) ] >>
+endobj
+19 0 obj
+<< /Kids [ 89 0 R 90 0 R 91 0 R 92 0 R 93 0 R 94 0 R ] /Limits [ (page.22) (subsubsection.3.2.2) ] >>
+endobj
+20 0 obj
+<< /Kids [ 95 0 R ] /Limits [ (table.caption.4) (table.caption.9) ] >>
+endobj
+21 0 obj
+<< /A << /D (cite.daka2014survey) /S /GoTo >> /Border [ 0 0 0 ] /C [ 0 1 0 ] /H /I /Rect [ 360.342 287.51 371.6 295.674 ] /Subtype /Link /Type /Annot >>
+endobj
+22 0 obj
+<< /A << /D (cite.quickcheck) /S /GoTo >> /Border [ 0 0 0 ] /C [ 0 1 0 ] /H /I /Rect [ 148.387 251.555 159.645 259.809 ] /Subtype /Link /Type /Annot >>
+endobj
+23 0 obj
+<< /A << /D (cite.arts2006testing) /S /GoTo >> /Border [ 0 0 0 ] /C [ 0 1 0 ] /H /I /Rect [ 419.528 239.599 426.153 247.853 ] /Subtype /Link /Type /Annot >>
+endobj
+24 0 obj
+<< /A << /D (cite.hughes2016experiences) /S /GoTo >> /Border [ 0 0 0 ] /C [ 0 1 0 ] /H /I /Rect [ 428.828 239.689 440.085 247.853 ] /Subtype /Link /Type /Annot >>
+endobj
+25 0 obj
+<< /A << /D (cite.hughes2016mysteries) /S /GoTo >> /Border [ 0 0 0 ] /C [ 0 1 0 ] /H /I /Rect [ 44.832 227.644 56.09 235.898 ] /Subtype /Link /Type /Annot >>
+endobj
+26 0 obj
+<< /A << /D (cite.karlsson2020quickrest) /S /GoTo >> /Border [ 0 0 0 ] /C [ 0 1 0 ] /H /I /Rect [ 58.78 227.644 70.037 235.898 ] /Subtype /Link /Type /Annot >>
+endobj
+27 0 obj
+<< /A << /D (cite.2022quickstrom) /S /GoTo >> /Border [ 0 0 0 ] /C [ 0 1 0 ] /H /I /Rect [ 72.727 227.644 83.985 235.898 ] /Subtype /Link /Type /Annot >>
+endobj
+28 0 obj
+<< /A << /D (cite.santos2018property) /S /GoTo >> /Border [ 0 0 0 ] /C [ 0 1 0 ] /H /I /Rect [ 86.675 227.644 97.933 235.898 ] /Subtype /Link /Type /Annot >>
+endobj
+29 0 obj
+<< /A << /D (cite.kea) /S /GoTo >> /Border [ 0 0 0 ] /C [ 0 1 0 ] /H /I /Rect [ 100.623 227.644 111.88 235.898 ] /Subtype /Link /Type /Annot >>
+endobj
+30 0 obj
+<< /A << /D (cite.lam2017chimpcheck) /S /GoTo >> /Border [ 0 0 0 ] /C [ 0 1 0 ] /H /I /Rect [ 345.745 215.689 357.003 223.943 ] /Subtype /Link /Type /Annot >>
+endobj
+31 0 obj
+<< /A << /D (cite.pbfdroid) /S /GoTo >> /Border [ 0 0 0 ] /C [ 0 1 0 ] /H /I /Rect [ 358.872 215.689 370.13 223.943 ] /Subtype /Link /Type /Annot >>
+endobj
+32 0 obj
+<< /A << /D (cite.sun2024property) /S /GoTo >> /Border [ 0 0 0 ] /C [ 0 1 0 ] /H /I /Rect [ 371.999 215.689 383.257 223.943 ] /Subtype /Link /Type /Annot >>
+endobj
+33 0 obj
+<< /A << /D (cite.kea) /S /GoTo >> /Border [ 0 0 0 ] /C [ 0 1 0 ] /H /I /Rect [ 385.127 215.689 396.384 223.943 ] /Subtype /Link /Type /Annot >>
+endobj
+34 0 obj
+<< /A << /D (cite.AmazeFileManager) /S /GoTo >> /Border [ 0 0 0 ] /C [ 0 1 0 ] /H /I /Rect [ 429.866 179.913 436.491 188.078 ] /Subtype /Link /Type /Annot >>
+endobj
+35 0 obj
+<< /A << /D (figure.caption.2) /S /GoTo >> /Border [ 0 0 0 ] /C [ 1 0 0 ] /H /I /Rect [ 274.693 141.721 281.239 153.094 ] /Subtype /Link /Type /Annot >>
+endobj
+36 0 obj
+<< /A << /D (figure.caption.2) /S /GoTo >> /Border [ 0 0 0 ] /C [ 1 0 0 ] /H /I /Rect [ 62.045 129.766 68.679 141.139 ] /Subtype /Link /Type /Annot >>
+endobj
+37 0 obj
+<< /A << /D (cite.kea) /S /GoTo >> /Border [ 0 0 0 ] /C [ 0 1 0 ] /H /I /Rect [ 333.007 132.003 344.265 140.257 ] /Subtype /Link /Type /Annot >>
+endobj
+38 0 obj
+<< /A << /S /URI /URI (https://arxiv.org/abs/2603.21263v1) >> /BS << /W 0 >> /NM (fitz-L0) /Rect [ 12 186.13 32 533.87 ] /Subtype /Link >>
+endobj
+39 0 obj
+<< /Length 10 /Filter /FlateDecode >>
+stream
+x+ |
+endstream
+endobj
+40 0 obj
+<< /Filter /FlateDecode /Length 3816 >>
+stream
+xڽْ6_JU*T! Kv&q{=Cq$)RݠHJr<[\IJ$ZF
ѳ'4˟=Y"i85gڎF~-*lʫxM[twSW
+W"
%asupyDDx:{5ʣRˊXZ֎VuYofY&D1!ь_R*{T4,)_\>r/rJGO^-ӸRտ3w8maJ~ol;-DA!&B:`Iz`KϿD@-uU}_ m}!?Z.vyyk $mn_|J_фw,dn4"L`P!#ߗEfpdKdNA#j!7K
ۺAػXi2/a`1cƨX6L)]ёx9&/9Q"{.k;SV2(:+#kD'Z,/t㖔ϮX~+/+GUixHN9;a,("--a`>Um% (hw<>I\rOL%@5w]vTmi}͚b MgC؏j^d䕠ч Ee%ÓGYpR\a/]^u/:0&,g4*c
©
u5~ak asC HV,WmVtmZα<vW4HP/Tݴܸrݺ]hB'ai^Xo*qY]uɎf+-ˮY)ykbʲTzWB`p[[}EC.R^9Lg30HE H4HkubL04.&Ơ1DMy{ђ5$h i#iC/7]{<sG| 8`&z_$,ࢭ#Y