Learn IRIS

Whether you’re new to IRIS or looking for a deep dive into the architecture, you’ll find what you need here.

Getting Started

New to IRIS? Start with the Getting Started guide to install IRIS and run your first program.

The Language

Learn IRIS syntax, types, and idioms in the Language Guide. IRIS uses an ML-like surface syntax that compiles to typed DAGs.

Standard Library

Explore the built-in Standard Library – math, collections, strings, file I/O, HTTP, JSON, threading, and more.

Architecture

Understand the four-layer architecture – from evolution to hardware, and everything in between.

Verification

Learn how IRIS verifies programs – the LCF proof kernel, refinement types, cost analysis, graded verification for evolution, and the Lean 4 formalization.

Tutorial

Follow the end-to-end tutorial – write a service, verify it, evolve alternatives, deploy as a binary, and run the self-improving daemon.

Reference

The complete language reference – formal grammar (BNF), every primitive opcode, effect tags, and the full type system.