diff --git a/packages/opencode/specs/simulation-research/architecture-synthesis.md b/packages/opencode/specs/simulation-research/architecture-synthesis.md
deleted file mode 100644
index 3f742a1cd0f..00000000000
--- a/packages/opencode/specs/simulation-research/architecture-synthesis.md
+++ /dev/null
@@ -1,270 +0,0 @@
-# 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
deleted file mode 100644
index ab8537678be..00000000000
--- a/packages/opencode/specs/simulation-research/paper-analyses.md
+++ /dev/null
@@ -1,290 +0,0 @@
-# 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
deleted file mode 100644
index d72fd520b1c..00000000000
--- a/packages/opencode/specs/simulation-research/papers/.gitattributes
+++ /dev/null
@@ -1 +0,0 @@
-*.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
deleted file mode 100644
index 9f72209fbed..00000000000
Binary files a/packages/opencode/specs/simulation-research/papers/2016-mysteries-of-dropbox.pdf and /dev/null 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
deleted file mode 100644
index 69ea69d4a09..00000000000
Binary files a/packages/opencode/specs/simulation-research/papers/2019-coverage-guided-pbt.pdf and /dev/null 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
deleted file mode 100644
index 59a4baa4ede..00000000000
Binary files a/packages/opencode/specs/simulation-research/papers/2021-mbt-web-applications-practice.pdf and /dev/null 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
deleted file mode 100644
index 50d15853b0f..00000000000
Binary files a/packages/opencode/specs/simulation-research/papers/2022-pbt-for-metamorphic-testing.pdf and /dev/null 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
deleted file mode 100644
index d0521b1f2e7..00000000000
Binary files a/packages/opencode/specs/simulation-research/papers/2022-stairway-to-verification.pdf and /dev/null differ
diff --git a/packages/opencode/specs/simulation-research/papers/2023-quickercheck.pdf b/packages/opencode/specs/simulation-research/papers/2023-quickercheck.pdf
deleted file mode 100644
index 46e60ee5607..00000000000
Binary files a/packages/opencode/specs/simulation-research/papers/2023-quickercheck.pdf and /dev/null 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
deleted file mode 100644
index 67318276930..00000000000
Binary files a/packages/opencode/specs/simulation-research/papers/2024-llms-write-good-pbt.pdf and /dev/null 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
deleted file mode 100644
index 8f9272acb04..00000000000
Binary files a/packages/opencode/specs/simulation-research/papers/2024-pbt-in-practice.pdf and /dev/null 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
deleted file mode 100644
index 3af5fa95f41..00000000000
Binary files a/packages/opencode/specs/simulation-research/papers/2026-agentic-pbt.pdf and /dev/null 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
deleted file mode 100644
index b22f9e4b315..00000000000
Binary files a/packages/opencode/specs/simulation-research/papers/2026-evolution-python-tests-to-pbt.pdf and /dev/null 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
deleted file mode 100644
index 64625585f70..00000000000
--- a/packages/opencode/specs/simulation-research/papers/2026-nl-to-executable-properties-mobile.pdf
+++ /dev/null
@@ -1,14318 +0,0 @@
-%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