Getting Started

A 60-second tour of installing Resilient, running your first program, and picking the right backend for your workload.

Table of contents

Try without installing

The fastest way to see Resilient run is the in-browser 🛝 playground — a WASM build of the compiler, no install required. Edit, run, and share examples directly from your browser.

Install

The shipped CLI is rz. Three install paths, pick whichever matches your setup:

One-liner — downloads the latest pre-built binary into ~/.rz/bin/rz:

curl -fsSL https://raw.githubusercontent.com/EricSpencer00/Resilient/main/scripts/install.sh | bash
# Then put ~/.rz/bin on $PATH (the script prints the line for your shell).

From source via cargo install — if you have Rust installed:

git clone https://github.com/EricSpencer00/Resilient.git
cd Resilient
cargo install --path resilient
# `rz` lands in ~/.cargo/bin/rz

From source via cargo build — typical contributor workflow:

git clone https://github.com/EricSpencer00/Resilient.git
cd Resilient
cargo build --release --manifest-path resilient/Cargo.toml
# Binary lands at: resilient/target/release/rz

There are four feature configs depending on what you need:

Build Adds Use when
default interpreter + bytecode VM Day-to-day development
--features z3 Z3-backed contract proofs You have hard requires/ensures clauses
--features lsp Language Server Protocol Editor integration (red squiggles)
--features jit Cranelift JIT Hot-loop / long-running workloads

You can stack them with cargo install: cargo install --path resilient --features "z3 lsp jit".

Hello, world 

// hello.rz — Resilient source extension is .rz
println("Hello, Resilient!");

Run it:

rz hello.rz
# → Hello, Resilient!

A real program

Two functions, a contract, a live block, and an assert. Save as safe_div.rz:

fn safe_divide(int a, int b)
    requires b != 0
    ensures  result * b == a
{
    return a / b;
}

fn main() {
    live {
        let r = safe_divide(100, 5);
        println("100 / 5 = " + r);
    }

    assert(safe_divide(50, 5) == 10, "math is broken");
}

main();

Note the divisor in the live block is 5, not 7 — the ensures result * b == a contract is exact integer equality, so the example needs a divisor that divides evenly. (Try changing it to 7 and running again: the live block detects the contract violation and retries up to 3 times before propagating the error. That’s the self-healing path in action — but the contract is wrong for the inputs, so retry can’t save it.)

Run normally (interpreter):

rz safe_div.rz
# 100 / 5 = 20

Run with the audit pass to see what the verifier proved at compile time vs left as runtime checks:

rz --audit safe_div.rz

With --features z3, the b != 0 precondition becomes a discharged proof obligation rather than a runtime check on every call.

Mission-critical example projects

Reading the syntax page is one thing — seeing the language used end-to-end on the kind of system it was designed for is another. The companion repo EricSpencer00/Resilient-examples contains six full mission-critical demos:

# Project Headline features
01 pacemaker live invariant, recovers_to, contract-checked decision logic
02 infusion-pump actor always:, cumulative-dose ceiling, parse_int Result chain
03 abs-brake-controller forall i in lo..hi, saturating clamp, per-wheel ensures
04 traffic-light-interlock cluster_invariant proves never-both-green
05 reactor-coolant-monitor actor envelope [0, 250] kPa, live over a sensor stream
06 can-bus-parser bytes literals, Result chain, match arm guards

Each project has its own README documenting the safety property under proof, the language features it exercises, and any compiler limitations. Run ./run_all.sh from that repo to diff every program against its golden output.

Pick a backend

Resilient ships three execution backends. All accept the same source — pick based on workload shape:

# Tree walker — fast to start, slow per-instruction.
# Best for one-shot scripts and during dev/test.
rz prog.rz

# Bytecode VM — ~12× faster than the tree walker on fib(25).
# Best for medium workloads where you want fast startup AND
# decent throughput.
rz --vm prog.rz

# Cranelift JIT — ~12× faster than the VM. Compile time is
# real, so use this for hot loops and long-running programs
# where compile cost amortizes.
cargo install --path resilient --features jit  # one-time
rz --jit prog.rz

See the performance page for the actual numbers and the JIT’s current limitations (no closures/structs/while loops yet — interp/VM accept all of those).

Use cases

Embedded / safety-critical

This is what Resilient was built for. The sibling resilient-runtime crate is #![no_std]-friendly and cross-compiles to thumbv7em-none-eabihf (Cortex-M4F class MCU). The Value enum carries Int, Bool, and (with --features alloc) Float, String. The host build uses the full interpreter + VM; the embedded build uses just the runtime value layer + ops.

The live { } block is the headline feature for this target — when a sensor read returns a corrupt frame, an I2C transaction times out, or a divide-by-zero would crash, the runtime restores the block’s state and re-runs it instead of panicking.

Verified utilities

Use the contract layer (requires / ensures) for code where “it works on the inputs we tested” isn’t good enough. Z3 backs the verifier (--features z3); proofs that succeed don’t emit runtime checks. For compliance / certification: --emit-certificate ./certs prog.rz writes one SMT-LIB2 file per discharged obligation, each independently re-verifiable under any compatible solver.

rz --emit-certificate ./certs resilient/examples/cert_demo.rz   # binary built with --features z3
z3 -smt2 ./certs/ident_round__decl__0.smt2
# unsat   ← the proof: negation is unsatisfiable, so the original holds

Bytecode-VM scripting

If you don’t need verification or live-block recovery and just want a fast, simple scripting language, the bytecode VM is competitive with Python on tight numeric loops while giving you a real type system and contracts when you want them.

JIT hot loops

The Cranelift JIT (Phases B–H) compiles arithmetic + control flow + recursion + function calls + let bindings to native code. On fib(25) it’s within ~1.4× of native Rust. For loop-heavy or recursion-heavy workloads, this is the right backend.

What the JIT doesn’t yet compile: reassignment (x = x + 1), while loops, closures, structs, arrays, live { } blocks. Use the VM for those (it accepts all of them) until the relevant JIT phase ships.

REPL 

rz
> let x = 5;
> x + 10
15
> :examples       # show a few canned examples
> :exit

The REPL also accepts :typecheck to toggle static type checking.

Editor integration

Run the LSP server (built with --features lsp):

rz --lsp

For Neovim with nvim-lspconfig, see LSP.md for the config snippet. VS Code needs a thin extension that points at the binary with --lsp.

The server publishes did_open + did_change diagnostics plus three cursor-aware features:

  • Hover — shows the type of any literal under the cursor (int, float, string, bool).
  • Go-to-definition — jumps from a call site to the top-level function or struct declaration.
  • Completion — offers all built-in functions (alphabetical) followed by every top-level declaration in the current file.

See the LSP guide for editor-specific setup.

Where next?