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;
}
Built with --features z3, which needs libz3 installed, the compiler hands those clauses to Z3 as SMT-LIB2 obligations and the prover either discharges them or reports that it cannot. 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 more parser problems than any synthetic test. They are scoped deliberately to safety properties (nothing bad happens) and not yet to liveness (something good eventually happens). The TLA+ integration that would allow liveness specs is a V2 ticket and has not been started.
Working today: the lexer and parser are panic-free and report line:col: diagnostics, 50+ tests cover the lexer through the interpreter, the Cranelift JIT runs fib(25) in 2.8 ms (about 145× the tree-walker, within ~1.4× of native Rust on the same workload), the runtime cross-compiles to both Cortex-M4F and RISC-V rv32imac with .text weight at about 2.3 KiB against a 64 KiB CI budget, certificates verify under stock Z3 from the command line, and the AI-threat lint pass (--ai-threats) catches the off-by-one, missed-else and swallowed-error patterns that show up in LLM-written embedded code that nobody read afterwards.
Not done, and not claimed: tool qualification for DO-178C, ISO 26262 and IEC 62304 has not started, that being a multi-year effort with auditors. There is no temporal liveness checker. The self-hosting prototype lexes a tiny subset of the language and stops there. The standard library is small. Structs and pattern matching are partial. The formatter does not preserve comments. The public list of gaps is at docs/EXPRESSIBLE_INVALID_STATES.md, with a closing ticket against each one. Open tickets across the goalpost ladder are listed in ROADMAP.md.
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.