Skip to main content
// built for agents

LemmaScript is TypeScript with syntax for contracts.

core.verified.ts// real code ↗Guaranteed
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}
Get started Read the docs
// caught in the act

The agent wrote buggy TypeScript.
LemmaScript's contract caught it.
The agent fixed it before surfacing the code.

Rejectedthe agent’s first try
allocateNaive.ts// real 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.

Guaranteedthe agent’s fix
allocate.ts// real 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 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.

// wherever you write typescript

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.

Web apps

The business logic under your app — the invariants that must hold on every request.

Algorithms

The core computations in your system — the right output for every input.

Security patches

A fix that covers the whole class of inputs behind a vulnerability — not just the reported one.

Agents

The rules that decide what’s permitted — correct for every configuration.

It’s TypeScript — so it runs anywhere TypeScript runs.
  • Browser
  • Node
  • Deno
  • Bun
  • Workers
  • Electron
// review intent, not implementation

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.

What you reviewthe spec · 5 lines
binarySearch.ts// real code ↗
//@ 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.

What the agent writesa while-loop with 7 spec lines
binarySearch.ts
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.

// get started

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.

Read the quickstart → View on GitHub
terminal
# install the LemmaScript toolchain
$ npm install -g lemmascript

# check your code against its contracts
$ lsc check