1×
Tree-walking interpreter
rz prog.rz
For fast iteration, REPL work, and the test loop. Zero build steps; instant feedback.
A LANGUAGE FOR SAFETY‑CRITICAL SYSTEMS
Resilient is a statically-typed, compiled language for software where failure is not an option. Contracts are proven at compile time. Hardware faults self‑heal. The same source runs on a development laptop or on a bare‑metal microcontroller.
#![no_std]// Fault-tolerant flight controller fn read_pressure(int sensor_id) -> float requires sensor_id >= 0 && sensor_id < 4 ensures result >= 0.0 && result <= 120_000.0 { let raw = hal::adc_read(sensor_id); return calibrate(raw, PRESSURE_CAL[sensor_id]); } fn altitude_controller() { live { // transient faults auto-retry — no crash let p = read_pressure(PRIMARY_SENSOR); let alt = barometric_altitude(p); assert(alt < MAX_ALTITUDE, "ceiling exceeded"); actuator::set_throttle(pid_update(alt)); } }
§ 01 · The thesis
Most languages assume the happy path. Resilient assumes the worst path — and refuses to ship until you have proven your software survives it.
A pacemaker may not throw. An anti‑lock brake controller may not leak memory. A reactor monitor may not panic. Live blocks let your code expect transient faults, recover from them, and keep the supervised state machine moving.
Function contracts are not documentation — they are formal obligations. Where the verifier can decide them, they are proven at compile time and a re-checkable SMT‑LIB2 certificate is emitted. Where it cannot, they become typed runtime guards.
No allocator. No exceptions. No panics in the default runtime. The compiler emits binaries small enough for a Cortex‑M0 and proofs strong enough for a DO‑178C audit — from a single source tree.
§ 02 · The runtime primitive
Wrap critical code in a live block and the runtime
becomes its supervisor. A snapshot is captured on entry. A
recoverable fault — a transient ADC glitch, a momentary CAN‑bus
dropout, a divide‑by‑zero from a bad reading — restores
state and retries. The watchdog never trips. The kernel never
panics. The mission keeps flying.
§ 03 · The compile-time contract
fn deliver_dose(float ml_per_hr, int seconds) requires ml_per_hr >= 0.1 && ml_per_hr <= 300.0 requires seconds > 0 && seconds <= 86_400 ensures total_ml(result) <= MAX_DAILY_ML { let total = ml_per_hr * (seconds as float) / 3600.0; pump::dispense(total); return Dose { ml: total }; }
✓ deliver_dose requires ml_per_hr ∈ [0.1, 300.0] proved ✓ deliver_dose requires seconds ∈ (0, 86_400] proved ✓ deliver_dose ensures total_ml ≤ MAX_DAILY_ML proved → certificate emitted at ./certs/infusion_pump.smtlib2 → re-checkable under any SMT solver
requires states what must hold on entry.
ensures states what holds on exit. The Z3 backend
decides them statically when it can — and emits an SMT‑LIB2
certificate so a downstream auditor can re‑verify under
their own solver of record.
§ 04 · The numbers
For fast iteration, REPL work, and the test loop. Zero build steps; instant feedback.
A compact, deterministic register machine. Ideal for embedded targets that don’t need a JIT.
Within 1.4× of native Rust on the standard suite. Same source, native speed.
Benchmarks measured on M1 Max, fib(25). Methodology & raw numbers →
§ 05 · Where it runs
The resilient-runtime crate is #![no_std] by
default — zero allocator, zero panics, zero std. Cross‑compile
gates run on every commit, and the Cortex‑M4F demo enforces a
64 KiB .text budget that has never regressed.
CORTEX-M4F
The flagship embedded target. Hard‑float ABI, .text ≤ 64 KiB, gated on every PR via the resilient-runtime-cortex-m-demo crate.
CORTEX-M0+
The smallest supervised target — soft‑float, sub‑100 MHz cores. Live blocks compile away to ~80 bytes of supervisor stub per site.
RV32IMAC
RISC‑V baseline with atomics & compressed insts. Open ISA, fully supervised — a fit for new‑build avionics and reactor monitors.
x86_64 · aarch64
The same source the satellite ships runs in your editor. cargo test on host. rz --jit for hot iteration. Bit‑for‑bit determinism with the embedded VM.
§ 06 · The standards
Resilient is not itself a certified tool. Its surface is mapped, line by line, to the objectives that the major safety regimes enforce — so the qualification kit you build downstream begins from a defensible starting point, not a clean‑sheet defense.
Avionics
Software considerations in airborne systems. Maps to A‑1 through A‑7 objective tables for Levels A & B.
View mapping →Automotive
Functional safety for road vehicles. Mapping covers ASIL D software — Part 6, Tables 1–10.
View mapping →Medical
Medical device software lifecycle. Class C software — pacemakers, infusion pumps, ventilators.
View mapping →§ 08 · Begin
git clone https://github.com/EricSpencer00/Resilient.git cd Resilient && cargo install --path resilient rz examples/altitude_controller.rz
