A self-improving programming language.

Programs that evolve, verify, and optimize themselves. ML-like syntax, formally verified, multi-tier execution from tree-walker to JIT.

Get Started Version 0.1.0

Why IRIS?

Self-Modifying

Your programs can inspect, rewrite, and evolve their own code at runtime. Graph introspection opcodes give programs direct access to their own structure -- swap operators, rewire edges, breed variants, and hot-swap improvements.

Verified by Construction

LCF proof kernel with 20 inference rules, zero unsafe Rust, and a Lean 4 formalization with 47 theorems (zero sorry). Refinement types and contracts verify functional correctness. A compiled Lean FFI bridge means the code that runs is the code that's proven.

Multi-Tier Execution

Programs run through a 4-tier execution cascade: tree-walking interpreter, bytecode VM, JIT-compiled x86-64, and AVX-512 SIMD containers. The right tier for the right job.

Familiar syntax, unfamiliar power.

Algorithms
-- Factorial with cost annotation
let rec factorial n : Int -> Int [cost: Linear(n)] =
  if n <= 1 then 1
  else n * factorial (n - 1)

-- GCD via Euclid's algorithm
let rec gcd a b : Int -> Int -> Int [cost: Unknown] =
  if b == 0 then a
  else gcd b (a % b)

-- Sum a list using fold
let sum xs : List Int -> Int [cost: Linear(xs)] =
  fold 0 (+) xs
Pipelines & Self-Modification
-- Filter, transform, and sum with pipes
let process xs : List Int -> Int [cost: Linear(xs)] =
  xs |> filter (\x -> x > 0)
     |> map (\x -> x * x)
     |> fold 0 (\acc x -> acc + x)

-- Nested lambdas capture outer scope
let scale_all xs factor : List Int -> Int -> List Int =
  map (\x -> x * factor) xs

-- Programs that rewrite themselves
let mutate program new_op : Program -> Int -> Program =
  let root = graph_get_root program in
  graph_set_prim_op program root new_op

Build it with IRIS

Evolutionary Programs

Breed solutions from specifications. NSGA-II population search with lexicase selection and novelty search.

Learn more →

Verified Systems

LCF proof kernel with 20 inference rules. Refinement types and cost annotations let programs carry machine-checked correctness proofs.

Learn more →

Full I/O

TCP, HTTP, files, threading, and JSON in the standard library. Capability-based security controls what effects your code can perform.

Learn more →

High Performance

Four execution tiers from interpreted to JIT-compiled x86-64 with native fold, map, filter, and tuple ops. JIT tests verify equivalence.

Learn more →

Get Involved

Read IRIS

Start with the language guide, explore the standard library, or dive into the architecture.

Build with IRIS

Install IRIS, run the examples, and start writing your own programs. A full library of example programs ships as references.

Contribute

IRIS is open source. Check out the GitHub repository to file issues, submit PRs, or join the discussion.