LemmaScript is TypeScript with syntax for contracts.
43//@ contract Keeps only the requests still inside the sliding time window. 44export function pruneWindow(log: number[], now: number, W: number): number[] { 45 //@ requires forall(k, 0 <= k && k < log.length ==> log[k] <= now) 46 //@ decreases log.length 47 //@ ensures \result.length <= log.length 48 //@ ensures forall(k, 0 <= k && k < \result.length ==> now - W < \result[k] && \result[k] <= now) 49 if (log.length === 0) { 50 return []; 51 } 52 const rest = pruneWindow(log.slice(1), now, W); 53 if (log[0] > now - W) { 54 return [log[0], ...rest]; 55 } 56 return rest; 57}
Engineers at Hiya leverage LemmaScript to reduce reviewer load.
I’ve been using LemmaScript to build a production-shaped TypeScript contact service for a phone product operating at roughly 150M daily users, with a formally verified domain core. It turns critical business rules, including membership integrity, idempotent commands, cascade deletion, and event cardinality, into explicit contracts that Dafny verifies. I also added ClaimCheck natural-language contracts, so we can review whether the English business intent matches the formal specification. The result is an agent harness: an AI coding agent can implement or change the service, but it must satisfy deterministic proof checks and runtime tests before its PR is credible. It feels like a meaningful step toward reducing mechanical reviewer load while keeping humans responsible for product intent and risk.
The agent wrote buggy TypeScript.
LemmaScript's contract caught it.
The agent fixed it before surfacing the code.
//@ contract Splits total across weights so every unit is accounted for. //@ requires total >= 0 // whole units, e.g. cents //@ requires weights.length >= 1 //@ requires forall(k, 0 <= k && k < weights.length ==> weights[k] >= 0) //@ requires sum(weights) >= 1 //@ ensures sum(\result) === total // must sum to the whole function allocateNaive(total, weights) { const W = sum(weights); return weights.map(w => Math.floor(total * w / W)); // floor each share, ship }
allocate(10, [1,1,1]) → [3,3,3] · that’s 9, not 10 — a cent vanished.
//@ contract Splits total across weights so every unit is accounted for. //@ requires total >= 0 // whole units, e.g. cents //@ requires weights.length >= 1 //@ requires forall(k, 0 <= k && k < weights.length ==> weights[k] >= 0) //@ requires sum(weights) >= 1 //@ ensures sum(\result) === total // must sum to the whole function allocate(total, weights) { const W = sum(weights); const result = weights.map(w => Math.floor(total * w / W)); let left = total - sum(result); // the leftover, lost to flooring for (let k = 0; left > 0; k++, left--) result[k] += 1; // hand them back out return result; }
Hands the leftover back out — now every cent is accounted for.
If you can write it in TypeScript, you can strengthen it with LemmaScript.
No new language, no runtime cost. Contracts go wherever your code already goes, across every domain where being right actually matters.
The business logic under your app — the invariants that must hold on every request.
The core computations in your system — the right output for every input.
A fix that covers the whole class of inputs behind a vulnerability — not just the reported one.
The rules that decide what’s permitted — correct for every configuration.
- Browser
- Node
- Deno
- Bun
- Workers
- Electron
You review the spec. The agent writes the rest.
A few declarative contracts say exactly what the code must do. The implementation that satisfies them is the agent’s job — you don’t have to read it.
//@ contract Finds target in a sorted array, or reports -1. //@ requires sorted(arr) //@ ensures \result >= -1 && \result < arr.length //@ ensures \result >= 0 ==> arr[\result] === target //@ ensures \result === -1 ==> forall(k, 0 <= k && k < arr.length ==> arr[k] !== target)
Read it in seconds. This is the whole guarantee.
export function binarySearch(arr: number[], target: number): number {
let lo = 0;
let hi = arr.length - 1;
let result = -1;
while (lo <= hi) {
//@ invariant 0 <= lo && lo <= arr.length
//@ invariant -1 <= hi && hi < arr.length
//@ invariant forall(k, 0 <= k && k < lo ==> arr[k] !== target)
//@ invariant forall(k, hi < k && k < arr.length ==> arr[k] !== target)
//@ invariant result === -1 || (result >= 0 && result < arr.length && arr[result] === target)
//@ done_with result !== -1 || !(lo <= hi)
//@ decreases (hi - lo + 1).toNat
const mid = Math.floor((lo + hi) / 2);
if (arr[mid] === target) {
result = mid;
break;
} else if (arr[mid] < target) {
lo = mid + 1;
} else {
hi = mid - 1;
}
}
return result;
} Famously easy to get subtly wrong — and a pain to test. You don’t read it; the spec already says what it does.
Start your next project correct by construction.
Begin a new project on LemmaScript from the first commit. Your agent writes the contracts and iterates until the code satisfies them, so everything builds on a core you can trust. Already have a codebase? Add a contract to a single function and grow from there.
# install the LemmaScript toolchain $ npm install -g lemmascript # check your code against its contracts $ lsc check