A machine-checked boundary attack

Tests ask whether it works.
We ask whether it can fail.

A fixed-window rate limiter looks right and passes ordinary tests. At the boundary, it admits twice the advertised limit. Seven annotation lines turn the production TypeScript below into a universal claim.

Read the LemmaScript contract

The actual LemmaScript source

Seven lines turn a function into a theorem.

The shipping implementation stays ordinary TypeScript. The //@ contract is the part a human reviews—and the part LemmaScript asks Dafny to prove for every valid input.

export function admit(log: number[], now: number, W: number, limit: number): AdmitResult {
  //@ requires W >= 1
  //@ requires limit >= 0
  //@ requires log.length <= limit
  //@ requires forall(k, 0 <= k && k < log.length ==> log[k] <= now)
  // BOUND:
  //@ ensures \result.log.length <= limit
  // WINDOW-FAITHFUL:
  //@ ensures forall(k, 0 <= k && k < \result.log.length ==> now - W < \result.log[k] && \result.log[k] <= now)
  // exact decision + non-restrictive:
  //@ ensures \result.ok === (activeCount(log, now, W) < limit)
  const active = pruneWindow(log, now, W);
  if (active.length < limit) {
    return { log: [...active, now], ok: true };
  }
  return { log: active, ok: false };
}

One command

$npm run verify

> lsc check --backend=dafny verified/core.verified.tsGenerated: verified/core.verified.dfy.genRunning dafny verify...Dafny program verifier finished with 24 verified, 0 errors

Boundary trace

10 requests. 1 millisecond apart.

9.999s

fixed boundary

10.000s

Naive fixed windowobserved

0admitted

counter resets at the boundaryLIMIT 5

Verified sliding windowverified

0admitted

the full window stays visibleLIMIT 5

✓

Universal guarantee

For every monotone request stream, every half-open window(s, s + W] contains at most limit admitted requests.

SlidingWindowBound

REFUTED

FixedWindowLeaks

The plausible design has a witness against it.

Window: 10 ms
Requests: t = 9, t = 10
Limit: 1
Result: both admitted

VERIFIED

Assurance receipt

The replacement carries a compositional proof.

Source: TypeScript
Backend: Dafny
Result: 24 verified
Errors: 0

Named trust boundary

Proofs should say what they do not prove.

The clock is monotone across calls.

The per-key store updates atomically.

The verified core is the code imported by the middleware.