The origins of ISL

Intent Specification Language — ISL — is a formal way to write down what AI-generated code is supposed to do. You declare the behavioral properties, the invariants, and the conformance rules a system has to honor, and the engine hands back evidence that the code behaved that way. Semantic analysis, contract evaluation, conformance testing — the point is to take something subjective, “the AI did what I asked,” and turn it into something you can check.

An intent contract is a promise the compiler can hold you to.

That is the whole bet. Intent stops being a sentence in a prompt and becomes an artifact the toolchain can read, type-check, and verify.

The dates are short and the work was not. Three commits frame the early shape of it:

ISL is a grammar and a runtime for treating intent as a first-class program artifact. An intent block carries five clauses, and the parser turns each one into a semantic node in an AST:

• requires — the preconditions an input has to meet.
• ensures — the postconditions an output has to satisfy.
• produces — the artifacts the work is meant to generate.
• evidence — the directives for collecting proof.
• verify — the predicates that decide conformance.

Underneath, ISL is an AST-based intermediate representation sitting between natural-language intent and executable checks. Each clause holds quantified predicates — forall for properties that have to hold everywhere, exists for the witness cases where one satisfying example is enough.

A semantic analyzer maps those clauses onto program invariants and test predicates. It type-checks every requires and ensures against the target signature and emits symbolic constraints for the verifier to chew on. The verifier then evaluates those predicates over real execution traces. A forall clause has to be true on every path; an exists clause collects the witnesses that prove it. What comes out the other end is signed evidence.

Run an intent against code and you get a content-addressed evidence artifact. It binds three things into one immutable, timestamped record: the intent contract, the execution trace — inputs, outputs, side effects — and the cryptographic proof that the trace satisfied the contract. That bundle is the authoritative answer to two questions at once: what the code was meant to do, and what it actually did. It is built for audit trails, compliance reporting, and supply-chain integrity, not for a dashboard you glance at and forget.

Conformance comes in four levels, each stricter than the last: L1 syntactic, it parses; L2 well-typed, the clauses match the signature; L3 verified, the predicates are true; L4 evidence-attested, the proof is signed and timestamped.

ISL came out of VibeCheck’s truthpack model — the idea of handing an AI coding agent verifiable ground-truth documents instead of hoping it remembers the rules. We had a plain problem to solve: how do you confirm that AI-generated code did the thing it was asked to do? You cannot reason about intent that lives only in a prompt or a comment. You need a machine-readable spec of the intent itself. So we wrote one.

The parser was pulled out of ShipGate’s internal verifier and published as @isl-lang/parser. That split is deliberate: outside tools can read and reason about intent contracts without touching the proprietary engine that produces the proofs.

• Specification — github.com/isl-lang/spec
• Parser — github.com/isl-lang/parser
• Editor support — ISL for VS Code

That is the origin. A grammar, a verifier, and a stubborn refusal to call code safe without proof to show for it. For why we made this the whole company, read the bet behind ISL.