Eric Spencer
projects
GitHub Repo · Examples Repo · Docs
Resilient is a programming language: .rz source files and a compiler called rz. The target domain is embedded control where a crash or a hang has physical consequences: pacemakers, infusion pumps, anti-lock brakes, reactor coolant loops. It grew out of formal methods reading and the TLA+ written for the microwave project, together with the observation that the languages usually shipped to a Cortex-M chip (C, sometimes Rust, occasionally Ada) each keep the safety story somewhere other than where the code lives. C relies on MISRA layered on top. Rust supplies memory safety but has no knowledge of program invariants. Ada/SPARK supplies proofs but requires a certified toolchain. Resilient places the contract, the runtime safety net, and the embedded story in one language, designed together.
The project is research-grade and the work of one person. It is not qualified for a certified system. The compiler is written in Rust and targets a bytecode VM, with a Cranelift JIT alongside it. The runtime is #![no_std] and cross-compiles to thumbv7em-none-eabihf (Cortex-M4F) and riscv32imac-unknown-none-elf (HiFive / GD32V / ESP32-C3 class). A Z3-backed verifier discharges function contracts at compile time. The language ships a REPL, a formatter (rz fmt), an LSP server (rz --lsp) and a VS Code extension on the Marketplace, and .rz is registered with GitHub Linguist so syntax highlighting works in repositories.
Functions carry requires and ensures clauses, in the manner of SPARK or Dafny:
fn safe_divide(int a, int b) -> int
requires b != 0
ensures result * b == a
{
return a / b;
}
With the Z3 backend enabled, the compiler hands those clauses to Z3 as SMT-LIB2 obligations and the prover either discharges them or reports that it cannot. Source builds use --features z3 and need libz3; the release binaries bundle Z3 on the platforms listed below. The driver can also dump the proof to a .smt2 file via --emit-certificate ./certs/, so a downstream reader can re-verify under a separate copy of Z3 without trusting the compiler binary. An Ed25519 signing step (--sign-cert) and a manifest with per-obligation SHA-256 hashes sit on top of that. The design puts the weight of the evidence on the certificate rather than on the compiler that produced it, which is what could in principle make the output usable in a real safety case.
A hand-rolled cheap verifier covers the easy cases (constant folding, let-binding propagation, inter-procedural chaining), so a useful subset is available without installing Z3. An --infer-contracts pass reads a function body and suggests omitted requires and ensures clauses: division-by-zero guards, index-bounds checks, single-return-expression invariants.
The second mechanism is the self-healing live block. A live { } block is a region of code the runtime supervises, with an invariant attached to it. If something inside the block fails transiently (a glitched sensor read, a divide-by-zero on unsanitized input, a broken invariant) the runtime neither panics nor halts the program. It rewinds the block's local state to its value on entry and re-runs the body. Either the block completes with the invariant intact or it never happened, in the manner of a database transaction.
live invariant: pressure >= 0 && pressure <= 250 {
pressure = read_coolant_sensor();
log_pressure(pressure);
}
This addresses the class of fault where a retry genuinely recovers: sensor noise, a debouncing window, a one-cycle EMI spike on an industrial bus, in a controller that cannot afford to fall off the rails. Cycle limits and an escalation path back the rewind, so a permanently broken invariant does not loop forever. That part is still rough, and the failure semantics are revised every few weeks.
A separate repository, Resilient-examples, carries the motivating programs. Each folder is a small runnable program, usually one .rz file and a README, modelling a real safety-critical domain:
01-pacemaker: implantable cardiac pacer, uses live { invariant } and recovers_to to guard the pacing decision logic.02-infusion-pump: drug delivery, modeled as an actor with an always: clause on the cumulative-dose ceiling.03-abs-brake-controller: anti-lock brakes, uses forall i in lo..hi over the wheel array and saturating arithmetic via clamp.04-traffic-light-interlock: road interlock, demonstrates cluster_invariant for the never-both-green property across two actor intersections.05-reactor-coolant-monitor: sensor stream supervised by a live block with a [0, 250] kPa envelope.06-can-bus-parser: CAN frame parser using bytes literals, Result chains, and match arm guards.The examples stress the language in a way the unit-test suite cannot: writing a pacemaker turns up parser problems that a small synthetic test misses. They model safety properties in particular control scenarios. For the separate work on state machines and model checking, see my TLA+ projects.
As of September 22, 2026, the project status recorded in the repository reports more than 9,000 passing tests across the parser, type checker, interpreter, editor support, embedded builds, and example programs. The self-hosting work now includes both a lexer and a parser, with a parity harness that compares them against the Rust implementation. It remains work in progress.
The release documentation lists bundled Z3 for Linux on x86-64 and ARM64, and macOS on Apple silicon. The Intel Mac build uses the smaller built-in verifier unless Z3 support is built separately. All four release targets include the language server. The published performance example measures fib(25) at 2.8 ms with the JIT on an Apple M1 Max; that is one workload, not a general speed claim.
This is still a research compiler, not a tool qualified for a certified system. The roadmap, known language gaps, and self-hosting notes track what is supported and what remains unfinished.
Much of the code in the repository was written with help from Claude. The failure mode that matters is a model satisfying an obligation by adjusting the test instead of the implementation, and the compiler's trust model is built around it. The LLM is treated as an untrusted client of the type system, never as a participant in the proof. The verifier re-derives every safety claim from the typed AST, and nothing asserted in a comment or a pull request description is taken at face value. STRUCTURAL_ENFORCEMENT.md documents that constraint, which shapes more of the project than any single feature.
curl -fsSL https://raw.githubusercontent.com/EricSpencer00/Resilient/main/scripts/install.sh | bash
rz --version
From source, with Rust available: run cargo install --path resilient in the cloned repository, adding --features z3 where libz3 is present and SMT proofs are wanted. resilient/examples/sensor_monitor.rz is the smallest interesting program. The Resilient-examples repository has a ./run_all.sh that runs the whole set.