Intelligent Runtime for Iterative Synthesis -- a self-improving programming language and runtime where programs are typed DAGs that evolve, verify, and optimize themselves.
IRIS is both a language and a runtime -- one system, two faces:
- The language is an ML-like surface syntax (
.irisfiles) that humans and LLMs write. It compiles to SemanticGraph, the canonical program representation. - The runtime is a four-layer execution substrate that evolves, verifies, and runs SemanticGraphs. Evolution can also produce programs directly -- no surface syntax required.
The surface syntax is a projection of the SemanticGraph, not the source of truth. Programs are content-addressed DAGs with 20 node kinds, purely functional, carrying their own type environments. The syntax is how you write them; the graph is what they are.
L0 Evolution -- population search (NSGA-II + lexicase + novelty)
L1 Semantics -- SemanticGraph (20 node kinds, BLAKE3 content-addressed)
L2 Verification -- LCF proof kernel (20 inference rules, zero unsafe Rust)
L3 Hardware -- tree-walker + CLCU (AVX-512)
- Self-improving: IRIS evolves its own mutation operators, seed generators, selection strategies, and compiler passes. The self-improving daemon profiles components, evolves replacements, gates them for correctness and performance, and deploys improvements automatically.
- Self-hosting: 256
.irisprograms cover all system components. The bootstrap evaluator loads the IRIS meta-circular interpreter, which handles all 20 node kinds. The irreducible Rust substrate is ~51K LOC across 5 crates (proof kernel + bootstrap evaluator + types + evolution engine + execution shim). - Verified: The LCF proof kernel (CaCIC -- Cost-aware Calculus of Inductive Constructions) proves type safety, cost bounds, and functional properties via refinement types and contracts. The kernel's 20 inference rules are formalized in Lean 4 with 47 theorems (zero
sorry), and a Lean FFI bridge lets the proven Lean code execute as the production kernel. - Recursive: IRIS programs improve IRIS programs. Stagnation detection identifies local maxima. A BLAKE3 Merkle chain provides tamper-evident audit trails for all self-modifications.
The runtime is implemented in Rust with 5 crates. The parser, proof kernel, and syntax pipeline are embedded inside the bootstrap crate (merged from the original 14-crate workspace):
Permanent Rust substrate (5 crates)
iris-types (5,370 LOC) -- SemanticGraph, Value, types, cost, wire format
iris-bootstrap (12,887 LOC) -- bootstrap evaluator + parser + proof kernel
+-- syntax/ -- lexer, parser, lowerer (merged from iris-syntax)
+-- syntax/kernel/ -- LCF proof kernel (merged from iris-kernel)
iris-exec (2,326 LOC) -- execution shim, capabilities, effect runtime
iris-evolve (30,340 LOC) -- evolution engine, self-improvement daemon
iris-clcu-sys (300 LOC) -- FFI bindings to C CLCU interpreter
IRIS Programs (256 files, 34K+ LOC)
interpreter/ -- meta-circular interpreter (all 20 node kinds)
evolution/ -- mutation, selection, crossover, seeds, NSGA-II
compiler/ -- 10-pass pipeline (monomorphize -> container pack)
codec/ -- GIN-VAE encoder/decoder, HNSW index
analyzer/ -- 10 pattern detectors for problem classification
exec/ -- evaluator, cache, effects, daemon, message bus
checker/ -- tier classification, obligation counting
foundry/ -- algorithm foundry API, fragment library
syntax/ -- tokenizer, parser, lowerer (self-hosting)
meta/ -- auto-improve, performance gate, instrumentation
deploy/ -- bytecode serialization, standalone binaries
store/ -- persistence, registry
algorithms/ -- fibonacci, gcd, factorial, quicksort
io/ -- TCP, files, system primitives
threading/ -- spawn/join, atomics, rwlocks
vm/ -- bytecode compiler, VM step/run
population/ -- population management, elitism
# Build
cargo build --release
# Run an IRIS program
cargo run --release --bin iris -- run examples/algorithms/factorial.iris 10
# Output: 3628800
# Type-check / verify a program
cargo run --release --bin iris -- check examples/verified/bounded_add.iris
# Output: [OK] bounded_add: 5/5 obligations satisfied (score: 1.00)
# Evolve a solution from a specification
cargo run --release --bin iris -- solve spec.iris
# Run the self-improving daemon
cargo run --release --bin iris -- daemon 100The run command loads the pre-compiled tokenizer, parser, and lowerer from
bootstrap/*.json, then evaluates the resulting SemanticGraph with the bootstrap
tree-walker. No feature flags are needed.
# Run core tests (273 pass)
cargo test -p iris-types -p iris-bootstrap -p iris-exec
# Run integration tests
cargo test --test test_effects --test test_security --test test_bootstrap_effects --test test_capability_wiring
# Run all tests (skipping known long-running benchmarks)
cargo test --workspace -- --skip bench_ --skip evolve_abs --skip evolve_dot_product_interleaved --skip fuzz_ --skip measure_ --skip algorithm_proving --skip complexity_scaling --skip iris_program_levelsiris daemon --exec-mode continuous --max-stagnant 5
The daemon:
- Runs evolution using IRIS-written components (mutation, selection, crossover, seeds)
- Profiles each component's real performance (sliding-window latency tracking)
- When a component exceeds the latency threshold, spawns a background thread to evolve a replacement
- Tests the replacement through the performance gate (100% correctness, <=2x slowdown)
- Atomically hot-swaps the component if it passes (or rolls back)
- Detects stagnation (N consecutive failed improvements) and stops trying
- Detects system convergence (all components at local maximum)
- Persists state to disk; resumes after restart
- Maintains a BLAKE3 Merkle audit chain for every modification
IRIS programs are .iris files with an ML-like surface syntax. The syntax compiles to SemanticGraph -- it's a human-friendly way to construct typed DAGs, not a traditional source language. Evolved programs that have no textual origin can be decompiled back to .iris (best-effort, may be lossy for complex DAG structures).
-- Factorial with recursion and cost annotation
let rec factorial n : Int -> Int [cost: Linear(n)] =
if n <= 1 then 1
else n * factorial (n - 1)
-- Sum a list using fold
let sum xs : List Int -> Int [cost: Linear(xs)] =
fold 0 (+) xs
-- Self-modifying: replace an operator in a program
let mutate program new_op : Program -> Int -> Program =
let root = graph_get_root program in
graph_set_prim_op program root new_op
| Category | Primitives |
|---|---|
| Arithmetic | +, -, *, /, %, neg, abs, min, max, pow |
| Comparison | ==, !=, <, >, <=, >= |
| Logic | and, or, not |
| Graph | self_graph, graph_nodes, graph_get_kind, graph_get_prim_op, graph_set_prim_op, graph_add_node_rt, graph_connect, graph_disconnect, graph_replace_subtree, graph_eval, graph_get_root, graph_add_guard_rt, graph_add_ref_rt, graph_set_cost |
| I/O | tcp_connect, tcp_read, tcp_write, tcp_close, tcp_listen, tcp_accept, file_open, file_read_bytes, file_write_bytes, file_close, file_stat, dir_list, env_get, clock_ns, random_bytes, sleep_ms |
| Threading | thread_spawn, thread_join, atomic_read, atomic_write, atomic_swap, atomic_add, rwlock_read, rwlock_write, rwlock_release |
| Collections | fold, map, filter, zip, concat, reverse, len |
| Effects | perform_effect (generic effect dispatch via opcode 0xA1) |
Once compiled to SemanticGraph, programs are evaluated by the bootstrap tree-walker. The evaluator handles all 20 node kinds, dispatches effects through a capability-guarded handler, and supports self-evaluation via graph_eval.
| Tier | Backend | Description |
|---|---|---|
| A | Tree-walking interpreter | Fast evaluation, no overhead |
| CLCU | AVX-512 containers | Hardware-accelerated via C CLCU library |
The bootstrap evaluator dispatches all 44 effect tags through an EffectHandler trait. The RuntimeEffectHandler implements real I/O (files, TCP, env, time, random, atomic state), and the CapabilityGuardHandler wraps it with capability enforcement.
Every execution path — IrisExecutionService, interpret_with_capabilities, and interpret_sandboxed — enforces capabilities. By default, programs run in a sandbox that allows only pure computation effects (Print, Log, Timestamp, Random).
IRIS has three layers of verification:
The kernel is ~7,345 LOC of Rust (in src/iris-bootstrap/src/syntax/kernel/) with zero unsafe blocks outside the Lean FFI bridge. It has 20 inference rules that produce opaque Theorem values — external code cannot forge proofs. The kernel proves type safety, cost bounds, and functional properties via refinement types ({x : Int | x > 0}) and contracts (requires/ensures).
The kernel's 20 rules are formalized in Lean 4 (lean/IrisKernel/) with 47 theorems and zero sorry markers. Key results include weakening (structural induction over all 20 constructors), cost lattice properties, and consistency. 85 cross-validation tests verify the Rust implementation matches the Lean specification.
A C shim + Rust bridge lets the compiled Lean code execute as the production kernel. Enable with --features lean-ffi (requires Lean 4 toolchain). Without it, the Rust implementation runs as a fallback — both produce identical results (verified by 85 cross-validation tests).
Every self-modification (component deployment, rollback) is recorded in a tamper-evident BLAKE3 Merkle chain. Each entry's hash covers all fields; each entry's prev_hash links to the previous. Modifying any entry breaks the chain.
All IRIS programs run through the CapabilityGuardHandler, which enforces fine-grained effect permissions before any I/O reaches the OS. The default sandbox blocks:
- All file operations (read, write, open, stat, dirlist)
- All network operations (TCP connect/listen/accept)
- Thread spawning
- FFI calls
- MmapExec (JIT code generation)
- Environment variable access
Only explicitly allowed effects (Print, Log, Timestamp, Random, ClockNs, RandomBytes, SleepMs) pass through.
IRIS programs declare the effects they need using allow/deny blocks:
allow [FileRead, TcpConnect "api.*"]
deny [MmapExec, ThreadSpawn, FfiCall]
Capabilities are enforced at runtime before each effect is dispatched. A program that attempts an effect not in its allow-list gets a PermissionDenied error.
File operations validate paths against an allow-list with glob matching (/tmp/**, /home/user/data/*). Paths are canonicalized to prevent symlink bypass attacks. Null bytes in paths are rejected. TCP operations validate host names against an allow-list with wildcard subdomain matching (*.example.com).
All 6 findings from the 2026-03-24 security audit have been resolved. See docs/security-todo.md for details.
The LCF proof kernel (at src/iris-bootstrap/src/syntax/kernel/) enforces zero unsafe blocks across all modules. The single exception is lean_bridge, which is explicitly #[allow(unsafe_code)] because it calls into Lean 4's C-compiled output via FFI.
src/
iris-types/ Core data structures (SemanticGraph, Value, types, cost, wire)
iris-bootstrap/ Bootstrap evaluator + syntax pipeline + proof kernel
src/syntax/ Lexer, parser, AST, lowering (merged from iris-syntax)
src/syntax/kernel/ LCF proof kernel (merged from iris-kernel)
iris-exec/ Execution shim, capabilities, effect runtime, registry
iris-evolve/ Evolution engine, self-improvement daemon
iris-clcu-sys/ FFI bindings to C CLCU interpreter
bin/iris.rs CLI binary (run, check, solve, daemon, repl)
src/iris-programs/ Core .iris programs (18 categories)
examples/ Demo .iris programs + Rust examples
examples/ 10 example projects with .iris test harness
benchmark/ 10 Computer Language Benchmarks Game implementations
bootstrap/ Pre-compiled IRIS interpreter (JSON)
lean/ Lean 4 kernel formalization (47 theorems, 0 sorry)
iris-clcu/ C CLCU interpreter (AVX-512 + scalar)
tests/ 115 test files (~273+ tests)
docs/ User guide, language reference, architecture, API, contributing
site/ Hugo-based documentation website
AGPL-3.0-or-later. See LICENSE for the full text.
Commercial licensing available — contact Brian Jones (bojo@bojo.wtf) for details.