diff --git a/conformance/typescript/machine/out/switch.ts b/conformance/typescript/machine/out/switch.ts
new file mode 100644
index 0000000..a4d9f45
--- /dev/null
+++ b/conformance/typescript/machine/out/switch.ts
@@ -0,0 +1,98 @@
+// Generated by accord from switch.accord. Do not edit.
+// Every obligation of these functions is proved. This TypeScript is not
+// proved equivalent to them: Accord tests its code generator against its
+// interpreter.
+// Each exported function checks its parameters and its `requires`, and
+// throws a TypeError or a RangeError when one doesn't hold.
+// A machine's events and observers also check that the state they are given
+// has its fields and meets every invariant and helper invariant. An event
+// returns the next state and leaves the one it is given unchanged.
+
+export type Light = "off" | "on";
+
+export type Switch = {
+  readonly light: Light;
+  readonly presses: number;
+};
+
+function checkSwitch$(where$: string, state$: Switch): Switch {
+  if (typeof state$ !== "object" || state$ === null) {
+    throw new TypeError(`${where$}: state must be a Switch`);
+  }
+  const { light, presses } = state$;
+  if (!["off", "on"].includes(light)) {
+    throw new TypeError(`${where$}: state.light must be a Light`);
+  }
+  if (typeof presses !== "number") {
+    throw new TypeError(`${where$}: state.presses must be an i32`);
+  }
+  if (!Number.isInteger(presses) || presses < -2147483648 || presses > 2147483647) {
+    throw new RangeError(`${where$}: state.presses must be an i32`);
+  }
+  if (!((BigInt(presses) >= 0n) && (BigInt(presses) <= 100n))) {
+    throw new RangeError(`${where$}: state breaks invariant pressed: presses >= 0 and presses <= 100`);
+  }
+  if (!(!(light === "on") || (BigInt(presses) > 0n))) {
+    throw new RangeError(`${where$}: state breaks helper invariant on_means_pressed: light == On implies presses > 0`);
+  }
+  return { light, presses };
+}
+
+export function start(): Switch {
+  return start$();
+}
+
+function start$(): Switch {
+  return { light: "off", presses: 0 };
+}
+
+export function resume(fromLight: Light, fromPresses: number): Switch {
+  if (!["off", "on"].includes(fromLight)) {
+    throw new TypeError("resume: fromLight must be a Light");
+  }
+  if (typeof fromPresses !== "number") {
+    throw new TypeError("resume: fromPresses must be an i32");
+  }
+  if (!Number.isInteger(fromPresses) || fromPresses < -2147483648 || fromPresses > 2147483647) {
+    throw new RangeError("resume: fromPresses must be an i32");
+  }
+  if (!(((BigInt(fromPresses) >= 0n) && (BigInt(fromPresses) <= 100n)) && ((fromLight === "off") || (BigInt(fromPresses) > 0n)))) {
+    throw new RangeError("resume: requires from_presses >= 0 and from_presses <= 100 and (from_light == Off or from_presses > 0)");
+  }
+  return resume$(fromLight, fromPresses);
+}
+
+function resume$(fromLight: Light, fromPresses: number): Switch {
+  return { light: fromLight, presses: fromPresses };
+}
+
+export function press(state$: Switch): Switch {
+  const { light, presses } = checkSwitch$("press", state$);
+  if (!(BigInt(presses) < 100n)) {
+    throw new RangeError("press: requires presses < 100");
+  }
+  return press$(light, presses);
+}
+
+function press$(light: Light, presses: number): Switch {
+  if (light === "off") return { light: "on", presses: presses + 1 };
+  return { light: "off", presses: presses + 1 };
+}
+
+export function turnOff(state$: Switch): Switch {
+  const { light, presses } = checkSwitch$("turnOff", state$);
+  return turnOff$(light, presses);
+}
+
+function turnOff$(light: Light, presses: number): Switch {
+  return { light: "off", presses: presses };
+}
+
+export function atLimit(state$: Switch): boolean {
+  const { light, presses } = checkSwitch$("atLimit", state$);
+  return atLimit$(light, presses);
+}
+
+function atLimit$(light: Light, presses: number): boolean {
+  return presses === 100;
+}
diff --git a/conformance/typescript/machine/src/switch.accord b/conformance/typescript/machine/src/switch.accord
new file mode 100644
index 0000000..c31c2e5
--- /dev/null
+++ b/conformance/typescript/machine/src/switch.accord
@@ -0,0 +1,47 @@
+/// Whether the light is on.
+pub enum Light { Off, On }
+
+/// A switch that counts its presses.
+pub machine Switch {
+    state {
+        light: Light,
+        presses: i32,
+    }
+
+    init start() {
+        next { light: Off, presses: 0 }
+    }
+
+    init resume(from_light: Light, from_presses: i32)
+        requires from_presses >= 0 and from_presses <= 100 and (from_light == Off or from_presses > 0)
+    {
+        next { light: from_light, presses: from_presses }
+    }
+
+    event press()
+        requires presses < 100
+    decide {
+        | light == Off => next { light: On, presses: presses + 1 }
+        | otherwise    => next { light: Off, presses: presses + 1 }
+    }
+
+    event turn_off() {
+        next { light: Off }
+    }
+
+    /// Whether the switch has reached its limit.
+    fn at_limit() -> Bool
+        ensures result implies presses == 100
+    {
+        presses == 100
+    }
+
+    invariant pressed: presses >= 0 and presses <= 100
+
+    helper invariant on_means_pressed: light == On implies presses > 0
+}
+
+example Switch
+    start()
+    press()
+    gives light == On and presses == 1
diff --git a/conformance/typescript/refused-machine/src/pair.accord b/conformance/typescript/refused-machine/src/pair.accord
new file mode 100644
index 0000000..5f0ca73
--- /dev/null
+++ b/conformance/typescript/refused-machine/src/pair.accord
@@ -0,0 +1,18 @@
+pub machine Pair {
+    state {
+        x: i32,
+        y: i32,
+    }
+
+    init start() {
+        next { x: 0, y: 0 }
+    }
+
+    event step()
+        requires x < 3
+    {
+        next { x: x + 1, y: y + 1 }
+    }
+
+    invariant y_bounded: y <= 3
+}
diff --git a/crates/accord/src/evidence/machine.rs b/crates/accord/src/evidence/machine.rs
index 967f42b..675e24b 100644
--- a/crates/accord/src/evidence/machine.rs
+++ b/crates/accord/src/evidence/machine.rs
@@ -11,7 +11,7 @@ use crate::obligation::{self, Claim, Obligation};
 use crate::syntax::{Machine, Program, Role};
 use crate::{
     Definition, DefinitionKind, ExampleRun, Exploration, Inputs, ObligationKind, Outcome,
-    Refutation, Run, Solvers, Standing, TraceStep, Verdict, identity, syntax,
+    Refutation, Run, Solvers, Standing, TraceStep, Verdict, identity,
 };
 
 /// What checking a machine established, short of its standing.
@@ -27,17 +27,9 @@ pub(super) struct Checked {
 /// machine's observers as functions known by their contracts, without the
 /// invariants they assume.
 fn callee_view(program: &Program, machine: &Machine) -> Program {
-    let mut functions = program.functions.clone();
-    for observer in &machine.observers {
-        let mut callee = observer.clone();
-        callee
-            .clauses
-            .retain(|c| c.kind != syntax::ClauseKind::Invariant);
-        functions.push(callee);
-    }
     Program {
         enums: program.enums.clone(),
-        functions,
+        functions: machine.functions(&program.functions),
         machines: Vec::new(),
         examples: Vec::new(),
         machine_examples: Vec::new(),
diff --git a/crates/accord/src/syntax.rs b/crates/accord/src/syntax.rs
index 098c760..8303217 100644
--- a/crates/accord/src/syntax.rs
+++ b/crates/accord/src/syntax.rs
@@ -301,6 +301,19 @@ pub(crate) struct Machine {
 }
 
 impl Machine {
+    /// The functions a member of this machine may call: `globals`, and the
+    /// machine's observers as callees know them, without the invariants they
+    /// assume of the state they read.
+    pub fn functions(&self, globals: &[Function]) -> Vec<Function> {
+        let mut functions = globals.to_vec();
+        for observer in &self.observers {
+            let mut callee = observer.clone();
+            callee.clauses.retain(|c| c.kind != ClauseKind::Invariant);
+            functions.push(callee);
+        }
+        functions
+    }
+
     /// Inits, then events, then observers: the order of the machine's
     /// obligations.
     pub fn members(&self) -> impl Iterator<Item = &Function> {
diff --git a/crates/accord/src/typescript.rs b/crates/accord/src/typescript.rs
index 791b0cf..3c7594f 100644
--- a/crates/accord/src/typescript.rs
+++ b/crates/accord/src/typescript.rs
@@ -14,9 +14,9 @@ mod lists;
 use std::collections::BTreeMap;
 
 use crate::openness::{Determinacy, Openness};
-use crate::syntax::{Body, Enum, Function, Program, Type, Width};
+use crate::syntax::{Body, Enum, Expr, Function, Machine, Program, Role, Type, Width};
 use crate::{Diagnostic, Outcome, Report, Run, Solvers};
-use boundary::{TEXT_CHECK, wrapper};
+use boundary::{TEXT_CHECK, state_check, state_type, wrapper};
 use expr::{Context, Scope, camel, string};
 
 const HEADER: &str = "// Every obligation of these functions is proved. This TypeScript is not
@@ -26,6 +26,12 @@ const HEADER: &str = "// Every obligation of these functions is proved. This Typ
 // throws a TypeError or a RangeError when one doesn't hold.
 ";
 
+const MACHINE_HEADER: &str =
+    "// A machine's events and observers also check that the state they are given
+// has its fields and meets every invariant and helper invariant. An event
+// returns the next state and leaves the one it is given unchanged.
+";
+
 /// One generated TypeScript module.
 #[derive(Clone, Debug, PartialEq)]
 pub struct Module {
@@ -60,16 +66,7 @@ fn proved(report: &Report) -> bool {
 /// names the functions that have one.
 pub fn build(files: &[(String, String)], solvers: &Solvers) -> Result<Build, Diagnostic> {
     let (program, names) = crate::program_of(files)?;
-    if let Some(machine) = program.machines.first() {
-        return Err(Diagnostic::new(
-            machine.line,
-            format!(
-                "`{}` is a machine: machines aren't written as TypeScript yet",
-                machine.name
-            ),
-        )
-        .in_file(&names[machine.file]));
-    }
+    check_exports(&program, &names)?;
     let report = crate::report(&program, None, &names, solvers);
     let modules = proved(&report).then(|| {
         modules(&program, &names, &report.openness)
@@ -80,6 +77,66 @@ pub fn build(files: &[(String, String)], solvers: &Solvers) -> Result<Build, Dia
     Ok(Build { report, modules })
 }
 
+/// The public machines declared in `file`.
+fn machines(program: &Program, file: usize) -> Vec<&Machine> {
+    program
+        .machines
+        .iter()
+        .filter(|m| m.file == file && m.public)
+        .collect()
+}
+
+/// Rejects a file whose module would declare one name twice: an exported
+/// function, a function's body or a machine's check, whichever it comes from.
+fn check_exports(program: &Program, names: &[String]) -> Result<(), Diagnostic> {
+    for (file, name) in names.iter().enumerate() {
+        let functions: Vec<&Function> = program
+            .functions
+            .iter()
+            .filter(|f| f.file == file && f.public)
+            .collect();
+        let mut declared: Vec<(String, usize)> = Vec::new();
+        let mut members: Vec<&Function> = Vec::new();
+        for function in &functions {
+            let exported = camel(&function.name);
+            declared.push((format!("{exported}$"), function.line));
+            declared.push((exported, function.line));
+        }
+        for e in program.enums.iter().filter(|e| e.file == file) {
+            declared.push((format!("type {}", e.name), e.line));
+        }
+        for machine in machines(program, file) {
+            declared.push((format!("type {}", machine.name), machine.line));
+            declared.push((format!("check{}$", machine.name), machine.line));
+            for member in machine.members() {
+                let exported = camel(&member.name);
+                declared.push((format!("{exported}$"), member.line));
+                declared.push((exported, member.line));
+                members.push(member);
+            }
+        }
+        let all: Vec<&Function> = functions.iter().chain(&members).copied().collect();
+        declared.extend(
+            called(program, &all)
+                .iter()
+                .map(|f| (format!("{}$", camel(&f.name)), f.line)),
+        );
+        for (index, (declaration, line)) in declared.iter().enumerate() {
+            if declared[..index]
+                .iter()
+                .any(|(other, _)| other == declaration)
+            {
+                return Err(Diagnostic::new(
+                    *line,
+                    format!("`{declaration}` is declared twice in the module this file becomes"),
+                )
+                .in_file(name));
+            }
+        }
+    }
+    Ok(())
+}
+
 /// The modules for `program`'s files, named after `names`, in their order.
 fn modules(program: &Program, names: &[String], openness: &[Determinacy]) -> Vec<(String, String)> {
     names
@@ -98,10 +155,15 @@ fn module(program: &Program, names: &[String], file: usize, openness: &[Determin
         .iter()
         .filter(|f| f.file == file && f.public)
         .collect();
+    let machines = machines(program, file);
+    let members: Vec<&Function> = machines.iter().flat_map(|m| m.members()).collect();
     let mut out = format!(
         "// Generated by accord from {}. Do not edit.\n{HEADER}",
         names[file]
     );
+    if !machines.is_empty() {
+        out += MACHINE_HEADER;
+    }
     for function in &functions {
         let found = openness.iter().find(|d| d.function == function.name);
         match found.map(|d| &d.openness) {
@@ -121,7 +183,8 @@ fn module(program: &Program, names: &[String], file: usize, openness: &[Determin
         }
     }
     let mut items = Vec::new();
-    let imports = imports(program, names, file, &functions);
+    let everything: Vec<&Function> = functions.iter().chain(&members).copied().collect();
+    let imports = imports(program, names, file, &everything);
     if !imports.is_empty() {
         items.push(imports);
     }
@@ -135,15 +198,31 @@ fn module(program: &Program, names: &[String], file: usize, openness: &[Determin
     }
     let mut text = false;
     for function in &functions {
-        let (wrapper, uses_text) = wrapper(program, function);
+        let (wrapper, uses_text) = wrapper(program, function, None);
         text |= uses_text;
         items.push(wrapper);
-        items.push(core(function, program));
+        items.push(core(function, program, &program.functions));
+    }
+    for machine in &machines {
+        items.push(state_type(machine));
+        let (check, uses_text) = state_check(program, machine);
+        text |= uses_text;
+        items.push(check);
+        let callable = machine.functions(&program.functions);
+        for member in machine.members() {
+            let (wrapper, uses_text) = wrapper(program, member, Some(machine));
+            text |= uses_text;
+            items.push(wrapper);
+            items.push(match member.machine.map(|m| m.role) {
+                Some(Role::Observer) => core(member, program, &callable),
+                _ => transition_core(member, machine, program, &callable),
+            });
+        }
     }
     // A called function's body is written into every module that calls it,
     // unexported, so no module exports an unchecked entry point.
-    for function in called(program, &functions) {
-        items.push(core(function, program));
+    for function in called(program, &everything) {
+        items.push(core(function, program, &program.functions));
     }
     if text {
         items.push(TEXT_CHECK.to_string());
@@ -255,13 +334,116 @@ fn signature(function: &Function, name: &str, ty: fn(&Type) -> String) -> String
     format!("{name}({}): {}", params.join(", "), ty(&function.ret))
 }
 
-/// The function's body, unexported; it may call the program's functions.
-fn core(function: &Function, program: &Program) -> String {
+/// The body of an init or event, unexported: it takes the state's fields,
+/// for an event, then its own parameters, and returns the next state.
+fn transition_core(
+    function: &Function,
+    machine: &Machine,
+    program: &Program,
+    functions: &[Function],
+) -> String {
+    let skip = match function.machine {
+        Some(member) if member.role == Role::Init => member.state,
+        _ => 0,
+    };
+    let params: Vec<String> = function.params[skip..]
+        .iter()
+        .map(|(n, t)| format!("{}: {}", camel(n), inner(t)))
+        .collect();
+    let code = Scope {
+        params: &function.params,
+        context: Context::Code,
+        functions,
+        enums: &program.enums,
+        indices: &[],
+    };
+    let mut out = format!(
+        "function {}$({}): {} {{\n",
+        camel(&function.name),
+        params.join(", "),
+        machine.name
+    );
+    match &function.body {
+        Body::Expr(body) => out += &transition(&code, machine, body, "  "),
+        Body::Decide(rows, _) => {
+            for row in rows {
+                out += &match &row.condition {
+                    Some(condition) => {
+                        let condition = code.bare(condition, None);
+                        branch(&code, machine, &condition, &row.result, "  ")
+                    }
+                    None => transition(&code, machine, &row.result, "  "),
+                };
+            }
+            if rows.last().is_some_and(|row| row.condition.is_some()) {
+                out += &format!(
+                    "  throw new Error({});\n",
+                    string(&format!("{}: no row matched", camel(&function.name)))
+                );
+            }
+        }
+    }
+    out + "}\n"
+}
+
+/// The statements that return the state an `if`, or a `next`, ends in.
+fn transition(code: &Scope, machine: &Machine, expr: &Expr, indent: &str) -> String {
+    match expr {
+        Expr::If(condition, then, otherwise) => {
+            let condition = code.bare(condition, None);
+            branch(code, machine, &condition, then, indent)
+                + &transition(code, machine, otherwise, indent)
+        }
+        Expr::Next(fields, _) => {
+            format!("{indent}return {};\n", state_object(code, machine, fields))
+        }
+        _ => unreachable!("`check` ends every init and event in a `next`"),
+    }
+}
+
+/// `if (condition)` and what returns the state `then` ends in.
+fn branch(code: &Scope, machine: &Machine, condition: &str, then: &Expr, indent: &str) -> String {
+    match then {
+        Expr::Next(fields, _) => format!(
+            "{indent}if ({condition}) return {};\n",
+            state_object(code, machine, fields)
+        ),
+        _ => format!(
+            "{indent}if ({condition}) {{\n{}{indent}}}\n",
+            transition(code, machine, then, &format!("{indent}  "))
+        ),
+    }
+}
+
+/// The state as an object literal, every field in the state's order.
+fn state_object(code: &Scope, machine: &Machine, fields: &[(String, Expr)]) -> String {
+    let parts: Vec<String> = fields
+        .iter()
+        .zip(&machine.state)
+        .map(|((_, value), (field, ty))| {
+            let want = match ty {
+                Type::Int(width) => Some(*width),
+                _ => None,
+            };
+            let value = code.bare(value, want);
+            let value = if *ty == Type::Int(Width::I64) {
+                format!("Number({value})")
+            } else {
+                value
+            };
+            format!("{}: {value}", camel(field))
+        })
+        .collect();
+    format!("{{ {} }}", parts.join(", "))
+}
+
+/// The function's body, unexported; it may call `functions`.
+fn core(function: &Function, program: &Program, functions: &[Function]) -> String {
     let name = format!("{}$", camel(&function.name));
     let code = Scope {
         params: &function.params,
         context: Context::Code,
-        functions: &program.functions,
+        functions,
         enums: &program.enums,
         indices: &[],
     };
diff --git a/crates/accord/src/typescript/boundary.rs b/crates/accord/src/typescript/boundary.rs
index 9e24b4f..710aa2b 100644
--- a/crates/accord/src/typescript/boundary.rs
+++ b/crates/accord/src/typescript/boundary.rs
@@ -1,10 +1,14 @@
 //! The exported function: it checks what the proofs assume of its caller,
 //! its parameters' types and ranges and each `requires`, and then calls the
 //! body. Integers in a `requires` are mathematical, so they are `bigint`s.
+//!
+//! A machine's state is a `readonly` object of its fields. An event or
+//! observer takes it first and checks it, its fields and then every
+//! invariant and helper invariant, before it checks anything else.
 
 use super::expr::{Context, Scope, camel, string};
-use super::{enumeration, outer, signature};
-use crate::syntax::{ClauseKind, Function, Program, Type, Width};
+use super::{enumeration, outer};
+use crate::syntax::{ClauseKind, Function, Machine, Program, Role, Type, Width};
 
 pub(super) const TEXT_CHECK: &str = "function isText$(value: string): boolean {
   for (const character of value) {
@@ -19,21 +23,42 @@ pub(super) const TEXT_CHECK: &str = "function isText$(value: string): boolean {
 
 const TEXT_RANGE: &str = "must hold only characters up to U+2FFFF, with no lone surrogates";
 
+/// A template literal that starts with `${where}: `, so a check of a state
+/// says which exported function it runs for. The message is escaped.
+fn template(message: &str) -> String {
+    let mut out = String::from("`${where$}: ");
+    for c in message.chars() {
+        if matches!(c, '\\' | '`' | '$') {
+            out.push('\\');
+        }
+        out.push(c);
+    }
+    out.push('`');
+    out
+}
+
+/// An `if` that throws `error` with the message, a literal, when `check`.
 fn throw(check: &str, error: &str, message: &str) -> String {
-    format!(
-        "  if ({check}) {{\n    throw new {error}({});\n  }}\n",
-        string(message)
-    )
+    format!("  if ({check}) {{\n    throw new {error}({message});\n  }}\n")
 }
 
-/// The exported function, and whether it checks a text.
-pub(super) fn wrapper(program: &Program, function: &Function) -> (String, bool) {
-    let name = camel(&function.name);
-    let mut out = format!("export function {} {{\n", signature(function, &name, outer));
+/// How a check words what it found.
+struct Words<'a> {
+    /// What the value is called in a message, given its variable.
+    subject: &'a dyn Fn(&str) -> String,
+    /// A message as a TypeScript literal.
+    render: &'a dyn Fn(&str) -> String,
+}
+
+/// The checks of `params`' types and ranges, one `if` each, and whether any
+/// is of a text. Each parameter is a variable of its camel-case name.
+fn param_checks(program: &Program, params: &[(String, Type)], words: &Words) -> (String, bool) {
+    let mut out = String::new();
     let mut text = false;
-    for (param, ty) in &function.params {
+    for (param, ty) in params {
         let p = camel(param);
-        let must = |what: &str| format!("{name}: {p} must be {what}");
+        let subject = (words.subject)(&p);
+        let must = |what: &str| (words.render)(&format!("{subject} must be {what}"));
         let variants = |enum_name: &str| -> String {
             let e = enumeration(program, enum_name).expect("`check` resolves every enum");
             let values: Vec<String> = e.variants.iter().map(|v| string(&e.text(v))).collect();
@@ -81,7 +106,7 @@ pub(super) fn wrapper(program: &Program, function: &Function) -> (String, bool)
                 out += &throw(
                     &format!("!isText$({p})"),
                     "RangeError",
-                    &format!("{name}: {p} {TEXT_RANGE}"),
+                    &(words.render)(&format!("{subject} {TEXT_RANGE}")),
                 );
             }
             Type::Enum(e) => {
@@ -105,12 +130,115 @@ pub(super) fn wrapper(program: &Program, function: &Function) -> (String, bool)
                     out += &throw(
                         &format!("!{p}.every(isText$)"),
                         "RangeError",
-                        &format!("{name}: {p} {TEXT_RANGE}"),
+                        &(words.render)(&format!("{subject} {TEXT_RANGE}")),
                     );
                 }
             }
         }
     }
+    (out, text)
+}
+
+/// The fields as a comma-separated list of camel-case names.
+fn field_names(machine: &Machine) -> String {
+    let names: Vec<String> = machine.state.iter().map(|(n, _)| camel(n)).collect();
+    names.join(", ")
+}
+
+/// The machine's state as a type: its fields, in order.
+pub(super) fn state_type(machine: &Machine) -> String {
+    let mut out = format!("export type {} = {{\n", machine.name);
+    for (field, ty) in &machine.state {
+        out += &format!("  readonly {}: {};\n", camel(field), outer(ty));
+    }
+    out + "};\n"
+}
+
+/// The function that checks a state: that it is an object with the fields'
+/// types and ranges, and that it meets every invariant and then every helper
+/// invariant. Also whether it checks a text.
+pub(super) fn state_check(program: &Program, machine: &Machine) -> (String, bool) {
+    let name = &machine.name;
+    let mut out = format!("function check{name}$(where$: string, state$: {name}): {name} {{\n");
+    out += &throw(
+        "typeof state$ !== \"object\" || state$ === null",
+        "TypeError",
+        &template(&format!("state must be a {name}")),
+    );
+    out += &format!("  const {{ {} }} = state$;\n", field_names(machine));
+    let (checks, text) = param_checks(
+        program,
+        &machine.state,
+        &Words {
+            subject: &|field| format!("state.{field}"),
+            render: &template,
+        },
+    );
+    out += &checks;
+    let spec = Scope {
+        params: &machine.state,
+        context: Context::Spec,
+        functions: &[],
+        enums: &program.enums,
+        indices: &[],
+    };
+    for helper in [false, true] {
+        for invariant in machine.invariants.iter().filter(|c| c.helper == helper) {
+            let check = format!("!({})", spec.bare(&invariant.expr, None));
+            out += &throw(
+                &check,
+                "RangeError",
+                &template(&format!("state breaks {}", invariant.text)),
+            );
+        }
+    }
+    out += &format!("  return {{ {} }};\n", field_names(machine));
+    (out + "}\n", text)
+}
+
+/// The exported function of a function, or of a machine's init, event or
+/// observer, and whether it checks a text. An event or observer takes the
+/// machine's state first; an init has none to take.
+pub(super) fn wrapper(
+    program: &Program,
+    function: &Function,
+    machine: Option<&Machine>,
+) -> (String, bool) {
+    let name = camel(&function.name);
+    let role = function.machine.map(|m| m.role);
+    let state = function.machine.map_or(0, |m| m.state);
+    let reads_state = role.is_some_and(|r| r != Role::Init);
+    let own = &function.params[state..];
+    let ret = match (role, machine) {
+        (Some(Role::Init | Role::Event), Some(machine)) => machine.name.clone(),
+        _ => outer(&function.ret),
+    };
+    let mut params: Vec<String> = Vec::new();
+    if let (true, Some(machine)) = (reads_state, machine) {
+        params.push(format!("state$: {}", machine.name));
+    }
+    params.extend(
+        own.iter()
+            .map(|(n, t)| format!("{}: {}", camel(n), outer(t))),
+    );
+    let mut out = format!("export function {name}({}): {ret} {{\n", params.join(", "));
+    if let (true, Some(machine)) = (reads_state, machine) {
+        out += &format!(
+            "  const {{ {} }} = check{}$({}, state$);\n",
+            field_names(machine),
+            machine.name,
+            string(&name)
+        );
+    }
+    let (checks, text) = param_checks(
+        program,
+        own,
+        &Words {
+            subject: &|p| p.to_string(),
+            render: &|message| string(&format!("{name}: {message}")),
+        },
+    );
+    out += &checks;
     let spec = Scope {
         params: &function.params,
         context: Context::Spec,
@@ -124,10 +252,13 @@ pub(super) fn wrapper(program: &Program, function: &Function) -> (String, bool)
         .filter(|c| c.kind == ClauseKind::Requires)
     {
         let check = format!("!({})", spec.bare(&clause.expr, None));
-        out += &throw(&check, "RangeError", &format!("{name}: {}", clause.text));
+        out += &throw(
+            &check,
+            "RangeError",
+            &string(&format!("{name}: {}", clause.text)),
+        );
     }
-    let args: Vec<String> = function
-        .params
+    let args: Vec<String> = function.params[if role == Some(Role::Init) { state } else { 0 }..]
         .iter()
         .map(|(n, t)| match t {
             Type::Int(Width::I64) => format!("BigInt({})", camel(n)),
@@ -135,16 +266,37 @@ pub(super) fn wrapper(program: &Program, function: &Function) -> (String, bool)
         })
         .collect();
     let call = format!("{name}$({})", args.join(", "));
-    if function.ret == Type::Int(Width::I64) {
+    let unsafe_fields: Vec<String> = match (role, machine) {
+        (Some(Role::Init | Role::Event), Some(machine)) => machine
+            .state
+            .iter()
+            .filter(|(_, ty)| *ty == Type::Int(Width::I64))
+            .map(|(field, _)| format!("!Number.isSafeInteger(result.{})", camel(field)))
+            .collect(),
+        _ => Vec::new(),
+    };
+    if function.machine.is_none_or(|m| m.role == Role::Observer)
+        && function.ret == Type::Int(Width::I64)
+    {
         out += &format!("  const result = {call};\n");
         out += &throw(
             "result < -9007199254740991n || result > 9007199254740991n",
             "RangeError",
-            &format!("{name}: the result is not a safe integer"),
+            &string(&format!("{name}: the result is not a safe integer")),
         );
         out += "  return Number(result);\n";
-    } else {
+    } else if unsafe_fields.is_empty() {
         out += &format!("  return {call};\n");
+    } else {
+        out += &format!("  const result = {call};\n");
+        out += &throw(
+            &unsafe_fields.join(" || "),
+            "RangeError",
+            &string(&format!(
+                "{name}: the state has a field that is not a safe integer"
+            )),
+        );
+        out += "  return result;\n";
     }
     out += "}\n";
     (out, text)
diff --git a/crates/accord/src/typescript/differential.rs b/crates/accord/src/typescript/differential.rs
index 68782db..7eaa511 100644
--- a/crates/accord/src/typescript/differential.rs
+++ b/crates/accord/src/typescript/differential.rs
@@ -25,8 +25,8 @@ mod inputs;
 use super::expr::camel;
 use crate::Solvers;
 use crate::interpret::{self, Value};
-use crate::syntax::{Enum, Function, Type, Width};
-use inputs::{SAFE, Seeded, inputs};
+use crate::syntax::{Enum, Function, Machine, Role, Type, Width};
+use inputs::{SAFE, Seeded, inputs, member_inputs};
 
 fn to_json(value: &Value, enums: &[Enum]) -> Json {
     match value {
@@ -74,6 +74,78 @@ fn expected(
     }
 }
 
+/// A state as the object the module takes and returns.
+fn state_json(machine: &Machine, values: &[Value], enums: &[Enum]) -> Json {
+    machine
+        .state
+        .iter()
+        .zip(values)
+        .map(|((field, _), value)| (camel(field), to_json(value, enums)))
+        .collect::<serde_json::Map<String, Json>>()
+        .into()
+}
+
+/// What a machine's init, event or observer must do in `state` with `args`:
+/// refuse a state that breaks an invariant or helper invariant, and
+/// otherwise behave as the interpreter does.
+fn expected_member(
+    machine: &Machine,
+    member: &Function,
+    state: &[Value],
+    args: &[Value],
+    functions: &[Function],
+    enums: &[Enum],
+) -> Json {
+    let skip = member.machine.map_or(0, |m| m.state);
+    let role = member.machine.map(|m| m.role);
+    let unsafe_i64 = |ty: &Type, v: &Value| {
+        *ty == Type::Int(Width::I64) && matches!(v, Value::Int(n) if n.abs() > SAFE)
+    };
+    let own = &member.params[skip..];
+    let mut names: interpret::Names = Vec::new();
+    if role != Some(Role::Init) {
+        names.extend(interpret::fields(member, state));
+        if machine
+            .state
+            .iter()
+            .zip(state)
+            .any(|((_, ty), v)| unsafe_i64(ty, v))
+            || !matches!(interpret::broken_invariant(member, state), Ok(None))
+        {
+            return json!({"error": "RangeError"});
+        }
+    }
+    names.extend(own.iter().map(|(n, _)| n.clone()).zip(args.iter().cloned()));
+    if own.iter().zip(args).any(|((_, ty), v)| unsafe_i64(ty, v)) {
+        return json!({"error": "RangeError"});
+    }
+    match interpret::broken_requires(member, &names) {
+        Ok(Some(_)) => return json!({"error": "RangeError"}),
+        Ok(None) => {}
+        Err(reason) => panic!("{}: requires can't be evaluated: {reason}", member.name),
+    }
+    if role == Some(Role::Observer) {
+        return match interpret::result(member, &names, functions) {
+            Ok(result) if unsafe_i64(&member.ret, &result) => json!({"error": "RangeError"}),
+            Ok(result) => json!({"ok": to_json(&result, enums)}),
+            Err(reason) => panic!("{}: no result for an admitted state: {reason}", member.name),
+        };
+    }
+    match interpret::transition(member, &names, functions) {
+        Ok(next)
+            if machine
+                .state
+                .iter()
+                .zip(&next)
+                .any(|((_, ty), v)| unsafe_i64(ty, v)) =>
+        {
+            json!({"error": "RangeError"})
+        }
+        Ok(next) => json!({"ok": state_json(machine, &next, enums)}),
+        Err(reason) => panic!("{}: no state for an admitted state: {reason}", member.name),
+    }
+}
+
 fn conformance() -> PathBuf {
     PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("../../conformance")
 }
@@ -180,6 +252,35 @@ fn generated_modules_agree_with_the_interpreter() {
                 }));
             }
         }
+        for machine in program.machines.iter().filter(|m| m.public) {
+            let module = dir.join(format!(
+                "{}.ts",
+                names[machine.file]
+                    .strip_suffix(".accord")
+                    .unwrap_or(&names[machine.file])
+            ));
+            let callable = machine.functions(&program.functions);
+            for member in machine.members() {
+                let reads = member.machine.is_some_and(|m| m.role != Role::Init);
+                for (state, args) in member_inputs(&program, machine, member, &mut seeded) {
+                    wanted.push((
+                        name.clone(),
+                        member.name.clone(),
+                        expected_member(machine, member, &state, &args, &callable, &program.enums),
+                    ));
+                    let mut given: Vec<Json> = Vec::new();
+                    if reads {
+                        given.push(state_json(machine, &state, &program.enums));
+                    }
+                    given.extend(args.iter().map(|a| to_json(a, &program.enums)));
+                    calls.push(json!({
+                        "module": module.display().to_string(),
+                        "name": camel(&member.name),
+                        "args": given,
+                    }));
+                }
+            }
+        }
     }
     assert!(built > 0, "no program built");
     let runner = root.join("runner.mjs");
diff --git a/crates/accord/src/typescript/differential/inputs.rs b/crates/accord/src/typescript/differential/inputs.rs
index 906c82d..a32afd6 100644
--- a/crates/accord/src/typescript/differential/inputs.rs
+++ b/crates/accord/src/typescript/differential/inputs.rs
@@ -1,7 +1,7 @@
 //! The inputs each exported function is called with.
 
 use crate::interpret::{self, Value};
-use crate::syntax::{Body, Expr, Function, Program, Type, Width};
+use crate::syntax::{Body, Expr, Function, Machine, Program, Role, Type, Width};
 use crate::{Outcome, Report};
 
 pub(super) const LIMIT: usize = 4096;
@@ -124,6 +124,71 @@ fn combinations(domains: &[Vec<Value>], seeded: &mut Seeded) -> Vec<Vec<Value>>
     }
 }
 
+/// The integer literals in `expr`.
+fn integers(expr: &Expr, found: &mut Vec<i128>) {
+    match expr {
+        Expr::Int(n, _) if !found.contains(n) => found.push(*n),
+        Expr::Not(inner) | Expr::Neg(inner, _) => integers(inner, found),
+        Expr::Binary(_, l, r) | Expr::Arith(_, l, r, _) => {
+            integers(l, found);
+            integers(r, found);
+        }
+        Expr::If(c, a, b) => [c, a, b].iter().for_each(|e| integers(e, found)),
+        _ => {}
+    }
+}
+
+/// Every state, with every set of arguments, that `member` of `machine` is
+/// called with: the combinations of its fields' and parameters' values, which
+/// include each integer the machine's clauses name and its neighbours, so that
+/// some states meet its invariants and others break them. An init takes no
+/// state, so its states are empty.
+pub(super) fn member_inputs(
+    program: &Program,
+    machine: &Machine,
+    member: &Function,
+    seeded: &mut Seeded,
+) -> Vec<(Vec<Value>, Vec<Value>)> {
+    let words = literals(program);
+    let mut named = Vec::new();
+    for clause in machine
+        .members()
+        .flat_map(|m| m.clauses.iter())
+        .chain(&machine.invariants)
+    {
+        integers(&clause.expr, &mut named);
+    }
+    let fields = member.machine.map_or(0, |m| m.state);
+    let reads = member.machine.is_some_and(|m| m.role != Role::Init);
+    let types: Vec<&Type> = member.params[if reads { 0 } else { fields }..]
+        .iter()
+        .map(|(_, ty)| ty)
+        .collect();
+    let domains: Vec<Vec<Value>> = types
+        .iter()
+        .map(|ty| {
+            let mut values = domain(ty, program, &words, seeded);
+            if let Type::Int(width) = ty {
+                for n in named.iter().flat_map(|n| [n - 1, *n, n + 1]) {
+                    let value = Value::Int(n);
+                    if (width.min()..=width.max()).contains(&n) && !values.contains(&value) {
+                        values.push(value);
+                    }
+                }
+            }
+            values
+        })
+        .collect();
+    let split = if reads { fields } else { 0 };
+    combinations(&domains, seeded)
+        .into_iter()
+        .map(|mut all| {
+            let args = all.split_off(split);
+            (all, args)
+        })
+        .collect()
+}
+
 /// An `example` argument's value: examples are written with literals.
 fn literal(expr: &Expr) -> Option<Value> {
     match expr {
diff --git a/crates/accord/src/typescript/expr.rs b/crates/accord/src/typescript/expr.rs
index 3eb908a..bde2a05 100644
--- a/crates/accord/src/typescript/expr.rs
+++ b/crates/accord/src/typescript/expr.rs
@@ -162,7 +162,9 @@ impl Scope<'_> {
             }
             Expr::Length(list, _) => self.length(list),
             Expr::Index(list, index, _) => self.index(list, index),
-            Expr::Next(..) => unreachable!("`build` refuses a program with a machine"),
+            Expr::Next(..) => {
+                unreachable!("a `next` is written by a machine's body, never as a value")
+            }
         }
     }
 
diff --git a/crates/accord/tests/machines.rs b/crates/accord/tests/machines.rs
index 1d7e132..6633acb 100644
--- a/crates/accord/tests/machines.rs
+++ b/crates/accord/tests/machines.rs
@@ -113,13 +113,134 @@ fn the_receipt_names_the_outcome_and_the_exploration() {
 }
 
 #[test]
-fn a_machine_is_not_written_as_typescript() {
+fn only_a_proved_pub_machine_is_written_as_typescript() {
     let solvers = Solvers::from_env().expect("Z3 and cvc5 are available");
-    let files = [("dial.accord".to_string(), DIAL.to_string())];
-    let Err(refusal) = build(&files, &solvers) else {
-        panic!("a machine was built");
+    let build_of =
+        |source: &str| build(&[("dial.accord".to_string(), source.to_string())], &solvers);
+    // `bounded` is refuted, so nothing is written.
+    let built = build_of(DIAL).expect("the program is accepted");
+    assert!(built.modules.is_none());
+    let proved = DIAL.replace("level <= 10", "level <= 12");
+    let built = build_of(&proved.replace("machine Dial", "pub machine Dial"))
+        .expect("the program is accepted");
+    let modules = built.modules.expect("every obligation is proved");
+    assert!(
+        modules[0]
+            .source
+            .contains("export function set(state$: Dial")
+    );
+    // A machine without `pub` writes nothing.
+    let built = build_of(&proved).expect("the program is accepted");
+    let modules = built.modules.expect("every obligation is proved");
+    assert!(!modules[0].source.contains("Dial"));
+}
+
+#[test]
+fn names_that_would_collide_in_a_module_are_refused() {
+    let solvers = Solvers::from_env().expect("Z3 and cvc5 are available");
+    let source = "pub fn start() -> i32 { 1 }
+pub machine M {
+    state { x: i32 }
+    init start() { next { x: 0 } }
+}
+";
+    let Err(refusal) = build(&[("m.accord".to_string(), source.to_string())], &solvers) else {
+        panic!("colliding names were built");
     };
-    assert!(refusal.message.contains("machine"), "{}", refusal.message);
+    assert!(refusal.message.contains("start"), "{}", refusal.message);
+}
+
+#[test]
+fn an_enum_and_a_machine_may_not_share_an_exported_type_name() {
+    let solvers = Solvers::from_env().expect("Z3 and cvc5 are available");
+    let source = "pub enum M { A }
+pub machine M {
+    state { x: i32 }
+    init start() { next { x: 0 } }
+}
+";
+    let Err(refusal) = build(&[("m.accord".to_string(), source.to_string())], &solvers) else {
+        panic!("colliding type names were built");
+    };
+    assert!(refusal.message.contains("type M"), "{}", refusal.message);
+}
+
+/// Writes the modules `source` builds to a folder of its own and runs
+/// `script`, a module that imports `./m.ts`, in Node; returns its output.
+fn node(source: &str, script: &str) -> String {
+    let solvers = Solvers::from_env().expect("Z3 and cvc5 are available");
+    let built = build(&[("m.accord".to_string(), source.to_string())], &solvers)
+        .expect("the program is accepted");
+    let modules = built.modules.expect("every obligation is proved");
+    let dir = std::env::temp_dir().join(format!(
+        "accord-machines-{}-{}",
+        std::process::id(),
+        script.len()
+    ));
+    let _ = std::fs::remove_dir_all(&dir);
+    std::fs::create_dir_all(&dir).expect("a folder");
+    std::fs::write(dir.join("package.json"), "{\"type\":\"module\"}\n").expect("written");
+    for module in &modules {
+        std::fs::write(dir.join(&module.name), &module.source).expect("written");
+    }
+    std::fs::write(dir.join("run.mjs"), script).expect("written");
+    let node = std::env::var("ACCORD_NODE").unwrap_or_else(|_| "node".to_string());
+    let output = std::process::Command::new(node)
+        .arg("--experimental-strip-types")
+        .arg(dir.join("run.mjs"))
+        .output()
+        .expect("Node runs");
+    assert!(
+        output.status.success(),
+        "{}",
+        String::from_utf8_lossy(&output.stderr)
+    );
+    let _ = std::fs::remove_dir_all(&dir);
+    String::from_utf8(output.stdout).expect("text")
+}
+
+#[test]
+fn a_state_is_read_once_and_the_event_runs_on_what_was_checked() {
+    let source = "pub machine Counter {
+    state { presses: i32 }
+    init start() { next { presses: 0 } }
+    event press() requires presses < 100 { next { presses: presses + 1 } }
+    event keep() { next { } }
+    fn doubled() -> i32 { presses }
+    invariant pressed: presses >= 0 and presses <= 100
+}
+";
+    let out = node(
+        source,
+        "import * as m from './m.ts';
+const attack = () => { let reads = 0; return { get presses() { return reads++ === 0 ? 5 : -5; } }; };
+console.log(JSON.stringify([
+  m.press(attack()).presses,
+  m.keep(attack()).presses,
+  m.doubled(attack()),
+]));
+",
+    );
+    assert_eq!(out.trim(), "[6,5,5]");
+}
+
+#[test]
+fn fields_named_state_and_where_build_and_import() {
+    let source = "pub machine Odd {
+    state { state: i32, where: i32 }
+    init start() { next { state: 0, where: 1 } }
+    event swap() { next { state: where, where: state } }
+    invariant small: state >= 0 and state <= 1 and where >= 0 and where <= 1
+}
+";
+    let out = node(
+        source,
+        "import * as m from './m.ts';
+const s = m.swap(m.start());
+console.log(JSON.stringify(s));
+",
+    );
+    assert_eq!(out.trim(), "{\"state\":1,\"where\":0}");
 }
 
 const STEPPED: &str = "machine Pair {
diff --git a/docs/design/syntax.md b/docs/design/syntax.md
index c6a86de..64dfc3a 100644
--- a/docs/design/syntax.md
+++ b/docs/design/syntax.md
@@ -179,8 +179,8 @@ Blocks are expressions: the last expression is the block's value. There is no
 ## Machines
 
 Accepted for stage 10 ([#82](https://github.com/sequelcore/accord/issues/82)).
-`accord check` checks a machine; `accord build` doesn't write it as
-TypeScript yet. A machine is a state, the ways it starts, the events
+`accord check` checks a machine, and `accord build` writes a `pub` machine
+as TypeScript once every obligation is proved. A machine is a state, the ways it starts, the events
 that move it, and what must hold in every state it reaches:
 
 ```accord
diff --git a/docs/typescript.md b/docs/typescript.md
index ab1a230..ef63752 100644
--- a/docs/typescript.md
+++ b/docs/typescript.md
@@ -10,7 +10,8 @@ imports with no runtime dependency.
 when every obligation is proved and every `example` passes; otherwise it writes
 nothing and exits 1 when something failed, or 3 when something wasn't proved.
 An open case doesn't stop it: the module's header names each function with
-one.
+one. A machine is written only when all its obligations are proved: one that is
+`not_inductive` or undecided stops the build, like any other obligation.
 
 | Code | Meaning |
 | --- | --- |
@@ -38,6 +39,8 @@ Node runs them directly.
 | `i64` | `number` for the caller, `bigint` inside |
 | `List<T>` | `readonly T[]` |
 | `requires` | A check on entry |
+| `pub machine M` | A type, a state check, and an exported function for each init, event and observer, below |
+| `machine` without `pub` | Nothing |
 | `ensures`, `open when`, `example`, `intent` | Nothing: they don't run |
 
 Inside, a decision table is an `if` chain in row order. Where no row is
@@ -62,6 +65,25 @@ never import each other's functions.
 fit `i32`, so it is well inside the integers a `number` holds exactly. `i64`
 arithmetic runs in `bigint`.
 
+## Machines
+
+A `pub machine Switch` becomes `export type Switch = { readonly light: Light;
+readonly presses: number; }`, its fields in order and in `camelCase`, and
+a function `checkSwitch$` that no module exports. Each init, event and
+observer is an exported function named in `camelCase`, with its body unexported
+beside it, as for a function:
+
+- an init takes its parameters and returns the state it gives;
+- an event takes the state, then its parameters, and returns the next state,
+  a new object that lists every field; it leaves the state it was given
+  unchanged;
+- an observer takes the state, then its parameters, and returns its result.
+
+An `i64` field is a `number` in the state, and an event that would leave one
+that isn't a safe integer throws a `RangeError`, as a function does for its
+result. A module whose exported names, or their bodies' names, would collide, or whose exported types (enums and machines) share a name, is
+refused, and nothing is written.
+
 ## The boundary
 
 The proofs assume the caller is checked code. A TypeScript caller isn't, so
@@ -74,6 +96,17 @@ each exported function checks, in order, before it runs:
 | A text holds only characters up to U+2FFFF, the solvers' alphabet, with no lone surrogates | `RangeError` |
 | Each `requires` holds, evaluated with mathematical integers (`bigint`) | `RangeError`, naming the clause |
 
+An event or observer first checks the state it is given, before its own
+parameters. It reads the state once: the check copies the fields into a fresh
+object, and the event or observer runs on that checked copy, so a getter that
+answers differently each time can't pass the check and then give the body
+another value. The generated names in a state check end in `$`, which no Accord
+name can, so a field may be called `state` or `where`. The check: it is an object (`TypeError`), each field has its type and range
+(`TypeError`, `RangeError`, worded `state.<field> must be …`), and then it
+meets every invariant, then every helper invariant, evaluated with
+mathematical integers (`RangeError`, `state breaks invariant <name>: …`). An
+init has no state to check; its result meets the invariants by proof.
+
 An `i64` result that isn't a safe integer throws a `RangeError` instead of
 losing precision. So the generated function accepts fewer inputs than the
 proofs cover, and never runs on one they don't.
@@ -85,5 +118,8 @@ compiler's own tests compare each module with the interpreter: on every
 combination of `Bool` and enum values, each integer width's boundaries and a
 seeded sample, the program's text literals and characters beyond ASCII, each
 `example`'s call and every input a solver gave, with a seeded sample past
-4,096 combinations per function. Agreement on those inputs is evidence, not a
+4,096 combinations per function. For a machine, the same inputs for each
+init, event and observer, and for events and observers, states built from its
+fields' values and the integers its clauses name, most of them breaking an
+invariant or helper invariant, which the module must reject. Agreement on those inputs is evidence, not a
 proof.