When the proof gate met Solidity
We pointed the same proof discipline at smart contracts — and found we could do better than runtime testing. Symbolic execution proving properties across every input, bound to bytecode.
ISL Studio · WholeStack Research
Formal Intent & Deterministic Proving
Notes on intent, proof, and the software in between.
Field notes, empirical benchmarks, and architectural essays from building Intent Specification Language (ISL), the deterministic compiler spine, and ShipGate independent release authority.
Flagship Essay
Intelligence is probabilistic. Authority must be deterministic.
A thesis for governing increasingly autonomous AI systems—and evidence that model mistakes do not have to become physical mistakes.
Published Essays
In-depth architectural writeups on formal specifications, compiler guarantees, and the economics of verification.
Authority · Autonomous Systems
Formal Methods · Smart Contracts
Infrastructure · Economics
Engineering Log · Autonomous Factory
Thesis · Specification
Security · Production Safety
Foundations · Compiler History
Intelligence is probabilistic. Authority must be deterministic.
We allow the intelligence proposing an action to participate too deeply in deciding whether the action is authorized. ISL is the boundary outside the model.
Language Design · SpecificationWhat an intent contract actually contains
Entities, relationships, temporal policies, mathematical invariants, and exception states — why natural language prompts are not contracts, and how ISL makes software provable.
Verification · ArchitectureProof, not vibes: where ISL is headed
What we discovered building ISL — a domain specification language that compiles one prompt into an application whose safety is adversarially proven against a real database.
Two cents a build: the economics of proof
Zeta writes one spec at ~3,000 tokens/sec, then proves the entire application deterministically. Proving is free. Measured across 236 real enterprise builds.
The pipeline is real
One window of work. Ten agents in isolated worktrees. Twenty commits on main and ~320 green tests proving that natural language → cryptographically verified TypeScript is no longer a slide deck.
The bet behind ISL
A year building a specification language for AI code. Natural language is the drift, not the interface — here is the thesis, what already ships, and what comes next.
Can we actually ship safe AI code?
A night with the gate, Intent Specification, and the wall ahead — cloning real Next.js repositories, hand-writing OAuth specs, and asking the question vibe-coding decks refuse to answer.
The origins of ISL
From VibeCheck's truthpack to a compiler contract: why AI-generated code requires an executable intent contract, and how ISL came to be the backbone of WholeStack.
Scale Lab
Failed Experiments Stay Published
Lab Notes: Finding The Wall
Development is not a highlight reel. Scaling is not only successful runs. When an optimization fails or a boundary is hit, we publish the telemetry. We don't optimize benchmarks by weakening verification.
| Experiment / Scale Rung | Entities | Routes | Files Emitted | TTPS / Clock | Verdict |
|---|---|---|---|---|---|
| 26-Entity Full Ship | 26 | 52 | 317 | 198.883s (133.2s evaluator) | P3 PASS (RECEIPT) |
| 156 Entities Scaling v0.2 | 156 | 666 | 3,122 | 10.370s emit | COMPILE ONLY |
| Parallel Probes Contention | 12 | 24 | 184 | p50: 25.7s / p95: 34.7s | FAILED OPTIMIZATION |
| Overlay Publish Re-use | 12 | 24 | 184 | p50: 23.3s / p95: 29.9s | ACCEPTED (FASTER) |
NOTE 01 · 2026-08-31
156 Entities
156 distinct entities, 337 relationships, 1,010 fields, 666 page routes, 3,122 files on disk, and 10,395 lines of ISL materialized in ~10 seconds. Full verification was intentionally not run — compile only is not verified.
NOTE 02 · 2026-08-31
Parallel Probes
Why concurrency made verification slower: live route probes hitting a warming Next.js app forced overlapping compiles instead of a sequential walk. Tail latency degraded from 30.4s to 34.7s.
NOTE 03 · 2026-08-31
Proof Graph
How proof representation became a scaling boundary. Proof work grows non-linearly with the generated graph. Turning proofs back on is the next experiment, not a number to backfill.
NOTE 04 · 2026-08-31
Overlay Publish
Reusing node_modules/.next across prompt-native runs via overlay publishing reduced p50 TTPS to 23.3s without changing or weakening a single P3 verification obligation.
NOTE 05 · 2026-08-31
Next: 156-Entity Full Ship
The progression is 38 → 156 → Ship. Until that receipt exists, 156 stays COMPILE ONLY. Verification cannot be bypassed to chase a vanity benchmark.
NOTE 06 · 2026-08-31
ISL Studio IDE
Monaco workbench at /ide. Contract-first ISL, Change Impact Lens, and ShipGate verification. Enterprise-gated — not a public playground door.
Software should end in proof, not a promise.
WholeStack is the manufacturing spine that turns messy business requirements into verified, deployed software.