Simulate to Verify

Turn a system's safety promises into a small, runnable model, then attack the model to find where the real system fails — in milliseconds, before any service starts. This is property-based testing of a state model (the field's real name; not "symbolic simulation" or "model checking" — see references/method.md §naming). It is the cheapest high-confidence way to answer "is this safe against inputs I haven't thought of yet?"

The win: the happy path is the path you already thought about. Bugs live on the hostile path — the empty string, the unicode look-alike, the value one step past a boundary, the truthy-but-garbage input. This skill finds them cheaply and repeatably, and — crucially — keeps the model honest so its green light actually means something.

When to reach for this

Use it when a system has invariants that must hold no matter the input: auth and access control, PII/secret redaction, input validation, state machines and lifecycle ladders, data pipelines, ledger/payment math, agent tool contracts, multi-tenant isolation. If you can write down a sentence of the form "X must never happen" or "Y can only happen after Z", this skill applies.

Do NOT reach for it for pure I/O, timing, concurrency, or real-model-quality questions — those are emergent and need the real thing (a fake service, a load test, an eval set). A simulation that claims to cover those is worse than none. State plainly what you cover and hand off the rest by name.

The loop (follow in order)

The whole method is seven moves. Each is explained — including why — in references/method.md. Read it before starting; it is the substance of this skill. The short version:

1. Reduce the system to rules. Strip away services and frameworks. Write each safety promise as one sentence + its citation in the real code (file:line). These invariants ARE the contract. Aim for ~6–12; if you can't name them, you don't yet understand the system well enough to simulate it.

2. Model each rule as a pure function. Mirror the real decision logic (not its I/O) in ~10–30 lines of plain code, no imports of the system. This model runs without any service — that's what makes it cheap and what lets it survive a dead machine.

3. Attack with a hostile corpus. For each rule, write many edge cases that try to break it. Push each through the model and classify the outcome: SAFE-REJECT (bad input blocked ✓), SAFE-PASS (benign input admitted ✓), LEAK (bad input got through ✗ — a safety bug), FALSE-REJECT (good input wrongly blocked — an availability cost, not a safety bug). See references/patterns.md for a catalogue of edge-case families that find real bugs in almost every system.

4. Run many seeds; find outliers. Run the corpus across N seeds (≥5). Most cases are deterministic. The dangerous ones flicker — safe on some seeds, leaking on others. Those are the outliers. A 58%-of-the-time bug is worse than an always-bug because it hides.

5. Amplify the outliers. Re-run each flickering case across hundreds more seeds to turn "sometimes" into a number ("leaks 58% of the time"), and trace which input causes it. This often also catches bugs in your own model.

6. Keep the model honest with a differential. This is the move that makes the green light mean something. Import the REAL code and assert model_decision(input) == real_decision(input) on the same inputs. If they ever disagree, THAT is the headline finding — the model has drifted and every other conclusion is suspect. Degrade gracefully (mark "undifferentiated") when the real code can't be imported, so the pure part still runs anywhere.

7. Fix test-first, then re-run to confirm. For each real leak: write a failing test against the REAL suite, fix the real code, watch it pass, then re-run the simulation and the differential to prove the hole closed and the model still mirrors the code. Triage findings — a PII leak is not the same as an interop nit; rank by what actually goes wrong.

Make it self-verifying (non-negotiable)

A simulation you can't trust to FAIL is a green light that means nothing. So the harness MUST have meta-tests proving it has teeth:

• the clean model is green;
• planting a leak (break a rule) turns it red;
• the differential catches a model that diverges from code;
• results are stable across seeds.

If you can't make it go red on demand, you haven't verified anything. Write the meta-tests alongside the harness, not after.

Scaffold — don't reinvent the harness

scripts/scaffold_simulation.py generates a working, runnable starter harness for a new system: the Artifact/Fact/State primitives, the classifier, the multi-seed runner, the outlier+amplifier, the differential stub, the ASCII visualization, and a meta-test file. Run it, then fill in the rules for the specific system:

python <skill-path>/scripts/scaffold_simulation.py --name <system> --out scripts/

It is a starting point, not a straitjacket — adapt the generated rules and corpus to the system. The point is that every future simulation starts from the proven shape (classifier, seeds, amplifier, differential, meta-tests) instead of rebuilding it. Read the scaffold's header for what each section does.

Output

Produce three things:

1. The harness (simulate_<system>.py) + its meta-tests.
2. A findings doc with the visualized run (pipeline-with-governor-health + verdict matrix), the GOOD-vs-BAD definition you observed, the outlier table with measured rates, and a severity triage.
3. An issues register if the run surfaces method debt or system bugs worth tracking — severity-ranked, each tied to the rule it touches and whether it's confirmed against code (differential) or model-only.

The honest closer

State, in one line, what a green run proves and what it doesn't. A green run proves the logical contract holds across the input space AND the model still mirrors the code. It does NOT prove the physical contract (real I/O, concurrency, timing) — name the tests that own that. This honesty is the whole point: cover the logic exhaustively, hand off the physics explicitly.

For the full reasoning behind every move, the naming, soundness limits, and a worked example, read references/method.md. For edge-case families and visualization recipes, read references/patterns.md.