Architecture

IRIS is a four-layer stack. Each layer operates on a single canonical representation: the SemanticGraph.

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         -- bootstrap evaluator + effect dispatch / CLCU (AVX-512)

SemanticGraph (L1)

The SemanticGraph is the canonical program representation. Every IRIS program – whether written by hand, compiled from .iris files, or bred by evolution – is a typed DAG with 20 node kinds.

Node Kinds

Each node carries a NodeId (64-bit BLAKE3 truncated), a type reference, a cost term, an arity, and operation-specific payload. Nodes are content-addressed – identical subgraphs share the same ID.

Evolution (L0)

IRIS evolves programs through genetic search. The evolution system itself is written in IRIS.

Mutation Operators

16 mutation operators (all .iris programs), tracked by the improvement system:

Selection Strategies

• Tournament selection – binary tournament on fitness
• Lexicase selection – sequential filtering on individual test cases
• NSGA-II – multi-objective Pareto optimization
• Novelty search – reward behavioral novelty over raw fitness

Population Management

• Pareto ranking – assign non-dominated rank
• Crowding distance – maintain population diversity
• Elitism – preserve top individuals across generations
• Death culling – remove unfit individuals

Crossover

The Graph-Embedding Codec (GIN-VAE) enables crossover by:

1. Encoding parent graphs into embedding vectors
2. Interpolating in embedding space
3. Decoding back to valid graphs
4. Running a 10-phase structural repair pipeline

The GIN-VAE is trained on a 1,045-program corpus (all .iris programs, evolution Pareto fronts, self-write mutation programs, bootstrap interpreter, and seed generators). The LearnedCodec achieves 0.012 reconstruction loss.

Improvement Tracking (PT3)

The evolution system tracks improvement dynamics for each component:

• Improvement rate – linear regression over sliding-window latency measurements
• Acceleration – second derivative of latency; negative acceleration means improvements are compounding
• Causal operator attribution – per-operator statistics tracking success rate, times used, and average fitness delta across 16 mutation operators
• Adaptive weighting – mutation operator selection weights adjusted proportional to observed success rate and improvement magnitude

When the tracker detects compounding improvements (acceleration < 0), the daemon increases investment in that component’s evolution. When deceleration is detected, it recognizes a plateau and redirects resources.

Verification (L2)

The proof kernel is the trusted core of IRIS. It implements CaCIC (Cost-aware Calculus of Inductive Constructions) with 20 inference rules.

See the Verification page for a deep dive into the proof kernel, refinement types, the checker, and the Lean formalization.

Properties

• Zero unsafe Rust – the kernel contains no unsafe blocks
• LCF-style – proofs can only be constructed through the kernel’s API; no external code can forge a Theorem value
• Refinement types – predicates on types checked via kernel rules refine_intro and refine_elim
• Cost annotations – type signatures carry computational cost metadata ([cost: Linear(n)]), used as evolution fitness objectives. Cost subsumption rules exist in the kernel but are not yet wired into proof construction.
• Lean 4 formalization – a separate Lean 4 codebase (lean/IrisKernel/) mirrors the 20 rules as inductive types and proves consistency properties of the type theory. This is a formalization of the design, not a verification of the Rust implementation. The proof kernel (kernel.rs) is the trusted core. It represents the Lob’s theorem ceiling – the only code that IRIS cannot replace with IRIS-evolved equivalents.

What “verified” means here: The kernel provides a sound verification framework – programs can carry machine-checked proofs, and the LCF architecture prevents proof forgery. Program verification is optional; most programs today carry no proofs. The kernel itself is not verified against the Lean spec (it’s small and auditable, but not extraction-based).

Verification Tiers

Execution (L3)

Programs run through the bootstrap evaluator with optional effect dispatch:

Bootstrap Evaluator

The bootstrap evaluator handles all 20 node kinds directly. It dispatches primitive operations (50+ opcodes), manages closures, and evaluates fold/unfold recursion. The meta-circular interpreter (full_interpreter.iris) can also dispatch on node kind tags via graph introspection.

Effect Dispatch: Opcode 0xA1 (perform_effect) dispatches all 44 effect tags through an EffectHandler. The RuntimeEffectHandler implements real I/O (files, TCP, environment, time, random). The CapabilityGuardHandler wraps any handler and enforces capability restrictions before each effect call.

Performance: ~0.2 microseconds per step.

CLCU (AVX-512)

Cache-Line Compute Units – 64-byte containers designed for 16-lane SIMD execution. Includes adaptive prefetch and branch predictor hints.

Self-Improvement Daemon

The daemon runs continuously, improving IRIS’s own internal components – specifically mutation operators and seed generators (e.g., mutation_insert_node, seed_arithmetic). It breeds IRIS program replacements for these Rust-implemented functions:

1. Profiles registered components via sliding-window latency tracking
2. When a component exceeds the latency threshold, spawns evolution
3. Tests replacements through the performance gate (100% correctness, ≤2x slowdown)
4. Atomically hot-swaps if the replacement passes
5. Feeds results to the improvement tracker for causal attribution and adaptive weighting
6. Detects stagnation after N consecutive failures
7. Detects compounding improvements and increases evolution investment
8. Maintains a BLAKE3 Merkle audit chain for tamper-evident history
9. Persists state to disk; resumes after restart

Bootstrap Chain

Rust bootstrap evaluator (~1,150 LOC)
  → loads IRIS meta-circular interpreter (full_interpreter.iris)
    → evaluates all other IRIS programs
      → evolves replacement components in IRIS

The goal: IRIS replaces all Rust except the proof kernel and the OS interface.

Crate Map