ISL Documentation

ISL is a formal way to write down what software is supposed to do — the entities, behaviors, invariants, and access rules a system has to honor — in a small language a compiler can read instead of a paragraph a model can drift from. In WholeStack, the .isl contract is the behavior source of truth: code generation compiles against it, and every release is judged against it.

The claim is deliberately precise. ISL formally defines selected application behavior and enforcement obligations. ShipGate verifies specified properties against declared evidence and documented verification policies. That is the whole promise — it does not “mathematically prove the entire application correct,” and we will not tell you it does. What you specify is what gets checked; the verdict is SHIP or NO_SHIP, with evidence attached.

The language itself is open — grammar, AST, and parser are published so any tool can read and reason about an intent contract. The engine that produces proofs from those contracts is the commercial half. For the story of why the language exists, read Origins of ISL and The bet behind ISL.

ISL ships as two dialects with different jobs. Knowing which one you are holding tells you which pipeline will consume it.

The domain dialect describes an application as data plus operations: domain wraps entity, behavior, and policy declarations. It is what the template specs are written in, what a repo import recovers from your code, and what the full-stack build lane compiles into a runnable app — entities lower to Postgres tables with CHECK constraints, policies lower to row-level security, behaviors lower to auth-wired, zod-validated server actions.

domain Crm {
  version: "1.0.0"

  entity Deal [shared] {
    id: UUID [primary, immutable, unique]
    ownerId: UUID [indexed, references: "User.id", onDelete: "CASCADE"]
    stage: DealStage [default: "LEAD"]

    invariants {
      - stage in [LEAD, QUALIFIED, PROPOSAL, NEGOTIATION, WON, LOST]
    }
  }

  policy per_owner_deal {
    applies_to: Deal
    rules {
      row.ownerId == ctx.userId: allow
      default: deny
    }
  }

  behavior advanceDeal {
    // description · input · output { success, errors } ·
    // preconditions · postconditions · security { requires authenticated }
  }
}

The engine dialect describes governed capability modules: engine wraps command, state_machine, role, and evidence declarations, and engines compose into applications. This is the dialect ISL Studio’s Compile and seal pipeline consume — commands are authorized mutations, transitions are guarded, and an invalid transition is a declared illegal move the verifier must refuse.

isl 1.1
engine "auth" {
  version "0.1.0"
  intent "Authenticated identity: users, organizations, memberships, and sessions."

  commands {
    command "revoke_session" {
      label "Revoke session"
      roles ["owner", "member"]
      emits ["session_revoked"]
      state_machine "session-lifecycle"
    }
  }

  state_machines {
    state_machine "session-lifecycle" {
      initial "created"
      states ["created", "active", "revoked"]
      terminal_states ["revoked"]
      transition "session-revoke" {
        from "active"
        to "revoked"
        command "revoke_session"
      }
    }
  }
}

ISL Studio at /ide is the builder’s front door. The welcome mat offers three ways in — new project, import a repo, import a folder — and the workbench then walks one linear golden path from architecture to deploy:

1. Architecture — shape intent and architecture documents with Zeta before anything is sealed.
2. Approve documents — you sign off on the plan; approval is a step, not a formality.
3. Build ISL — the contract is authored and validated in the editor (Run → Validate ISL Workspace; the editor carries ISL-aware hover, outline, and completion).
4. Build the app — Compile App Pages turns the sealed contract into the application.
5. Preview and verify — Preview the Project Runtime boots the real app; Run ShipGate produces the verdict, and Explain NO_SHIP tells you exactly which clause failed when it fails.
6. Deploy — the deploy panel ships the proven build.

Everything on that path is also reachable from the command palette (Cmd/Ctrl-K style, View → Command Palette), and this page lives under Help → ISL Studio Docs.

The terminal builder ships as two binaries, zeta and wholestack (same commands, pick a name). Every command except login, logout, whoami, status, help, and version needs a signed-in account on a paid plan.

The short loop: zeta login once, then zeta plan to see the architecture, zeta build to get a buildId, zeta preview to use the real thing, and zeta ship when you want the whole certified pipeline — build, proof, deployment, signed receipt — in one command. Run zeta help for the full command set.

You do not have to start from a blank contract. From /ide, import a GitHub repo or upload a folder and WholeStack lifts a draft ISL contract out of the code you already have — it reads your Prisma models, your app/api route handlers, and the auth guards it can actually see, then emits parser-valid domain-dialect ISL into your workspace as specs/<domain>.recovered.isl.

Two honesty rules govern the lift. First, every recovered fact carries provenance: a signal read deterministically from your schema or source is labeled derived (a reviewer can re-derive it byte-for-byte), while a name-convention guess — say, a bare userId column with no real foreign key — is labeled inferred and is never treated as a proven fact. Second, the lift fails closed: entity recovery currently requires a Prisma schema, and a repo without one yields an empty-but-valid domain, never a fabricated one.

The recovered file is a draft, and it is named that way on purpose. Finish the contract in the editor — promote the inferred guesses you agree with, add the invariants only you know — and from there the imported project rides the same golden path as a new one.

The platform ships a corpus of 25 domain-dialect template specs — complete, working contracts for real products: crm, marketplace, blog-cms, booking-scheduler, realtime-chat, jobs, saas-auth-billing, social-feed, project-tracker, analytics-dashboard, ai-helpdesk, file-media, pay-invoices, habit-tracker, notes-tags, and more.

Three flagships push the same idea to where being wrong costs money: a medical-bill-auditor whose conservation invariant is sum(line items) == bill total, an agent-spend-guard-wallet where spentCents <= capCents and payees must be allowlisted, and an elder-spend-guard with per-transaction and daily caps. In each, the invariant is not decoration — it is the product.

Every spec in the corpus is validated end to end by the build matrix: parse, Postgres plan, compiled DDL, Drizzle schema, React plan, emitted Next.js pages. That is also why they matter beyond copy-paste — they are the reference corpus the spec generator imitates, so a spec produced for your idea is codegen-ready by construction.

Two tables, one per dialect. The engine-dialect descriptions are exactly the hover text ISL Studio’s editor shows for each keyword.

Domain dialect

Engine dialect