Playground

The editor below sends your spec to spec-to-rest running server-side on the same container as this docs site, bundled into the image, invoked by an in-process API route. No auth, no separate backend.

service SafeCounter {
  state {
    count: Int
  }

  operation Increment {
    requires:
      true

    ensures:
      count' = count + 1
  }

  operation Decrement {
    requires:
      count > 0

    ensures:
      count' = count - 1
  }

  invariant countNonNegative:
    count >= 0
}

// Click Run to compile the spec.

What each target does

• check: parse + lint; empty stdout on success, pointer to the failing rule on error.
• summary: entity / op / invariant counts and per-op classification.
• ir: internal representation as Scala case-class text.
• dafny: generated verification kernel (datatypes, ServiceStateInv, per-op requires / ensures / modifies headers).

What about compile / verify / synth?

All three run in the playground too. They're already bundled in the same spec-to-rest binary that powers the inspect targets. verify does the Alloy / Z3 model check; compile emits the full per-framework + per-DB output (fastapi Python / express TypeScript / chi Go × sqlite / postgres / mysql) which the UI renders as a file tree; synth invokes the LLM CEGIS loop and needs a key you provide (the playground never stores it; it's forwarded as a header for that single request and discarded).

For long-running work like verify on a complex spec or synth with multi-iteration repair, installing the CLI is still faster (~50 ms cold start vs cold-VM boot, no spec-size cap, no per-request wall-clock limit).

The examples dropdown is populated from fixtures/spec/ at build time by build-playground-examples.mjs. Broken / negative-test / oversize (>16 KB) specs are excluded; the rest are exactly the specs used by the project's own conformance and lint suites.