Proof, not vibes: where ISL is headed

A generated CRM that compiles is easy. A generated CRM where one tenant physically cannot read another’s rows, where a deal can’t skip a stage, where an audit ledger rejects edits at the database — that’s the hard part, and it’s the only part that matters once real users and real money show up. We decided generation without proof is a demo, not a product.

So ISL — our domain spec language — never stops at code. It compiles a prompt into a Domain AST, then into Postgres (tables, enums, row-level security, indexes) and a Next.js app (pages, REST routes, type-safe server actions), and then it runs the result through a proof gate. The gate returns SHIP / NO-SHIP and a trust score. Nothing reaches you on the strength of “the model seemed confident.”

The breakthrough wasn’t a smarter model. It was a harness that boots a real Postgres and attacks the generated app the way an adversary would: insert across tenants, tamper with a stamped field, mutate an append-only row, push an entity through an illegal state transition. If the attack succeeds, the build fails. There are 33 of these blocking checks across structure, security, semantics, and runtime — and each one is a concrete experiment, not a lint rule.

That harness is what turns a feature into a provable primitive. Today there are 17, and adding a primitive means adding its adversarial proof, not just its codegen:

• Data integrity

  append-only ledgers · field invariants → DB CHECK · rollup sums · stamped server-forced fields

• Isolation

  per-tenant RLS · cross-tenant adversarial matrix · author-stamped collab feeds

• Lifecycle

  state machines with proven liveness · workflow ordering · expire / cron-swept deadlines

• Ingest & AI

  file upload (auth-gated, SSRF-safe) · semantic embed · extract / OCR / transcribe

• Outbound

  exactly-once email · inbound webhook (HMAC) · outbound webhook (SSRF-safe, receipted)

• Money

  Stripe subscription gating · storefront checkout with server-recomputed price

The trust score is deliberately honest: it’s proven properties over everything we tried to prove — including the things we couldn’t. Unproven surface lowers the number. A score that can only go up is marketing; a score that can go down is a measurement.

Two dozen full applications are locked, verified, and re-buildable from a single prompt — spanning a CMS, an LMS, sales CRM, helpdesk, fleet, claims, bookings, field service, procurement, and more. Across them: over 200 proven entities, more than 260 access-guarded server actions, 23 append-only ledgers, and 159 capability primitives — every one through the gate.

The hardest single build today is a roughly 14-entity, 14-action multi-tenant SaaS — a CMS or LMS class app with multi-role RBAC, lifecycle state machines, an audit ledger, and up to eleven stacked primitives (file upload, semantic search, OCR, exactly-once email, Stripe, cron-swept deadlines), all isolated and all proven. Not a toy. A believable back office you could hand to a team.

Every one ships with a publicly re-verifiable proof certificate. You don’t take our word for it — see what’s been proven or start from a proven build.

Three lessons reshaped the roadmap. First: the wall is never generation — it’s proof. Getting a model to emit a queue or an access policy takes an afternoon. Proving it holds under attack is the real work, and it’s the work that’s worth anything.

Second: our weakest axis is clause-coverage. Structural safety — isolation, invariants, lifecycles — is strong. But deep multi-precondition workflow logic (the “only if A and B and not C” rules) is only thinly bound to proof so far. We’d rather say that out loud than paper over it. It’s the frontier, and it’s where we’re spending now.

Third, and most useful: prefer the provable equivalent. You can’t adversarially prove heterogeneous two-phase commit or exactly-once Kafka inside one Postgres — so we don’t chase the literal version. We chase the form that delivers the same guarantee and can be proven: sagas instead of 2PC, a Postgres-durable queue instead of a broker, CRDTs instead of hand-rolled sync. Anything else is codegen wearing a proof badge, and that breaks the one thing that makes ISL ISL.

Clause-coverage makes the apps we already ship trustworthy. ABAC, temporal tables, and hierarchical state machines unlock the regulated work — health, finance, legal. SSO, durable queues, and sagas unlock scale and the enterprise sale. CRDTs unlock the field. Every one arrives the same way: with a proof, or not at all.

The goal was never to generate software faster. It was to generate software you can trust on day one — and to keep widening the set of things that “trust” provably covers.