Status: Shipped (#196 G6)
This book is the step-by-step developer and AI-agent guide to Lume (Edition 2026), the AI-first programming language where code is authored with formal contracts, verified by a sound decision procedure or minimal proof kernel, and compiled to native executables without a C toolchain.
G0)Install the prebuilt self-hosted Lume toolchain (lume, lumec, lasm, lcli, lcaas, lcert, ltarget, levolve) with no C compiler required:
sh scripts/install.sh --prefix "$HOME/.lume"
export PATH="$HOME/.lume/bin:$PATH"
lume self verify
lume self verify checks every installed binary and source module against MANIFEST.sha256 and returns structured JSON:
{"ok":true,"command":"self-verify","version":"0.2.0","edition":"2026","zero_c_required":true,"manifest_verified":true}
#197)Lume defaults to immutable values with Perceus in-place reuse (own) and provides explicit compiler-enforced ownership tiers when shared references are required:
rc[T] (rc(v), .get(), .clone(), .drop(), .strong_count(), .downgrade()) — deterministic single-threaded reference counting; rejected across spawn/par boundaries ([S0001]).arc[T] (arc(v), .get(), .clone(), .drop(), .strong_count(), .downgrade()) — atomic reference counting (lock xaddq) safe across spawn, par, and shard.weak[T] (.downgrade(), .upgrade(fallback) -> T, .is_alive()) — non-owning reference that upgrades to the live payload while strong count > 0 or returns fallback after drop.fn tier_example() -> int =
let shared: arc[int] = arc(21) in
let w: weak[int] = shared.downgrade() in
let upgraded = w.upgrade(0) in
let res = shared.get() + upgraded in
let d = shared.drop() in
res
G5, G6)Every function can carry requires preconditions, ensures postconditions, @bound(cycles: N) WCET bounds, and module-level law declarations checked by Lume’s sound QF_LIA solver (Fourier-Motzkin over integers):
pub fn clamp_pos(x: int, hi: int) -> int
requires x >= 0 and hi >= 10
ensures result >= 0 and result <= hi
= if x > hi then hi else x
law clamp_idempotent(x: int, hi: int) =
if x >= 0 and hi >= 10 then clamp_pos(clamp_pos(x, hi), hi) == clamp_pos(x, hi) else 1 == 1
lume prove --diff)Compare two revisions of a module to verify that no proof obligation regressed ([V0003]):
./lume prove --diff old_module.src new_module.src
lume prove --share)Generate a self-contained shareable proof bundle with a lume://verify/sha256:... URI and independent proof certificate:
./lume prove --share module.src
G2, #191)Compile a critical module as a Verified Sidecar and call it from Lume (examples/interop/sidecar/):
payment_core.src with pub extern "c" fn exports and requires/ensures contracts../lume certify payment_core.src and ./lume verify-cert payment_core.src../lume build payment_core.src --emit-c-header payment_core.h -o payment_core.so.host_lume.src). External-language hosts and in-process WASM execution are not claimed by this example.G4, G7)Every Lume package declares its required capabilities in lume.toml (allow = ["pure"] or allow = ["io", "net"]) and locks every module’s SHA-256 digest in lume.lock:
./lume pkg publish <dir> --store <registry_dir> refuses to publish any package whose contracts fail lume certify or lume verify-cert ([V0001])../lume pkg audit <dir> verifies capability grants (P26), lockfile SHA-256 integrity (P32), and the independent proof certificate (lcert)../lume pkg check-rot <old_dep.src> <new_dep.src> <downstream.src> detects semantic proof rot ([V0003]) when a dependency weakens a postcondition relied upon by downstream code.#198)docs/19 §3): ./lume agent patch <file.src> <fn_name> "<new_expr>" edits the typed AST directly, verifies contracts before accepting the edit, and projects canonical formatted Lume source.docs/19 §4): ./lume agent replay <file.src> records logical-time trace steps, verifies deterministic replay hashes, and bisects the exact first_negative_step.docs/19 §5): ./lume agent lineage <file.src> <fn_name> answers “why am I this?” with function origin (human vs llm_untrusted), input taint, verify(...) gates, and proof status.docs/23 H1, H4): ./lume prove --compositional <mod_a.src> <mod_b.src> verifies cross-module contracts and enforces [V0004] whenever an extern llm fn output crosses into a proven function without a verify(...) guard.