ruby-lean: A Ruby semantics with a type soundness proof

Bottom line up front: I, with heavy augmentation from LLMs, have built an executable model of Ruby's semantics in Lean, together with a proof of type soundness for a small fragment of Sorbet's type system built on the semantics. The semantics is validated by differential testing against Ruby and passes a large swath of conformance tests. Through this project, I learned firstly that agents do great at long-horizon tasks if the task definition is clear; if it is not clear, they mess up in unpredictable ways. Secondly, I learned that advanced AI, via its ability to work with proof assistants, has the potential to revolutionize how we manage the correctness of software.

Check out the ruby-lean playground and see it in action. For the technically inclined, see the Technical Appendix. View the source code on GitHub.

Introduction: "Semantics Done Quick"#

Suppose you have a program in your language of choice, and you want to prove that it is correct. Proof here means for all inputs, of which there could be infinitely many. No amount of unit tests can satisfy that obligation.¹ So, you need a mathematical argument. This is where formal methods shines.

How might you mount a mathematical argument for the correctness of a program, though? First, you need to define correctness. A simple definition is "this program terminates and returns a value." Now, you need to define meaning. To see why, take the program "2" + 2. The meaning of this is ambiguous because it depends on the programming language. If you've ever written JavaScript, you may recognize that this program evaluates to "22". In Ruby, this program throws an exception. These outcomes hint at the computational intent of the statement in each language. In JavaScript, the meaning is approximately "concatenate the string '2' with the result of coercing 2 into a string." In Ruby, the meaning is "attempt to call the string's + operator with 2 as an operand, which attempts to coerce 2 using the to_str method." This fails as the code for String#+ executes, because the Integer class has no to_str method. This definition of meaning, given by computational intent, is known as a programming language's semantics.² When the semantics is loaded into a proof assistant like Lean, we can mechanically reason about programs and their correctness!

Armed with a definition of correctness and a semantics, consider a program like "2" + x, where x is some input variable. In JavaScript, this program is correct for any x except specific cases like x = Symbol(). In Ruby, this program is correct for any x that can be coerced into a string (i.e., x has a to_str method). To make the Ruby program correct for all inputs, we can make the to_str check explicit:

"2" + x if x.respond_to?(:to_str)

The astute reader might notice that even this is not correct! Evaluating x.to_str could still raise an exception or not terminate.

These example programs are dead simple, and yet they still have many edge cases that are hard to reason about. This is why modeling the semantics of entire programming languages has historically taken multiple PhD-years of effort. Mike Dodds proposed Semantics Done Quick out of the belief that advanced AI should be able to greatly accelerate the construction of useful semantics. I say "useful" because results about semantics make it to academic conferences but don't find broad use in industry.

Why? It's not that semantics are inherently useless. Quite the opposite: they are generally useful because we can vary our definition of correctness to suit the task at hand. They can be used, for instance, to prove soundness of type checking, which states that if a type checker—like Sorbet, which is widely used for Ruby—accepts a program, then the typed parts of the program are truly free of type errors. This has immediate business value: it provably rules out certain uncaught exceptions in production code. Semantics can additionally be used to prove robustness against malicious inputs so that software can be relied on in security-critical contexts.

Rather, semantics are not adopted because:

they often have severe limitations, such as not being able to model the complex parts of a given language, which tend to be the most useful; and
authoring proofs against them requires technical expertise in formal methods and in the specific nature of the semantics.

Advanced AI shows promise in addressing both of these impediments.

This summer, I worked on this project as a fellow in the Apart Research Secure Program Synthesis fellowship. As an outcome, I am pleased to announce ruby-lean, my semantics of Ruby in Lean 4. ruby-lean is an executable semantics, meaning that it can execute real Ruby code. It is modeled as a CESK machine. To demonstrate that this semantics is indeed useful, I have also developed a system of type judgments based on Sorbet and proven it sound. I defined soundness above, but to reiterate what this concretely means here: if a program passes the ruby-lean type validator, then it is completely free of a certain family of type-related exceptions. Both of the aforementioned impediments to widespread use of this semantics are effectively addressed: the semantics models complex features of Ruby like method_missing and eigenclass reopening, and a substantial theorem about a type system has been written and proven.

I can probably count on my hands the number of lines of actual Lean code I wrote by hand. Frontier AI breezed through a lot of this project, but when it came to the most difficult part of proving a hard property against the semantics, AI struggled, and I intervened by crystallizing the task definition, the theorem statements, and the proof design approach. Admittedly, it was somewhat refreshing to find a task that AI does not immediately excel at, and I came away with some learnings about how to best steer AI on complex tasks like these.

In sum, my results here illustrate that:

Semantics can be built quickly (~2.5 months of part-time human labor + agents).
Semantics with AI-authored proofs provide a foundation to scale correctness claims up to all programs in ways that fuzzing or other empirical methods will never be able to.

`ruby-lean` and its type validator#

A live demo playground is available. It is seeded with many example Ruby programs. Play around with it!

The five pipeline stages: 0, read the annotations (what types the program declares); 1, remove the annotations; 2, desugar Ruby into the small core the model runs; 3, propose a proof (untrusted); 4, check the proof (the trusted step).

Here are the five stages of the program analysis pipeline:

Run Sorbet on a program with specific flags, so that Sorbet emits annotation information.
Strip the program's annotations, since Sorbet annotations are real syntax that's outside of what the Lean model supports today.
Desugar³ the program, producing an s-expression that builds programs from a core set of Ruby primitives.
Run an untrusted certificate emitter (a companion program written in Ruby) that proposes a type derivation for the program. A derivation is like a conjecture about what types the methods and variables have in a program.
Run the trusted validator, given as validateD p d in ruby-lean's code. This validates the type derivation against the program. The validator returns true if the derivation accurately types the program according to its internal rules, and we have proven a theorem that demonstrates the soundness of this validation procedure.

Here's how the pieces fit together, and where the trust boundary lies:

flowchart TB
    subgraph untrusted["Untrusted"]
        corpus[("Corpus of typed<br/>Ruby programs")]
        anyprog[/"Any Ruby program"/]
        prog(["Program p"])
        sorbet["Sorbet"]
        emitter["Certificate emitter"]
        cruby["CRuby 4.0.5"]
    end

    subgraph tcb["Trusted computing base"]
        subgraph tcbruby["Ruby"]
            rubypad[" "]
            sigstrip["sig_strip"]
            desugarer["Desugarer"]
        end
        subgraph tcblean["Lean"]
            validator["Type Validator<br/>validateD p d"]
            proof["Soundness proof"]
            semantics["Semantics<br/>(CESK machine)"]
        end
    end

    corpus --> prog
    anyprog --> prog
    prog --> sigstrip
    sigstrip -->|"sig_strip(p)"| desugarer
    prog --> sorbet
    sorbet -->|"type information in p"| emitter
    desugarer -->|"core program"| validator
    emitter -->|"derivation d"| validator
    proof -.->|"proves sound"| validator
    proof -.->|"over"| semantics
    cruby -.->|"differential<br/>testing"| semantics
    cruby -.->|"differential<br/>testing"| desugarer
    emitter ~~~ sigstrip
    sigstrip ~~~ proof
    validator -->|"true"| verdict(["p has no type errors"])

    style rubypad fill:none,stroke:none
    style untrusted stroke-dasharray: 6 4
    style tcb stroke-width: 3px

"Why should I trust this?"#

My semantics is validated against Ruby by differential testing. I have implemented a multi-pronged conformance suite, where each prong generates test cases with a different methodology. This is explained in more detail in the Technical Appendix.

If you have doubts, see for yourself: I have released a playground where you can run Ruby code in original Ruby alongside the Lean semantics, via compiled artifacts in WebAssembly. The code is open-source as well.

I am not pretending that the semantics is perfect. In fact, I recently discovered, during a differential testing campaign, an instance of non-conformance related to the example Ruby program given in the intro. I have not yet patched this, so you can run this program to convince yourself that CRuby and ruby-lean are two distinct models of the language:

class WithToStr
  def to_str = "ok"
end

puts "hi" + WithToStr.new

# ruby-lean: TypeError: no implicit conversion of WithToStr into String
# CRuby: hiok

The behavioral difference is that original Ruby automatically coerces the right-hand side of a string's + via its to_str method. The ruby-lean semantics has not captured this behavior yet. When this is patched, I'll make a note of it here.

In the type judgments and the soundness proof, I guarded against proof-slop by carefully auditing the end-to-end theorem statement. This theorem, given in the Technical Appendix, is an easy-to-interpret statement that directly relates the validator to the stuck-freedom property.

The Lean kernel still has to be trusted, and soundness bugs in it have been found in the past, but I have no reason to believe that agents exploited any of them. I took great care to make sure that the tasks the AIs were given were achievable. I did not give them impossible goal statements and gave them emergency exits from goal pursuit that they could use if needed (a suggestion borrowed from Mike Dodds).

"Why Ruby?"#

I chose Ruby for a few reasons:

It isn't Python. Python has been treated rather extensively in the literature. It amusingly appears to be a popular topic for master's theses.⁴ Ruby has some prior art, and I used it as inspiration for certain parts of the semantics, but in general it seems that Ruby is more "out of distribution" for frontier AI than Python.
It has high-profile users in industry. Notably, Stripe has one of the largest Ruby codebases in the world. Stripe processed 1.6% of global GDP in 2025, so this Ruby codebase can be seen as a critical piece of global infrastructure. Beyond Stripe, Homebrew is written in Ruby. Ruby on Rails is a mainstay in web development. Shopify is a prominent user of Ruby on Rails, and was funding academic research on Ruby as of several years ago.
It's complicated. Ruby has features, absent in Python, that complicate static analysis. The example that immediately comes to mind is that of blocks. In Ruby, it's possible to pass a block to a function. A block is sort of like a lambda, except it has different scoping rules and multiple ways that it can return. I believe there's a solid chance that Ruby is "semantics-complete." That is, if we can solve Ruby, we can solve semantics for every other language.⁵
It has a de facto type checker. Sorbet was created at Stripe, and it is used at Stripe and beyond. Sorbet is unsound by construction, allowing T.unsafe(...) as an escape hatch. However, we are particularly interested in the maximal sound fragment of Sorbet that we can model. Any soundness bug in Sorbet, where it claims a typed program is safe when it is not, would be immediately relevant to Ruby/Sorbet users.

Cost of verification#

Following Quinn's advice, I report the verification burden here.

The work to obtain this result unfolded over the course of ~2.5 months, at 10–20 hours per week of human labor, with $9,000 of token budget provided by Apart Research.

The model used to author most of the code was Claude Opus 5. I occasionally used Claude Fable 5 as a consultant, but I shied away from using it for grindy sessions because I found that it burned through tokens far faster than I intended, without much of a speedup in the ladder climb. The final push towards the soundness proof over a nontrivial fragment of Ruby that is presented here was grinded with the new GPT 6 Astra model, which I found did a very good job at a more reasonable cost, but this may also be due to the more rigorous ratchet discipline I imposed in my most recent attempt at growing a sound type system.

Limitations#

This work is limited by the fragments of Ruby semantics and Ruby types that are covered. The semantics has a ways to go before it models the long tail of esoteric Ruby features, and the type system still needs to be grown to cover frequently used Ruby constructs like blocks. In case it is not clear: the semantics and the type system cover two different sets of Ruby constructs. Blocks are well supported by the semantics, but not yet covered by the type system. As a rule of thumb, it is much harder to admit a construct to the type system than to the semantics, because of the proof required.

The semantics also does not model Ruby programs' interaction with the surrounding system context, like the RubyGems package manager, the operating system, or the network. Modeling these interactions will be essential for industrial-grade reasoning.

Aside from the limitations of the project as it's currently scoped, there are several interesting open research questions in the science of growing these semantics and steering agents to complete long-horizon proof tasks within them.

Specifically,

I have not developed a theory of how best to steer LLMs to obtain useful semantics. This will require time and funding to run more controlled experiments and benchmarks.
I did not run any comparison between different LLMs/harnesses for the tasks here, except for a brief stint playing around with GLM 5.2 and GLM 5.3, to no avail. I expect that performance will vary significantly with respect to model choice, reasoning effort, choice of agent harness, and prompting strategy. ruby-lean provides a nice environment for evaluating how agents can reason about a complex logical system. A benchmark could look like a set of properties about Ruby and its types, where the agent's job is to prove or disprove them.

If you are interested in working on/funding this project or its future directions, let me know.

Future work#

My immediate next steps are:

Grind the semantics to cover any reasonable Ruby program.
Grind the type system enough to run the type validator on a repo in the wild (Homebrew is my initial target). At a minimum, this includes reasoning about the types of blocks, flow sensitivity, and class inheritance with mixins.
Attempt to find real Sorbet unsoundness (i.e., not just unsoundness introduced by deliberate escape hatches).

Beyond these, something I would like to explore more is leveraging the semantics for adversarial synthesis of deserialization attack chains. This is a recurring bug class in Ruby and probably in other languages; deserialization of uncontrolled input is a huge attack surface.

Learnings and final thoughts#

Want to build something similar? Take away these learnings so that hopefully you don't have to tear down your work multiple times like I did :).

ALWAYS have a clear idea of what you want the agent to do, unless you're deliberately exploring and okay with potentially throwing out whatever the agent gives you.
Having a ratchet discipline, where an agent can only make progress by pushing some metric up, is important.
Do not be wishy-washy in prompts. Be direct about what you're asking for and what the definition of done is.
Clean up the code regularly to remove the buildup of agent-authored cruft. This is something I did not do, and now I'm paying for it.
Deep thinking about the logical structure of semantics (or whatever you're trying to do) is still necessary. Relying too heavily on agents at times made me more confused and biased me towards certain nonsensical ways of thinking about the problem. I made real progress at inflection points where I decided to let go and rebuild my mental model from first principles.
This is a technical detail, but one you can include in your prompts to your agents: try to prove lemmata that allow for decomposed reasoning. For example, a continuation stack decomposition lemma proved very useful for expediting several proofs.⁶
Commit regularly and save agent transcripts with /export to a journal folder for posterity. I have had agents search them to find context from past discussions, and this has been helpful at times.

This post is less of an announcement of a finalized piece of work than a check-in on one that is very much in progress, so I'm sure I'll have more learnings to report soon.

Ultimately, I think you should take away the elegance of this pattern of using an agent to formalize something with respect to some black-box oracle. It works quite well, and it can even be applied to specific software systems or libraries (e.g., the Ruby on Rails framework) instead of plain programming languages. This technique is useful anywhere you may want to abstract away the messy details of the implementation and reason about the higher-level behavior.⁷ You just need to build confidence that the model is faithful by developing a really strong test suite.

Finally, I have simply been blown away by how good LLMs are at most engineering tasks, but they are only as good as the task definition you give them. Sadly, this makes me more afraid than I used to be about the deployment of AI agents at scale on tasks where their performance is not being properly evaluated or not evaluable in the first place...

Acknowledgements#

Thank you, Eitan Sprejer and the Apart Research team, for your support in this project.

Thank you, Mike Dodds, for your mentorship and feedback on this piece. Thank you, Max von Hippel, Victor Arsenescu, and Dana Wensberg for your helpful comments as well.

And thank you for reading. Want to get involved? Reach out at s.xifaras999@gmail.com!