←samx.io

ruby-lean/type checking Ruby, with a proof

—

This page runs large WebAssembly modules in your browser — real Ruby and the Lean checker, compiled to wasm. It does not work in Safari. Chrome on a phone does, but for best results use Chrome on your desktop.

target —

The program — Ruby, with Sorbet type annotations. Editable.

Without the annotations — what actually gets checked and run

Certificate — the proposed proof. Edit it and stage 4 will check what you wrote.

The pipeline — press ▸ to run one, or “Check it” for all five

Declared types 

— run stage 0 to read the program's type annotations

The program, desugared — the core form the model runs

— run stages 1 and 2

Verdict — the one trusted answer on this page

— run stages 3 and 4

Run it — the Lean model beside real CRuby. They should agree.

— 
— press “Lean model” to run the program in the formal model
— press “CRuby” to run the same program in real Ruby
Step it one stepFn transition at a time — a printer over the real machine, so whatever the model runs, this shows
—
Trace a program to begin.

Call stack — top frame first

— no trace

Continuations — what happens after

  1. — no trace

stdout so far

—
What is this?

A collection of small Ruby programs carrying type annotations — Sorbet sigs, the kind you would write in a real codebase — and a type checker written in Lean that decides whether each one is safe.

What makes the checker unusual is that it has been proved sound. Not tested until it seemed right: proved, as a theorem, for the fragment of Ruby it covers.

Why?

Production software is littered with bugs and security vulnerabilities. AI has proven very good at exploiting them in Ruby as well as in other languages and software.

As exploit grows cheaper, we must find ways to increase its cost. A guarantee of non-exploitability of software makes this cost approach infinity, but it requires a formal model of the system. Here, we present such a model for Ruby, and we demonstrate that it's useful for proofs with the accompanying type safety result.

How?

This work was steered closely by me, Sam, but heavily augmented by frontier LLMs, and accomplished with a small fraction of the time and effort that would be required to produce this normally. This is a promising sign that a future of true high-assurance software engineering is not far off.

What a green result means

When the checker answers true, that program cannot raise a type error — no NoMethodError, no TypeError, no ArgumentError — no matter how long it runs. That is a mathematical guarantee, machine-checked, not a test result or a heuristic.

The guarantee is about an executable model of Ruby, also written in Lean, which is where the second half of this page comes in.

Why CRuby is here too

A proof about a model is as good as the model's faithfulness. So real CRuby runs beside it: press Lean model and CRuby on the same program and compare. Every program in this collection is checked both ways, and they agree. The model is not a paper description of Ruby with an interpreter next to it — the interpreter is the semantics.

Stepping the machine

Step it walks the model one transition at a time: what it is about to evaluate, the call stack with live local variables, what is waiting to happen next, and the output so far. This is the same machine the proof is about, not a simplified illustration of it.

This is a proof of concept. Of the 259 programs here, the certified fragment currently covers 63. The rest are outside it — the checker declines them rather than getting them wrong, and each one names what stopped it. Blocks and rejections are honest answers about coverage, not failures of the program.

The aim is to grow that fragment toward the whole language and type system, and to leverage it to reason about industrial-scale Ruby programs. Eventually, we can replicate this for every other piece of software. Today the fragment is small, but with a powerful proof behind it.