Safeguard

On January 28, 1986, the Space Shuttle Challenger was destroyed 73 seconds after launch. A known failure mode was not handled correctly under all conditions. Safeguard makes "unhandled condition" a compile error.

Safeguard is a compiled, safety-critical finite-state-machine language. You describe a system as states, events, transitions, sensors, and actuators in a .sg file. The compiler statically proves nine correctness properties — and only then emits portable C99, a TLA+ specification ready for TLC, and a Graphviz diagram for the design review.

The same intermediate representation drives every backend. The C a firmware team flashes, the TLA+ a formal-methods reviewer model-checks, and the diagram a systems engineer signs off on are, by construction, the same state machine — not three artefacts kept in sync by hope and discipline.

---

The headline failure mode

examples/rocket_abort_system.sg declares a five-state rocket flight machine. Four states route AbortCommand to a safe-abort handler. One does not.

$ safeguard check examples/rocket_abort_system.sg

error[SG001]: state `Flight` does not handle event `AbortCommand`
   ┌─ examples/rocket_abort_system.sg:48:9
   │
48 │   state Flight {
   │         ^^^^^^ missing `on AbortCommand` handler
   │
   = `AbortCommand` is handled by other states of machine `RocketAbort`;
     every state must transition on it or mark it `unhandled`

  help: add an explicit handler to acknowledge this event is intentional
       + on AbortCommand -> unhandled

error[SG009]: deadlock: state `Flight` cannot reach the initial state `Nominal`
   ┌─ examples/rocket_abort_system.sg:48:9
   │
48 │   state Flight {
   │         ^^^^^^ no transition from this state leads back to `Nominal`

Two errors from one mistake: the missing handler (SG001) and the fact that without it the machine deadlocks (SG009). The fix is shown as a diff. The verifier reports every defect on a single invocation — round-tripping is unacceptable in the workflows this language is built for.

---

Quick start

Build the toolchain (Rust 1.74 or newer):

cargo build --release

The compiler binary is ./target/release/safeguard.

Verify a clean program:

$ safeguard check examples/autopilot_lane_change.sg
ok examples/autopilot_lane_change.sg

Verify a deliberately-broken one (exit code 1):

$ safeguard check examples/rocket_abort_system.sg
error[SG001]: state `Flight` does not handle event `AbortCommand`
...

Compile to all three artefacts in one pass:

$ safeguard compile -o out examples/traffic_light.sg
compiled examples/traffic_light.sg -> out/
  safeguard_fsm.h      1.8 KB
  safeguard_fsm.c      1.8 KB
  Safeguard.tla        2.2 KB
  Safeguard.dot        690 B

Or pick a single backend:

safeguard tla examples/traffic_light.sg    # TLA+ module to stdout
safeguard dot examples/traffic_light.sg    # Graphviz DOT to stdout

---

The language at a glance

sensor   pedestrian_waiting: bool
actuator open_crossing()

state_machine TrafficLight {

  initial state Red {
    on Timer -> Green
  }

  state Green {
    on Timer -> Yellow
  }

  state Yellow {
    on Timer -> Red
  }
}

The vocabulary deliberately tracks the way safety reviewers already talk:

• state_machine — one bounded automaton; a program may declare several.
• initial state — exactly one per machine, anchored by SG006 / SG007.
• sensor — a read-only input. C codegen emits an extern getter the firmware must provide.
• actuator — a side-effecting output. C codegen emits an extern setter.
• on Event [where guard] -> Target — a transition; Target must exist (SG003).
• requires { sensor: range } — a per-state invariant; types must match the sensor declaration (SG004).
• entry { ... } / exit { ... } — actuator calls invoked on transition.
• global { on Event -> ... } — a handler folded into every state of the surrounding machine. The "PowerLoss is handled everywhere" pattern.
• unhandled — an explicit acknowledgement that an event is meaningless in this state. Suppresses SG001 for that one site only.

The full grammar lives in crates/safeguard-parser.

---

The nine static checks

The verifier runs all nine on every program and collects every diagnostic it finds. None short-circuits the others.

Code	Check
SG001	Completeness — every state handles every event the machine names.
SG002	Reachability — every state is reachable from the initial state.
SG003	Transition target names an existing state.
SG004	requires clause types match the sensor declaration.
SG005	Guard sensor reads appear in the surrounding requires block.
SG006	Each machine declares an initial state.
SG007	Each machine declares at most one initial state.
SG008	Actuator call argument count and types match the declaration.
SG009	No deadlocks — every state has a path back to the initial state.

SG002 and SG009 are graph properties: SG002 is a BFS from the initial node, SG009 runs Tarjan's strongly-connected-components on the transition graph and flags any SCC that does not reach the initial state. Both go through petgraph; the verifier does not hand-roll graph traversal.

SG001 is the only check that emits a structured Suggestion — the diff-style + on Event -> unhandled line that the renderer surfaces under the error.

---

The four artefacts, side by side

safeguard_fsm.h / safeguard_fsm.c — portable C99

The firmware integrator's deliverable. Zero allocation, zero unsafe, every sensor and actuator emitted as extern so the firmware controls implementation. The dispatcher is a flat switch per state, fault routing goes through a single firmware-provided hook:

extern void safeguard_unhandled_event(
    const char *machine,
    const char *state,
    const char *event);

A program with zero actuators (traffic_light.sg) emits no actuator-extern machinery at all — verified by a pipeline test.

Safeguard.tla — TLA+ module

Ready for TLC. Per-state, per-event actions; the Init predicate pins the initial-state variable; Next is the disjunction of every action plus an EnvironmentStep for sensor changes; multi-machine programs get per-machine state variables with correctly-segregated UNCHANGED clauses (also verified by a pipeline test).

TrafficLight_Init == TrafficLight_state = "Red"

TrafficLight_Red_Timer_0 ==
    /\ TrafficLight_state = "Red"
    /\ TrafficLight_state' = "Green"
    /\ UNCHANGED << sensor_pedestrian_waiting >>

Guard expressions are translated to TLA+ syntax where they map cleanly (&& → /\, == → =, != → #) and over-approximated to TRUE otherwise. Over-approximation, not under: a translation that loses precision must never hide behaviour from the model checker.

Safeguard.dot — Graphviz state diagram

For design review. One subgraph cluster per machine; the initial state is a green dot edge into a double-circle node; global handlers render as dashed edges so they are visibly distinct from local transitions on a printed page.

---

Architecture

   .sg source
       │
       ▼
┌──────────────────┐
│ safeguard-lexer  │   logos-based tokeniser
└──────────────────┘
       │
       ▼
┌──────────────────┐
│ safeguard-parser │   recursive descent, spanned AST
└──────────────────┘
       │
       ▼
┌──────────────────┐
│  safeguard-ir    │   petgraph DiGraph per machine,
└──────────────────┘   globals folded into local transitions
       │
       ├────────────────────────────────────────────┐
       ▼                                            ▼
┌──────────────────┐                       ┌───────────────────────┐
│ safeguard-types  │  the nine static     │  safeguard-codegen-*  │
│   (verifier)     │  checks; never bails │  (c / tlaplus / dot)  │
└──────────────────┘  on first error      └───────────────────────┘
       │                                            │
       ▼                                            ▼
   diagnostics                              C / TLA+ / DOT

Each step is its own crate so each step has its own test suite. The verifier does not depend on a code generator. The C generator does not depend on the TLA+ generator. The IR is shared; nothing else is.

safeguard-cli is the single binary that wires the pipeline together. safeguard-tests is a workspace-level crate that asserts cross-cutting invariants no per-crate suite can check on its own: every IR state appears in every backend's output, every renderer is deterministic across repeated calls, the initial state in the source agrees with the state pinned in the TLA+ Init and the C init function.

---

Workspace layout

crates/
├── safeguard-lexer            // tokeniser
├── safeguard-parser           // parser → spanned AST
├── safeguard-ir               // AST → IR; global folding; petgraph
├── safeguard-types            // the nine static checks
├── safeguard-codegen-c        // C99 emitter
├── safeguard-codegen-tlaplus  // TLA+ emitter
├── safeguard-codegen-dot      // Graphviz emitter
├── safeguard-cli              // the `safeguard` binary
├── safeguard-web              // dashboard (placeholder; see Status)
└── safeguard-tests            // workspace-level integration + snapshots
examples/
├── traffic_light.sg           // clean, hello-world
├── autopilot_lane_change.sg   // clean, Tesla demo (sensors, actuators, globals)
├── rocket_abort_system.sg     // trips SG001 + SG009 (SpaceX demo)
└── elevator_controller.sg     // trips SG009 (deadlocked SCC)

---

Build, test, lint

# Build everything.
cargo build --release

# Run all tests (parser, IR, verifier, three codegens, CLI, pipeline).
cargo test --workspace

# Reproduce the CI lint gate exactly.
cargo clippy --workspace --all-targets -- -D warnings

Workspace-wide lint rules live in Cargo.toml:

• unsafe_code = "forbid" — stronger than deny; cannot be locally overridden.
• missing_docs = "warn" — every public symbol is documented.
• unwrap_used / expect_used / panic — clippy-restriction lints; library code uses Result end-to-end, panics live only in tests.

The release profile (opt-level = 3, lto = "thin", codegen-units = 1, panic = "abort", line-tables-only debug info) targets the kind of deterministic, reasonably-small binary an embedded toolchain ships.

Diagnostic output is snapshotted per example under crates/safeguard-tests/tests/snapshots/. Any regression — intentional or not — surfaces as a .snap.new file that has to be reviewed and explicitly accepted (cargo insta review). The output is the contract.

---

Status

• Compiler. Stable. Parser, IR, verifier, and all three code generators are feature-complete and covered by per-crate tests plus a workspace-level snapshot suite. The CLI surfaces parser and verifier diagnostics through codespan-reporting with the same shape rustc uses — severity, code, source excerpt, underlined span, and (for SG001) a diff-style suggestion.

• Dashboard. crates/safeguard-web is an axum server that runs the full pipeline from a textarea. Launch it locally:

  cargo run --release -p safeguard-web
  # safeguard-web listening on http://127.0.0.1:8080

  Endpoints: GET / (HTML dashboard), GET /api/health, GET /api/examples (the same four .sg files bundled with the CLI), POST /api/compile (JSON in, JSON out — diagnostics text plus structured spans plus the four generated artefacts when the build is clean). The binary is self-contained: HTML, CSS, JS, and the example sources are all include_str!-embedded.

---

Why this exists

Safety-critical systems get reviewed three times: by an embedded engineer reading the C, by a formal-methods reviewer reading the TLA+, and by a systems engineer reading the diagram. In most projects those three artefacts are written by three different people in three different tools and kept "consistent" by code review and process. Safeguard collapses that into one source of truth: the .sg file is the design document, and the compiler is the one part of the workflow that cannot be talked out of an inconsistency.

This is what a finite-state-machine language looks like when you optimise for the reviewer — not for the author.

---

License

Dual-licensed under MIT OR Apache-2.0, at your option.