TypeScript formal verification experiment

What assurance do tests, proofs and system models add to a TypeScript admission rule, and what work keeps that assurance connected to running code?

Recorded October 28–29, 2026. Independently authored by Nnenna Ndukwe with a coding agent. This page is the research record; the accompanying article and social drafts remain unpublished.

What the experiment found

For a small bounded rule, exhaustive execution and formal checking each rejected all eight deliberately seeded defects; seven examples rejected seven. At the largest tested domain, formal checking had lower measured wall time and higher sampled memory. Separate HTTP tests and bounded system modeling exposed interaction failures. A maintenance fixture passed verification after its caller moved to another function; checking the actual target rejected its seeded bug.

The same rule across five domains

The initial pure port tracks global and client counts plus whether the caller holds a permit. Acquisition succeeds exactly when that caller has no permit and both caps have room. A successful acquisition increments both counts once. Rejection and repeated release preserve counts; release of an owned permit decrements both once. Each scaling instance substitutes cap constants in this same complete contract and implementation.

Exhaustive execution was faster through 920,066 pairs. At 14,690,306 pairs, medians were 3.446 seconds exhaustive and 1.231 seconds formal. Maximum sampled process-tree peaks across the four clean invocations at that domain were 89.6 and 514.0 MiB respectively. This is a checking-cost crossover for these implementations of a simple arithmetic rule. Editing productivity and application throughput remain unmeasured.

Interaction and maintenance results

The separate local HTTP workflow uses synthetic owner labels, retained one-shot request IDs and permit cleanup after work failure. Six clean HTTP scenarios passed. Four fixtures deliberately break check/commit atomicity, ownership, repeated-release accounting and failure cleanup. The 20,000-step sequential generator caught foreign and repeated release; races and work failure required dedicated action/schedule tests.

The bounded TLA+/TLC model explored 189 clean states and 512 unique transitions, including 188 stutter transitions. It checks six safety invariants with two clients, four request identities and global/client capacity one. Five real-controller replay paths reproduced six invariant violations; five corresponding clean controls passed. No fairness or eventual-progress theorem was checked.

Manual mapping review found that the model's pending set excludes duplicate simultaneous request IDs. A separate real HTTP test exposed two successes, active count two and one retained permit entry in the race fixture. That finding belongs to execution testing.

The pstack-guided maintenance demonstration used the same LemmaScript/Dafny checker for a bug, approved cap change, harmless refactor and stale caller mapping. The first two direct checks blocked at correspondence; maintenance rejected the bug and accepted the approved change. The refactor passed both checks. The stale old target passed; checking the actual implementation rejected its bug. Runtime bodies stayed unchanged during verification maintenance. A first attempt blocked after a generated merge base was overwritten; preserving the synchronized generation corrected the procedure. This was one informed agent with known tasks, with no comparative agent-efficiency or model-token measurement.

Methods and controls

The question, exact properties, negative controls and resource ceilings were frozen before results. The original study used one clean implementation plus eight one-edit teaching mutants across types, lint, examples, exhaustive execution, deterministic traces and formal checking. Its 216 records are nine variants × six stages × four invocations. One defect intentionally targets an input absent from the seven examples. Equal detection on that designed sample supplies no general equivalence estimate.

The finite-state count is N=(G+1)(2C+1)−C(C+1), with two actions per state. Independent summation and enumeration checked the cardinalities. Scaling streams inputs rather than materializing pairs. Ninety records comprise sixty clean invocations and thirty control invocations: two defect families at five cap settings, across three methods. Exhaustive/formal checks rejected every negative instance; examples missed the interior wrong-delta controls.

First invocation records process order, with no cache clearing. Each clean method/domain has three additional warm runs; controls have one invocation per stage/domain. Timings include process startup, harness and observer overhead. A 25 ms polling loop plus process-list cost samples summed descendant RSS. One checker ran at a time, with 60 seconds per cell, a sampled 2 GiB process-tree threshold and 1,800 seconds total measured active-wall budget. All 142 monitored cells finished without triggering a limit; their child-wall sum was 103.459 seconds, excluding reading, installation, coding and drafting. Brief memory peaks can escape polling.

Ordinary types/lint/tests, false-property and skipped-proof controls supplement proof review. A weak bounds-only contract accepts the 13→15 accounting defect; the full exact-behavior contract rejects it. The canonical proof reports ten verified units including helper witnesses; benchmark copies report two. Units aren't a count of product guarantees. Independent review recomputed cardinalities, reconciled all 90 scaling records and reconstructed the 189-state graph. It found an unobserved monitor-exception cleanup path and overstrong memory wording; both were corrected while retaining measured data.

Scope and trusted assumptions

This is a standalone pure port inspired by public Controlled Release Lab admission logic, plus a separate synthetic HTTP workflow. The original application, hosted service and JavaScript async scheduler weren't verified in place. LemmaScript translates mathematical numbers; the pure port restricts inputs to bounded integers and tests runtime guards. Translation, solver and JavaScript execution remain trusted components.

The system model derives client counts from owned permits; the sequential reference oracle separately checks the runtime's stored client map. Crash/restart, authentication, distributed coordination, request-record eviction and arbitrary user work fall outside the bounded model. Model-to-code correspondence is manually reviewed and supported by selected replays. The author/agent designed implementation and specifications, so shared-origin specification mistakes remain possible. No local/cloud AI-review benchmark ran.

Reproduce and inspect

Download the source and check bundle, per-invocation measured data and artifact SHA256 manifest. The bundle includes portable synthetic source, full contracts, negative controls, system model/configs and replay commands. It excludes private review documents, machine paths, agent instructions and dependency caches. The data export preserves measured values and omits host/context fields.

node scripts/bootstrap.mjs
npm test
npm run verify
npm run demo
ADMISSION_DEMO_ONLY=1 node phase2/workflow/replay-model-paths.mjs

The bootstrap pins official tools and targets macOS ARM64. Measured versions: Node 26.8.2, npm 11.19.1, TypeScript 5.9.3, LemmaScript 0.6.5, Dafny 4.11.0 and TLC 2.19 from the official 1.7.4 jar. Java was OpenJDK 21.0.10 (x86_64 on the ARM host). Hardware: M4 Pro / 24 GiB, macOS 26.6. Other platforms need matching official tool assets. The bundle README explains expected failures and model prerequisites.

Sources and provenance

The derived subject is Controlled Release Lab at bb71115. Tools and workflow sources: LemmaScript pinned source, its number model, Dafny 4.11.0, official TLC release and pstack by Lauren Tan. Pstack supplies workflow instructions and a model runner; external checkers supply proof/model outcomes. Factual attribution implies no endorsement.

Back to research and resources