RCE: the Reality Code Engine

RCE stands for Reality Code Engine. It is a programming language and toolchain in which every program has the one shape of the Form, so that programs can be written, checked, changed and run by machines without a language model in the loop. The shape is rigid at each commit of the specification, and it grows inside the same text when a program needs a form it lacks.

Why RCE exists

RCE is made for the AI coding era. Models now write most of the code that gets written, and they write it in languages designed for people: text whose meaning depends on the compiler, the platform, the library versions and the flags, and whose correctness is checked after the fact by tests, reviews and more model calls. Every one of those steps spends energy and tokens on resolving ambiguity that the language itself introduced, and none of them can promise that the result is right.

RCE removes the ambiguity at the source. A program is a Form: a state machine P = (S, E, δ, D, λ) of declared states, declared events, a pure step function from a state and an event to the next state and its outputs, and the hash-chained log D of every event applied. Everything the program can do is in the Form, including the example lines it carries, so an accepted program is a Form whose examples hold. Where a text does not yet have the Form's shape (a parse error, a type error, an example that does not hold), the checker names the place and the part of the shape it lacks.

This is what makes autonomous coding deterministic. A proposal, whether a person, a search over existing Forms or a model produced it, is read by the checker alone, with the same result on every machine. Once accepted, the Form replays identically wherever the reference runs, is designed to project to any target language without changing meaning, and is reused as a whole. RCE is designed so that every language is both an output and an input of the Form (spec/proposals/rce-form.md): a print table emits a language from the Form, and a lift table, the reverse map, brings a program written in that language into the Form, each accepted at a level by exact comparison with the language's own implementation. That layer is not built yet. Today rce emit translates a checked program, not the Form, to Rust, Python, JavaScript and Scala through four hand-written emitters, all four of which agree with the reference on the conformance suite (1,459 tests pass, 0 fail, for each). The lifts are the probe spec/lift/go/lift_go.py, for one Go pattern, and spec/lift/python/lift_py.py, for a subset of Python 3.13, which carries 6 of the 92 cases of the pinned Python corpus (lang/README.md). The registry (spec/proposals/emit-targets.md) lists the languages that follow, including the new entrants of 2024 to 2026. No model is needed to decide what a program means, whether a change is safe, or whether two programs are the same, so the costly and non-deterministic part of AI coding is taken out of the loop. The aim is the lowest cost and lowest energy per correct program. Energy is not measured today. The checker counts work in integer cost units and fuel per input, which the specification states are not a measurement of time or energy (C.6). A receipt's joule terms are estimates (est) or unpriced, and no receipt in this repository holds a counter or meter reading (D.11). A calibrated joules-per-unit model is a proposal (spec/proposals/energy-calibration.md).

What the language guarantees:

1. A program gives the same answer on every computer. Arithmetic, text and floating point each have one defined result, so nothing depends on the machine or the compiler.
2. Every program finishes. Loops have limits and recursion works on smaller and smaller parts of its input, so a program cannot hang.
3. A program's meaning is settled before it runs. Ownership, every case of a match and the program's example lines are part of its Form, so an accepted program never uses memory after giving it away, never leaves a case unhandled and has no example that fails. Where a text does not yet have that shape, the checker names the place and the rule.
4. There is one language, batteries included. The specification at one commit is the language, every module of a program is in it, and the whole standard library is built into the checker: a program writes use enc and has it, with nothing to install, no directive and no flag (rce lib lists the modules). Nothing in this repository depends on a released or pinned version of anything else in it; the library is pinned by hash. A program never breaks because a library or a tool moved.

What is here

This repository holds everything that defines, implements, teaches, exercises or must agree with the language: the specification, the reference checker and interpreter, the Lean proofs, the grammar package, the book, the standard library, the example programs, the conformance suite, the IDE and the playground. All of it is built and checked from the same commit.

The checker reads a program into its Form, naming the place where a text does not yet have the Form's shape; every step is appended to the log D; rce emit translates the program to a target language (Rust, Python, JavaScript and Scala today; every registry language by table is the design); a host runs it on a compute fabric.

Try it

The playground runs the checker, compiled to WebAssembly, in the browser. The RCE Book teaches the language from first principles.

Install

Every commit of main that passes CI is released as rce-<commit>, where <commit> is the first 12 hex digits of the commit hash, and rce-latest points at the newest; there is no typed version number, and rce version prints the commit. The release workflow retains only the 30 newest rce-<commit> releases and deletes older ones, so a commit can be pinned by its release only while it is among those 30. To install the newest on Linux (x86_64, aarch64), macOS (Apple silicon) or Windows (Git Bash), checked against the release's SHA256SUMS:

curl -fsSL https://raw.githubusercontent.com/openIE-dev/rce/main/scripts/install.sh | sh

sh install.sh COMMIT installs one commit's release; COMMIT is the 12-hex-digit short hash, as in rce-<commit>. The container image is ghcr.io/openie-dev/rce, tagged latest and with the full 40-hex-digit commit hash; docs/DEPLOY.md runs a program as a service with it.

Build

rce is built from source with Rust; rustup reads spec/checker/rust-toolchain.toml and installs the toolchain on first build. The default build needs a C compiler only for ring, the crypto provider of the TLS adapter.

git clone https://github.com/openIE-dev/rce
cd rce/spec/checker
cargo build --release
install -m 755 target/release/rce ~/.local/bin/

The desktop IDE, with its own copy of rce, is built from ide/ (see ide/README.md). Its releases v0.1.0 to v0.1.3 are on the releases page of openIE-dev/rce-ide, the repository the IDE lived in before it moved here. New IDE releases are published from this repository by .github/workflows/ide-release.yml when an ide-v* tag is pushed; none has been pushed yet.

Quickstart

Save this as counter.rce:

intent "a counter that never goes below zero"
    example Inc, Inc, Dec -> 1
    example Dec -> kept: Underflow

state Counter
    n: u64 = 0

event Inc
event Dec

error Underflow

step Counter on Inc -> n + 1
step Counter on Dec -> try n.checked_sub(1) else Underflow

$ rce test counter.rce
ok counter.rce (2 examples, 0 checks)
1 passed, 0 failed

$ rce run counter.rce "Inc, Inc, Dec, Dec, Dec"
0 (initial) Counter { n = 0 }
1 Inc Counter { n = 1 }
2 Inc Counter { n = 2 }
3 Dec Counter { n = 1 }
4 Dec Counter { n = 0 }
5 Dec kept: Underflow

The example lines are part of the program: if one did not hold, the file would require change under W-INT-1.

Commands

Command	What it does
rce check FILE...	parse, type check and admit; one verdict per file
rce test FILE...	the same, and count each file's examples and checks
rce run FILE [EVENTS]	apply events, or run fn main()
rce trace FILE [EVENTS]	reference trace of each example, or of EVENTS, for checking another implementation step by step
rce emit TARGET FILE	form (the Form as JSON), or a target language: rust, python, js and scala today; the emit registry proposal lists the rest
rce fmt [check] FILE...	write the rewrites of the altered rules (W-UNUSED-1, W-DROP-1), then rewrite files in the canonical layout
rce dim [control] [json] [fuel N] FILE	count the behaviours a program can be in and the redundancy of its state (spec 6.10, 10.11)
rce repair [json] [bound N] [known GOOD] FILE	propose a change to a program that requires change, by exact proposers (reuse, lookup by type, the rewrites of rce fmt, one small edit, renames; with a known-good version GOOD, the renaming onto it first) judged by the checker, with no model call (spec 10.13)
rce mutants [json] [bound N] FILE	make every single edit of a program and run its examples, checks and laws on each: the score, what each obligation kills, the vacuous ones (W-MUT-1) and each surviving edit with its diff (spec 6.12, 10.14)
rce host run [GRANT...] FILE D [EVENTS], rce host serve [GRANT...] [http HOST:PORT] FILE D	run a program under the host contract (Appendix E): admitter, log D, adapters, sandbox
rce lsp	language server on standard input and output
rce help, rce version	every command with its words; the commit rce was built from

Section 10 of the specification defines each command. A command line is rce COMMAND WORD... OPERAND... (spec/proposals/positional-cli.md): the words, such as json or fuel N, come before the files, and no argument starts with -. A removed flag exits with status 2 and prints its new spelling, for example --json was removed; write: rce dim json door.rce.

Repository

Path	Contents
spec/book/	the specification, one chapter per file; start at 00-overview.md. 03-syntax.md is the normative EBNF grammar, read by the tools; 16-host-contract.md is the host contract (Appendix E)
spec/RCE-SPEC.md	the specification as one file, generated from spec/book/ by rce-book build
spec/checker/	the reference parser, type checker, interpreter, emitters, formatter, language server and host runtime (Rust); also rce-spec-check, rce-book, rce-spec-data and rce-fuzz
spec/checker-wasm/	the checker compiled to WebAssembly; spec/wasm-test/ tests the package against the examples
spec/lean/	the Lean 4 model of the core language and its proofs (section 8); scripts/lean-audit.sh checks the axioms
spec/examples/	programs the checker must accept, and in change/syntax/, change/types/ and change/admission/, programs that must require change
spec/traces/	reference traces of the example corpus
spec/data/	the specification as data (grammar tables, rules, method and cost tables)
spec/proposals/	design proposals and the decision ledger (LEDGER.md)
spec/fuzz/	results of the grammar-level program fuzzer
tree-sitter/	the tree-sitter grammar package for editors (grammar, generated parser, queries, bindings); the checker's independent second parser
book/	The RCE Book (mdBook); every listing is checked by book/scripts/check-listings.sh
playground/	the browser playground
stdlib/	the standard library (stdlib/lib/), its vectors and checks; the protocol libraries written in RCE are stdlib/lib/crypto.rce (SHA-2, X25519, Ed25519, X3DH, double ratchet), stdlib/lib/hpke.rce (RFC 9180), stdlib/lib/mls.rce (RFC 9420), stdlib/lib/pq.rce (ML-KEM) and their companions (framing.rce, grp.rce, protect.rce, treekem.rce, welcome.rce)
rcedb/	RCEdb: the log as the database, indexes written in RCE
apps/	applications run by rce host: end-to-end encrypted chat, an SFU and a terminal
programs/	example programs by area (body, data, money, network, science, systems, text, world, hardware, media, multi) and the ecosystem programs
examples/	Form, surface and ingest examples
conformance/	the implementation-independent conformance suite, its harness, adapters and reports
lang/	pinned oracles (rce-oracle/1) and corpora (rce-corpus/1) for Go, Python and JavaScript, the recorder corpus.py and the generator generate.py; the Python lift spec/lift/python carries 6 of the 92 Python cases (lang/README.md)
ide/	the editor, language server, MCP server and sandbox, built on spec/checker
compile/	RCE Compile: a research project, independent of RCE's checker and Form, that tests whether one Law of Compilation holds for every compiler; its charter, registered hypotheses and experiments, starting with E1, the determinism of lowering (compile/README.md)
docs/figures/	figures with captions, scripts and data
scripts/	repository scripts: proofs and Lean audit, cross-architecture hashes and determinism streams, the Form corpus generator, claim counts, demos
.github/workflows/	one workflow per directory; each builds the checker from the current commit and runs that directory's checks against it, except compile-e1.yml, which runs RCE Compile's experiment E1 and does not use the checker

Checking the specification

cd spec/checker
cargo run --release --bin rce-spec-check
cargo test --release

rce-spec-check reads the grammar from spec/book/03-syntax.md, builds LALR(1) tables and fails on any conflict, parses every example with two parsers that must agree, runs the checker over all accepted examples and all that require change, and checks that RCE-SPEC.md matches the chapters. With --features tree-sitter (needs a C compiler and the tree-sitter CLI) it also regenerates the tree-sitter parser and uses it as a third parser. The emitter tests need rustc, python3 and node; a missing one is reported as skipped.

Status

The specification is a draft under review. The reference interpreter defines what programs mean and is not built for speed; there is no production compiler. Section 10.8 lists what the tools do not do yet. Counts quoted about the specification and the checker are taken from the source by scripts/claim-counts.py check; a count is not a test result.

The research site and the experiments (research-openie-web, openie-research-experiments) read this repository; this repository never reads them.

Contributing

See CONTRIBUTING.md. Everyone taking part follows the code of conduct.

License

Copyright (c) 2026 Open Interface Engineering, Inc.

Licensed under either of

• Apache License, Version 2.0 (LICENSE-APACHE)
• MIT license (LICENSE-MIT)

at your option. Unless you explicitly state otherwise, any contribution you intentionally submit for inclusion in this work shall be dual licensed as above, without any additional terms or conditions.