Skip to content
Get our updates
✓ Thanks for subscribing!
← Back to Posts

LemmaScript contracts by example

Nada Amin

We show examples of contracts from the LemmaScript case studies.

Verified contracts

LemmaScript contracts are written as structured comment annotations and have no effect on the TypeScript runtime: the executable pipeline remains intact while the verification pipeline runs in parallel to check the implementation against its contracts. The core vocabulary is as follows:

  • requires e and ensures e state pre- and postconditions; \result names the return value in an ensures.
  • invariant e and decreases e give loop invariants and termination measures; decreases also applies to recursive functions.
  • contract text states the function’s intent in prose. It never reaches the prover; it is read back by Claimcheck, which compares the formal specification with what the prose claims.
  • verify marks a function for verification. By default, lsc extracts every function in a file; if any function carries //@ verify, only marked functions are extracted. This selective mode is how existing files are verified in place, since many of their functions may fall outside the supported subset.

In the Hono rate limiter, pruneWindow keeps admissions inside the sliding time window (now - W, now]:

//@ contract Keeps only the requests still inside the sliding time window.
export function pruneWindow(log: number[], now: number, W: number): number[] {
  //@ requires forall(k, 0 <= k && k < log.length ==> log[k] <= now)
  //@ decreases log.length
  //@ ensures \result.length <= log.length
  //@ ensures forall(k, 0 <= k && k < \result.length ==> now - W < \result[k] && \result[k] <= now)
  //@ ensures \result.length === CountIn(log, now, W)
  if (log.length === 0) {
    return [];
  }
  const rest = pruneWindow(log.slice(1), now, W);
  if (log[0] > now - W) {
    return [log[0], ...rest];
  }
  return rest;
}

The ensures clauses guarantee soundness (each entry is in the window) and near completeness (result has the exact count). Without the near completeness ensures clause, returning the empty result all the time would be an acceptable implementation.

Finding and fixing errors

The verification feedback, from running the verifier on the intermediary Dafny where the contract is proved to be satisfied against a model of the TypeScript code, can guide an agent in developing a correct solution.

For example, in Eventab, the allocate contract was initially implemented naively by the agent:

//@ 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
}

But verification failed. A counterexample: For total = 100 and weights = [1, 1, 1], flooring each share gives [33, 33, 33]. One unit is lost, so the conservation postcondition fails. Through the verifier feedback, the agent wrote a corrected version that distributes the leftover:

//@ 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;
}

The contract stays the same. The implementation changes so that every unit is accounted for. This correction happened without a human in the loop.

Specifying rounding policy

For Eventab, the allocate contract is the simplest instance of arithmetic conservation. The functionality was iterated on with the guidance of the user, to satisfy the app requirements of bill splitting, to reach the following function after several iterations:

export function settleRounded(balances: number[], hub: number, G: number): number[] {
  //@ contract Routes settlement through the hub but rounds each non-hub transfer to a whole multiple of G (the hub absorbs the leftover); each non-hub transfer equals its rounded balance and the transfers sum to zero.
  //@ requires balances.length >= 1
  //@ requires 0 <= hub && hub < balances.length
  //@ requires G >= 1
  //@ ensures \result.length === balances.length
  //@ ensures forall(p, 0 <= p && p < \result.length && p !== hub ==> \result[p] === roundToG(balances[p], G))
  //@ ensures sumTo(\result, \result.length) === 0
  // ... implementation
}

The contract records the rounding policy: each participant other than the hub gets a transfer equal to their balance rounded by roundToG, and the hub absorbs the leftover so the transfers sum to zero. G is the rounding granularity, and sumTo sums the transfers up to the given length.

Preserving state invariants

If all state change goes through either an initializer or a step function, and we can prove that each initializer establishes a state invariant and each step function preserves the invariant, then we have a global state invariant. We can encode a lot of the correctness of an application in such an invariant.

For example, this is the invariant of a session state in Henri, a coding agent. It states what every reachable session state satisfies: the transcript is well-formed; a batch in flight is nonempty, has an unanswered call, and its results pair with its calls; a pending compaction cut is a safe boundary.

export function inv(st: Session): boolean {
  //@ verify
  const ph = st.phase;
  if (ph.kind === "toolBatch" || ph.kind === "awaitingPrompt") {
    return (
      wellFormed(st.msgs) &&
      ph.calls.length > 0 &&
      ph.done.length < ph.calls.length &&
      pairsTo(projectCalls(ph.calls), ph.done)
    );
  }
  if (ph.kind === "awaitingSummary") {
    return (
      wellFormed(st.msgs) &&
      0 < ph.cut &&
      ph.cut <= st.msgs.length &&
      (ph.cut === st.msgs.length || headOk(st.msgs[ph.cut]))
    );
  }
  return wellFormed(st.msgs);
}

In addition to the initial state satisfying the invariant, there is a lemma that states that every step preserves it.

export function stepPreservesInv(st: Session, ev: SEvent): boolean {
  //@ verify
  //@ contract The session invariant survives every event -- interrupts mid-stream and mid-batch, prompt answers, and compaction included.
  //@ requires inv(st)
  //@ ensures inv(step(st, ev).st)
  return true;
}

step(st, ev) computes the next state and the commands to issue. The lemma requires inv(st) and ensures that the next state satisfies the same invariant, for every event.

A lemma function can have a body that only returns true. Its postcondition states a property to be proved, independently of that return value. Returning true does not discharge the obligation: the agent supplies any needed proof steps in the generated verification model, and the verifier checks them.

Order independence

In Quorum, permutation invariance of the heatmap justifies accepting participants in any order:

export function heatmapPermInvariant(a: Event, b: Event): boolean {
  //@ verify
  //@ contract Two events whose participant lists are permutations of each other have identical heatmaps.
  //@ requires a.numSlots >= 0 && a.numSlots === b.numSlots
  //@ requires perm(a.participants, b.participants)
  //@ ensures heatmap(a).length === a.numSlots
  //@ ensures heatmap(b).length === b.numSlots
  //@ ensures forall(s, 0 <= s && s < a.numSlots ==> heatmap(a)[s] === heatmap(b)[s])
  return true
}

The two events have the same number of slots, and their participant lists are permutations of each other. The postconditions say that the heatmaps have the expected length and agree at every slot.

More generally, proving that operations commute establishes that their order does not affect the resulting state. This supports concurrent execution through a surrounding protocol that ensures replicas apply the same operations atomically, assuming replicas start from the same state.

Soundness and completeness

Equality Game asks whether two lists of number cards can be made equal using arithmetic expressions. Its decision procedure is sound and complete with respect to an abstract predicate, ExpressionsAgree. The statement is a single postcondition:

export function canEqualize(L: number[], R: number[]): boolean {
  //@ contract A sound and complete decision procedure for whether the two card lists can be equalized -- returns true exactly when expressions over L and R can agree.
  //@ requires L.length >= 1
  //@ requires R.length >= 1
  //@ ensures \result <==> ExpressionsAgree(L, R)

  const sL = reachable(L);
  const sR = reachable(R);
  for (const v of sL) {
    if (sR.has(v)) return true;
  }
  return false;
}

ExpressionsAgree(L, R) says that there are valid expressions using the cards on each side that evaluate to the same number. The <==> means “if and only if”: when canEqualize returns true, such expressions exist; when it returns false, no such expressions exist. The contract establishes both that the procedure accepts valid instances and that it rejects invalid ones.

Mediating tool execution

In Henri (a verified agent CLI), sessions are factored out explicitly so that mediation can be stated over a step function:

export function stepMediation(st: Session, ev: SEvent, i: number): boolean {
  //@ verify
  //@ contract Mediation: in any invariant-satisfying state, for any event -- provider tool calls included, so prompt injection is in scope -- every execTool command the step emits is justified; there is no unjustified path to an effect.
  //@ requires inv(st)
  //@ requires 0 <= i && i < step(st, ev).cmds.length
  //@ requires step(st, ev).cmds[i].kind === "execTool"
  //@ ensures justified(st, step(st, ev).st, ev, step(st, ev).cmds[i].call)
  return true;
}

This factoring follows the functional programming pattern of “interpreter”, where commands are explicit objects that are interpreted to separate logic (the creation of the command) from the effect.

The postcondition states that for any state satisfying the invariant and any event, every emitted execTool command must satisfy the policy’s justified relation. Provider tool calls are included among those events. The guarantee concerns the commands emitted by the verified session logic; the surrounding runtime executes the actual tools.

From a static check to a safety guarantee

The capstone lemma of Guardians shows that a static workflow check implies concrete safety: no leak to a sink and no reachable automaton error.

export function verifyWfSound(
  introduces: (tool: number) => boolean,
  sanitizes: (tool: number) => boolean,
  isSink: (tool: number) => boolean,
  isTarget: (tool: number) => boolean,
  chooseThen: (wf: Wf) => boolean,
  t0: boolean,
  wf: Wf,
): boolean {
  //@ verify
  //@ ensures verifyWf(introduces, sanitizes, isSink, isTarget, t0, wf) ==> (!leaksWfConcrete(introduces, sanitizes, isSink, chooseThen, t0, wf) && !reachesTargetWfConcrete(isTarget, chooseThen, wf))
  return true;
}

The function arguments classify tools: which introduce taint, which sanitize it, which are sinks, and which are forbidden targets. t0 is the initial taint state. The workflow wf can contain nested conditionals, and chooseThen selects the branch taken at each conditional.

The static checker considers both branches. Its acceptance implies that the concrete execution has neither a taint leak to a sink nor a forbidden target, for any supplied branch-selection function. The guarantee is relative to the modeled workflow and the declared tool classifications.

Conclusion

These examples are fairly diverse, and help humans and agents think about the correctness of the code. In general, it’s easier to read a contract than it is to reason through whether the code satisfies it, and this is the payoff and guarantee of verification.