EvoCC

An experimental C compiler, written by AI agents.
Agents propose. Checkers decide.

EvoCC is an experimental C compiler for AArch64 Linux and macOS, x86-64 Linux and RISC-V64 Linux. AI agents wrote it from scratch in Rust and Lean 4, in under three months, under the direction of one engineer: about 2,400 commits, 350,000 lines of Rust and 69,000 lines of Lean by release 0.1.0. It has its own preprocessor, parser, three intermediate representations, optimizer, register allocator and assembly emitter. On AArch64 Linux it builds a Linux kernel that boots, SQLite, Doom and other real C programs. On x86-64 and RISC-V64 Linux it builds userspace programs such as SQLite, Lua and toybox.

One rule runs through the whole compiler: an untrusted part proposes, and a small checker decides.

The same checks serve your programs. EvoCC's typed IRs keep each rule of C as an explicit check, so evo check names the exact operation that breaks one, also when GCC's warnings and UBSan miss it (undefined behavior). Use evocc in place of cc, and give evo mcp to your coding agent.

Why EvoCC

• AI agents wrote the compiler. The paper tells how one engineer directed them, what they got wrong and which checks caught it.
• The IRs keep the rules of C. C-HIR keeps C's types, which bytes are initialized and which object each pointer may point to. EvoIR is typed SSA: each rule of C is a predicate and an obligation that no pass may delete, and memory and I/O travel on explicit tokens.
• Lean 4 proves each rewrite rule of the EqSat optimizer (-Oeq-scalar) for every bit width. For the core-v1 subset on AArch64 Linux, evo prove has Lean 4 check each stage, from typed Core source to the final assembly text (checked optimization, compiling with proof).
• In registered experiments, agents needed fewer steps or tokens with EvoCC on the bugs that GCC's warnings and UBSan miss (Built for agents).

One line through the typed IRs

Line 7 of mean.c at four stages of the release compiler:

Proven on real code

These results are for AArch64 Linux. The 0.2.0 compiler measured the 15 application lanes and Doom on 2026-11-04 and 2026-11-05, and its build of commit c8f36c48 built the kernel on 2026-11-05. Records: Linux kernel, SQLite test log, application lanes, Doom and c-testsuite, Csmith and Lean 4 rules. The status page and the evidence give each count with its limits.

On each target

Subject	AArch64 Linux	x86-64 Linux	RISC-V64 Linux
Linux kernel	builds and boots	no kernel build	no kernel build
c-testsuite	220 of 220	220 of 220	220 of 220
SQLite, Lua, zlib, cJSON	tests pass	tests pass	tests pass
toybox	same results as GCC	same results as GCC	same results as GCC
Zstandard	tests pass	tests pass with -DDYNAMIC_BMI2=0	tests pass
jq	tests pass, 69 of 70 files by EvoCC	8 of 9 test scripts	8 of 9 test scripts
Csmith	0 mismatches in 1,000 programs	0 mismatches in 800 programs	not run
Mbed TLS, TinyCC, musl, PolyBench, Doom	0 EvoCC failures	not run	not run

jq's vendored decNumber.c overflows int in one of its tests, and EvoCC traps on that undefined behavior. With -fwrapv on that file, all 9 scripts pass on x86-64 and RISC-V64. On AArch64, GCC compiles that file. Records for x86-64 and RISC-V64: the x86_64-ladder-* and riscv64-ladder-* files in tests/contracts/, and the toybox, jq, Zstandard and kernel measurements.

Built for agents

An agent repairs C in a loop: build, run, read, edit. It can act only on what the tools report. In 18 programs of our experiments, GCC 14's warnings and UBSan reported nothing for an uninitialized read, a dangling pointer or an out-of-bounds access. evo check reports each of them with a stable code and the line, in a JSON record.

What the agent sees

In this program, prepare() keeps a pointer to its local array, and byte_at() reads through it after prepare() returns. GCC 14 with -O0 -Wall -Wextra -fsanitize=undefined gave the agent this record. The fixed program gives the same record, byte for byte:

=== build exit 0
=== run exit 16
--- stdout
--- stderr

EvoCC's record adds the JSON result of evo check. Its rendered field, with the path shortened:

error[E3010]: dangling-pointer-access
  --> input.c:43:12
   |
43 |     return view->data[index];
   |            ^^^^^^^^^^^^^^^^^ dangling-pointer-access
   |
   = note: this operation failed on the executed path

On the six dangling-pointer programs, Qwen3.8 27B repaired 3 of 18 trials with the GCC record and 18 of 18 with the EvoCC record.

What an agent gets

• A stable code for each finding, such as E3010, and the line. evo explain E3010 gives the rule, with examples that a test runs against the compiler.
• One exit-status rule for each of evo run, check, explain, fix, prove and build. With --json, each writes one JSON object per line.
• Repairs as data. evo fix --plan lists repairs and edits nothing. evo fix --apply applies only safe repairs; a review repair needs a human.
• The same records for the same input. A test runs run, check, explain, fix --plan and prove twice on fixed inputs and compares the JSON, apart from temporary paths.
• evo mcp, which serves run, check, explain, prove and fix_plan (setup). AGENTS.md, also as llms.txt, and the EvoCC skill give the commands, the exit codes and the review rule.

What we measured

We gave agents the same bugs with GCC and UBSan or with EvoCC, and registered the predictions before each measured run.

• Kimi K3, 144 sessions: p < 0.001 for each step saving and for 40% fewer tokens on short programs.
• Three chat models, 432 trials of one answer: p < 0.01 for each token saving.
• Repairs: more with EvoCC for Qwen3.8 27B, p = 0.004. The others repaired nearly all with both.
• Control bugs, which GCC and UBSan report: about the same repairs with both.

Not every experiment separated the toolchains:

#	Model and programs	Result
1	DeepSeek V4.1 Flash, as a chat model; 30 short programs	no difference: 91 to 98% repaired on the first try with each toolchain, a ceiling
2	DeepSeek V4.1 Flash and Qwen3.5 9B; 30 longer programs	inconclusive: most answers ran out of output tokens or time, and the spending limit stopped the run
3	Kimi K3, as a coding agent; pilots	without a sandbox, the agent downloaded the original sources; with one, a ceiling again
4	Kimi K3, sandboxed; 18 silent bugs, 6 controls	the same repairs, 23 of 24 with each toolchain; fewer steps with EvoCC, found after the run
5	Kimi K3, registered replication; 18 short and 12 longer programs	fewer steps and fewer tokens with EvoCC, p < 0.001
8	DeepSeek V4.1 Flash, MiniMax M3.1 Flash and Qwen3.8 27B, as chat models; the bugs of 4	fewer tokens with EvoCC for all three, p < 0.01; more repairs with Qwen3.8 27B, 54 against 30 of 54

Protocols 6 and 7 have pilots only. Agent experiments gives each protocol, receipt and transcript, and the commands that reproduce each analysis without a model call.

Quick start

Install

Build 0.2.0 from source. You need Git, Rust and 25 GiB of free disk space:

git clone --branch v0.2.0 https://github.com/onehr/evocc.git
cd evocc
cargo build --release --offline --locked -p evocc -p evocc-proofcheck
export PATH="$PWD/target/release:$PATH"

This gives evo (the commands), evocc (the compiler) and evocc-checker (the certificate checker). evo prove also needs evoir-sem (the Lean checker). Installation shows its build and the headers of each target. We build and test EvoCC on macOS on Apple silicon and on AArch64 Linux. Version 0.1.0 has prebuilt archives for these two hosts; it compiles for AArch64 only.

The example programs below are in examples/.

Compile, as with cc

$ evocc hello.c -o hello && ./hello
Hello, world!
$ make CC=evocc

Compile for x86-64 or RISC-V64

Each target needs its Linux headers and a GCC for that target, which assembles and links:

$ evocc --target=x86_64-unknown-linux-gnu --sysroot=DIR --assembler=GCC --linker=GCC hello.c -o hello
$ evocc --target=riscv64-unknown-linux-gnu --sysroot=DIR hello.c -o hello

DIR holds the headers in usr/include, and GCC is a GCC for x86-64 Linux. On Linux, the RISC-V64 command finds riscv64-linux-gnu-gcc itself. qemu-riscv64 -L /usr/riscv64-linux-gnu ./hello runs the RISC-V64 program on another machine. Installation shows where the headers come from.

Find a famous bug

first_bad.c has the binary-search bug that broke Java's Arrays.binarySearch in 2006:

int mid = (lo + hi) / 2;

GCC 14 and Apple Clang compile it with -O2 -Wall -Wextra and give no warning. The GCC program does not finish. The Clang program stops with a trap. evo check shows the cause:

$ evo check first_bad.c
error[E3004]: signed-integer-overflow
  --> first_bad.c:9:19
   |
 9 |         int mid = (lo + hi) / 2;
   |                   ^^^^^^^^^ signed-integer-overflow
   |
   = note: this operation failed on the executed path

Change the line to int mid = lo + (hi - lo) / 2;, and the check passes.

See what UBSan misses

In mean.c, the declaration struct stats s; gives count and total no value. GCC with -Wall -Wextra -fsanitize=undefined gives no warning and no report. The program returns 0 at -O0. At -O2, it returns a wrong value that changes from run to run. The right answer is 4.

$ evo check mean.c
error[E3001]: read-of-uninitialized-object
  --> mean.c:7:9
   |
 7 |         s->count += 1;
   |         ^^^^^^^^^^^^^ read-of-uninitialized-object
   |
   = note: this operation failed on the executed path
$ evo explain E3001 | head -n 3
# E3001: read-of-uninitialized-object

The executed path reads object bytes that have not been initialized.

Prove a compilation

$ evo prove abs.c -o abs.s
checked from typed Core source to final assembly text: …/checked/record.json

Lean 4 checks each stage of this compilation, from typed Core source to AArch64 Linux assembly text. If a check fails, evo prove writes no output. abs(INT_MIN) has no valid result in C, so the checked assembly traps instead of returning a wrong value:

    subs w0, w1, w0
    b.vs .Labs_block4
    ...
.Labs_block4:
    brk #3004

subs computes 0 - a and sets the overflow flag. On overflow, b.vs jumps to the trap.

Give it to your agent

$ claude mcp add evo -- evo mcp

The evo commands also write JSON with --json. Agents shows the setup for Claude Code and Codex.

What it compiles correctly

Doom / Freedoom Headless replay results	TinyCC paints reflections Compiles a ray tracer results	Lua explores a fractal Floating-point pixels results
SQLite 0 errors in 329,803 tests results	jq make check passes 69 of 70 C files by EvoCC results	cJSON 216 unit tests, 0 failures results
Linux 6.18 make CC=evocc; boots on 4 CPUs results	Toybox 1,669 tests, same results as GCC results	Mbed TLS seals pixels Encrypt, restore, reject results
Zstandard packs a fractal Identical pixels results	zlib ships a tiny arcade Sprites restored intact results	PolyBench models a field FDTD-2D simulation results
OpenTyrian Three frames match GCC results	Neverball One disclosed source fix results	Quakespasm / LibreQuake 3D demo replay results

Each image is program output, a plot of it or an excerpt of a recorded test log on AArch64 (capture notes and credits, compatibility table). On each target gives the results on x86-64 and RISC-V64.

How it works

• C-HIR keeps the meaning of C: types, evaluation order, which bytes are initialized and what each pointer may point to. evo run executes this level.
• EvoIR turns the undefined-behavior rules of C into explicit checks. evo check executes this level. An optimization can remove work, but never a check.
• EvoMIR treats the machine as data. Registers, calling conventions and instruction encodings are tables in targets/, with one directory for each architecture.
• Lean 4 proves the 62 rewrite rules of the optimizer. For core-v1 on AArch64 Linux, five Lean checkers compare the input and output of each stage, and one theorem covers that chain.

The release compiler made this EvoIR and this assembly from abs.c:

Where EvoCC fits

A sanitizer instruments one optimized build and reports a bug when that build reaches it. CompCert proves its passes correct once, for every program in the C subset that it accepts. EvoCC sits between the two. It compiles large real programs, keeps the rules of C explicit in every stage and checks the path that a program runs. Lean 4 proves the rewrite rules of its optimizer and, for a small subset, checks whole compilations.

Add a proved optimization

In EqSat mode, a new optimization is an equality with a Lean 4 proof, not a new pass:

Your First Proved Optimization follows the rule x + 0 → x through the registry, its Lean proof, the compiler and the checker, and runs it on a real program.

Scope of 0.2.0

EvoCC 0.2.0 is a prototype.

• It compiles for four targets:

  --target	Platform	Scope
  aarch64-unknown-linux-gnu	AArch64 Linux	Programs and the Linux kernel. The only target of evo prove.
  aarch64-apple-darwin	AArch64 macOS	Programs.
  x86_64-unknown-linux-gnu	x86-64 Linux	Userspace programs.
  riscv64-unknown-linux-gnu	RISC-V64 Linux (RV64GC, LP64D)	Userspace programs.

  The tests run x86-64 programs under Rosetta and QEMU, and RISC-V64 programs under QEMU. The proof-required path refuses both targets with exit status 6.

• x86-64 and RISC-V64 have no kernel build. Each compile command of the kernel has a flag that EvoCC refuses on these targets, and its headers and inline assembly need more forms (measurements).

• toybox needs workarounds on x86-64 and RISC-V64, and Zstandard on x86-64, because EvoCC refuses some forms and flags that they use. The measurements list them.

• Its AArch64 code is 1.8 to 2.3 times the size of GCC -O2 output on five library files, and it is not tuned for speed (evaluation).

• evo check checks the path that a run takes, not all inputs. It runs programs that do not call the C library (undefined behavior).

• Proofs cover core-v1: integer functions with loops, switch, the narrow integer types and calls, without pointers, arrays, global objects, floating point or recursion, from typed Core source to AArch64 Linux assembly text. Parsing, assembly, linking and other C programs are not proved (verification contract).

• GNU C support is broad but not complete, and full kernel test acceptance is open. The changelog lists each known limit.

• The agent results use injected bugs in programs adapted from zlib, Zstandard and cJSON: one coding agent at low reasoning effort with two repetitions, and three chat models with three. They do not rank models or toolchains (limits).

x86-64 and RISC-V64 Linux

--target=x86_64-unknown-linux-gnu compiles C for x86-64 Linux userspace. Of 800 Csmith programs, 739 give the same checksum from EvoCC at -O0, from EvoCC at -O2, and from GCC 14 and Clang 19; no checksum differs. The target compiles thread-local storage for a static executable, a PIE and a shared object, inline assembly with operands in the subset of GCC's x86 constraints, with clobbers and register variables by register name, and an over-aligned object next to a variable-length array; the tests x86_64_tls.rs, x86_64_asm.rs, x86_64_register_variables.rs and aligned_frames.rs compare the output with GCC 14 under Rosetta and under QEMU. The target also compiles GNU vectors and _Float16. vector_forms.rs compares the output with GCC 14, and vector_abi.rs and x86_64_half_boundary.rs cross each call in both directions between builds of GCC 14, Clang 19 and EvoCC. vector_abi.rs leaves Clang 19 out for the vectors that it passes another way than GCC 14.

--target=riscv64-unknown-linux-gnu compiles C for RISC-V64 Linux userspace (RV64GC, LP64D). All 220 programs of c-testsuite give the output that the suite expects in static, PIE and shared builds. The target compiles thread-local storage, inline assembly with operands, asm goto, _Complex long double, _Float16 and GNU vectors. riscv64_half_records.rs and vector_abi.rs cross each call in both directions between builds of GCC 14, Clang 19 and EvoCC.

Learn more

• Architecture: the pipeline, crate interfaces and trust boundaries.
• The EvoCC Book: installation, a first program, undefined behavior, proofs and agents.
• The paper: how agents built EvoCC, its design and its evaluation.
• Specifications: EvoIR, EvoMIR, the target tables and the verification contract.

Contributing

Read CONTRIBUTING.md. To report wrong code, open a pull request with a failing test, or use the wrong-code issue template.

License

Apache License 2.0. Copyright 2026 Haoran Wang, NexRidge. See LICENSE, NOTICE and THIRD-PARTY-NOTICES.md.