Introduction

Every programmer has seen it: a file you forgot to open, a socket you tried to read after closing, a database connection you used after it was freed. The program compiles, it runs, and then — at 3 AM in production — it crashes.

Typestate analysis attacks this class of bugs at the root. The key insight, introduced by Robert Strom and Shaula Yemini in 1986, is simple: encode the current lifecycle state of an object directly into its type. An unopened file has a different type than an open one. A closed connection and an active connection are distinct types. And once states are types, using an object in the wrong state becomes a type error — the kind that the compiler catches before you ever run the program.

This is not just a theoretical nicety. The Rust programming language adopted a close relative of typestate (its ownership and borrow-checker system) as a core design principle, and it is one of the main reasons Rust can guarantee memory safety without a garbage collector. Understanding typestate is understanding one of the most powerful ideas in modern type theory.

Try It

A file passes through states: Closed → Open → Closed. Each state allows only certain operations. Build a sequence of operations using the buttons, then press Check to see whether the typestate checker accepts or rejects your program.

<!-- Interactive typestate checker — file lifecycle demo -->
<p class="hint">A file starts <b>Closed</b>. Add operations using the buttons, then press <b>Check</b> to verify the sequence. Each state allows only certain operations: <code>open()</code> from Closed; <code>read()</code>, <code>write()</code>, <code>close()</code> from Open.</p>
<div class="state-bar">
  <span class="state-label">Current state</span>
  <span id="state-display" class="state-chip closed">Closed</span>
</div>
<div id="program" class="program">
  <span class="placeholder">(empty program — add operations)</span>
</div>
<div class="op-buttons">
  <button id="btn-open" type="button" title="open() — valid only in Closed state">open()</button>
  <button id="btn-read" type="button" title="read() — valid only in Open state">read()</button>
  <button id="btn-write" type="button" title="write() — valid only in Open state">write()</button>
  <button id="btn-close" type="button" title="close() — valid only in Open state">close()</button>
</div>
<div class="action-row">
  <button id="btn-check" type="button">Check</button>
  <button id="btn-reset" type="button" class="ghost">Reset</button>
</div>
<div id="status" class="status"></div>
<div id="trace" class="trace"></div>

/* Styles for the typestate checker demo */
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .8rem; line-height: 1.5; }
.state-bar { display: flex; align-items: center; gap: .5rem; margin-bottom: .6rem; }
.state-label { font-size: .8rem; font-weight: 600; color: #555; text-transform: uppercase; letter-spacing: .05em; }
.state-chip { font: 700 .82rem ui-monospace, monospace; padding: .18rem .55rem; border-radius: 5px; }
.state-chip.closed { background: #e8eef3; color: #1d3557; border: 1px solid #cdd9e3; }
.state-chip.open   { background: #d4edda; color: #155724; border: 1px solid #b8d9c3; }
.program { min-height: 2.4rem; background: #f5f7fa; border: 1px solid #dce3ec; border-radius: 8px;
           padding: .45rem .65rem; font: .85rem ui-monospace, monospace; display: flex; flex-wrap: wrap;
           gap: .3rem; align-items: center; margin-bottom: .7rem; }
.placeholder { color: #aaa; font-style: italic; font-size: .82rem; }
.op { padding: .2rem .5rem; border-radius: 5px; font: 600 .82rem ui-monospace, monospace;
      display: inline-flex; align-items: center; gap: .25rem; }
.op.ok  { background: #d4edda; color: #155724; border: 1px solid #b8d9c3; }
.op.err { background: #f8d7da; color: #721c24; border: 1px solid #f1b0b7; }
.op .x  { cursor: pointer; font-size: .95rem; opacity: .6; }
.op .x:hover { opacity: 1; }
.op-buttons { display: flex; gap: .5rem; flex-wrap: wrap; margin-bottom: .6rem; }
.op-buttons button { font: 600 .82rem ui-monospace, monospace; padding: .3rem .7rem;
                     border: 1px solid #1d3557; background: #1d3557; color: #fff;
                     border-radius: 7px; cursor: pointer; }
.op-buttons button:hover { opacity: .85; }
.action-row { display: flex; gap: .5rem; flex-wrap: wrap; margin-bottom: .5rem; }
.action-row button { font: 600 14px system-ui, sans-serif; padding: .4rem .9rem;
                     border: 1px solid #1d3557; background: #1d3557; color: #fff;
                     border-radius: 8px; cursor: pointer; }
.action-row button.ghost { background: #fff; color: #1d3557; }
.status { font-size: 1rem; font-weight: 600; min-height: 1.4em; }
.status.ok  { color: #0a7d33; }
.status.err { color: #c92f3c; }
.trace { font: .8rem ui-monospace, monospace; color: #555; margin-top: .4rem; line-height: 1.6; white-space: pre-wrap; }

const i18nFmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Typestate transitions: each state maps allowed ops to their next state.
// 'closed' allows only open(); 'open' allows read/write/close.
const TRANSITIONS = {
  closed: { open: 'open' },
  open:   { read: 'open', write: 'open', close: 'closed' }
};
// ops = list of operation names the user has added
const ops = [];
let simState = 'closed';

const programEl  = document.getElementById('program');
const stateEl    = document.getElementById('state-display');
const statusEl   = document.getElementById('status');
const traceEl    = document.getElementById('trace');

function updateStateChip(state) {
  // update the state chip label and color class
  stateEl.textContent = state === 'closed' ? 'Closed' : 'Open';
  stateEl.className = 'state-chip ' + state;
}

function renderProgram() {
  // re-draw the program strip from the ops array
  programEl.innerHTML = '';
  if (ops.length === 0) {
    programEl.innerHTML = '<span class="placeholder">(empty program — add operations)</span>';
    return;
  }
  ops.forEach((op, i) => {
    const span = document.createElement('span');
    span.className = 'op ok';
    span.innerHTML = op + '() <span class="x" data-i="' + i + '">&#x2715;</span>';
    span.querySelector('.x').addEventListener('click', () => { ops.splice(i, 1); renderProgram(); });
    programEl.appendChild(span);
    if (i < ops.length - 1) {
      const arr = document.createElement('span');
      arr.textContent = '→';
      arr.style.color = '#888';
      programEl.appendChild(arr);
    }
  });
}

function addOp(op) {
  // append one operation and clear previous check result
  ops.push(op);
  renderProgram();
  statusEl.textContent = '';
  statusEl.className = 'status';
  traceEl.textContent = '';
}

function check() {
  // walk the typestate machine and report accept or reject
  let state = 'closed';
  const lines = [];
  let errorIdx = -1;
  for (let i = 0; i < ops.length; i++) {
    const op = ops[i];
    const next = TRANSITIONS[state] && TRANSITIONS[state][op];
    if (next === undefined) {
      // operation is not in TRANSITIONS[state] — type error
      lines.push(i18nFmt('✗ %op% — illegal in state '%state%'', { op: op + '()', state: state }));
      errorIdx = i;
      break;
    }
    lines.push(i18nFmt('✓ %op%: %from% → %to%', { op: op + '()', from: state, to: next }));
    state = next;
  }
  // a well-formed program must return the file to Closed
  if (errorIdx === -1 && state !== 'closed') {
    lines.push(i18nFmt('✗ Program ends in state '%state%' (must end Closed)', { state: state }));
    errorIdx = ops.length;
  }
  traceEl.textContent = lines.join('\n');
  if (errorIdx === -1) {
    statusEl.textContent = '✓ Accepted — valid operation sequence.';
    statusEl.className = 'status ok';
  } else {
    // show the offending op in red
    statusEl.textContent = i18nFmt('✗ Rejected — %op% is illegal here.', { op: ops[errorIdx] !== undefined ? ops[errorIdx] + '()' : '?' });
    statusEl.className = 'status err';
    markError(errorIdx);
  }
  simState = state;
  updateStateChip(simState);
}

function markError(idx) {
  // style the op chip at the error index as an error
  const spans = programEl.querySelectorAll('.op');
  spans.forEach((sp, i) => {
    if (i === idx) sp.className = 'op err';
  });
}

function reset() {
  ops.length = 0;
  simState = 'closed';
  renderProgram();
  updateStateChip('closed');
  statusEl.textContent = '';
  statusEl.className = 'status';
  traceEl.textContent = '';
}

document.getElementById('btn-open').addEventListener('click', () => addOp('open'));
document.getElementById('btn-read').addEventListener('click', () => addOp('read'));
document.getElementById('btn-write').addEventListener('click', () => addOp('write'));
document.getElementById('btn-close').addEventListener('click', () => addOp('close'));
document.getElementById('btn-check').addEventListener('click', check);
document.getElementById('btn-reset').addEventListener('click', reset);

updateStateChip('closed');
Result
Console

Notice the asymmetry. Checking whether a sequence is valid is linear — walk the states one step at a time. But writing a correct program means respecting the protocol in every execution path, including branches, loops, and error handlers. That is the hard part that typestate analysis automates.

The Real Complexity

How hard is typestate analysis, really?

  • Checking one path is trivial: start at the initial state, apply each operation in sequence, reject if any step is illegal. This is O(n)O(n) in the length of the program.
  • All paths matter. Real programs have branches, loops, and exceptions. A method called inside an if might leave the object in a different state along different branches. The checker must track all possible states the object can be in at each program point — this is a dataflow analysis problem.
  • Finite state machines. If the object's lifecycle is modeled as a finite automaton with kk states, the analysis propagates sets of possible states through the control-flow graph. With nn program points, the fixpoint computation runs in O(n⋅k)O(n \cdot k) time — polynomial and practical.
  • Undecidability at the edges. If you allow the state to depend on runtime values (for example, the file is open if and only if a boolean flag is true), the analysis becomes intertwined with general dataflow, which is undecidable for arbitrary programs. Real tools either restrict the model or use sound approximations.
  • Alias analysis is the hard part. Two variables can point to the same object. If you open it through one alias and close it through another, a naive typestate checker is confused. Handling aliasing correctly — as Rust does with its borrow checker — requires solving problems related to pointer analysis, which is itself PSPACE-hard in full generality.

The result is a practical sweet spot: for the common case (single-owner, sequential state transitions), typestate checking is fast and exact. For full generality with aliasing and concurrency, it shades into the hard problems of program analysis.

Where It Matters

Typestate is not an academic curiosity — it is one of the most practically impactful ideas in type theory:

  • Rust's ownership system: Rust does not have a garbage collector. Instead, every value has a single owner, and the borrow checker enforces at compile time that you never use a value after it has been moved or dropped. This is typestate in disguise: T, &T, &mut T, and the dropped state are distinct types that the compiler tracks through the program.
  • Network protocols: a TLS connection goes through states — handshaking, established, shutdown. Encoding those states in types (as the rustls library does) means you cannot call send() before the handshake completes — the type simply does not have that method.
  • Embedded and systems programming: hardware peripherals (UART ports, DMA channels) have precise initialization sequences. Typestate lets you model "peripheral is initialized" vs. "peripheral is uninitialized" as different types, so the driver cannot be misused.
  • Cryptographic APIs: many vulnerabilities come from using a cipher object in the wrong phase — before a key is set, after finalization. Typestate-enforced APIs eliminate the whole category.
  • Database transactions: a Transaction type that transitions from Active to Committed or Rolled Back prevents double-commit bugs statically.

In all of these cases the benefit is the same: bugs that would surface at runtime — or only under specific timing conditions — become compile-time errors that cannot ship. The cost is a richer type system and sometimes more verbose code; the reward is a whole class of production incidents that simply cannot happen.

Conclusion

Typestate analysis is a beautiful marriage of two fundamental ideas: finite automata (the lifecycle of a resource is a state machine) and type theory (wrong states should be type errors). The result is that an entire category of runtime bugs — use-after-close, double-free, missing initialization — becomes structurally impossible rather than merely unlikely.

The most important production of this idea is Rust, where the ownership and borrow-checker system enforces typestate discipline for every value in the program, not just explicitly annotated resources. That is why Rust can promise memory safety without a garbage collector: the type system itself carries the proof.

The next time you see a Rust compiler error that says "value used after move," you are not looking at an annoying restriction. You are looking at a type error that, in any other language, would have been a segfault waiting to happen at 3 AM.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/typestate-analysis/Content licensed under CC BY-NC 4.0.