I built the RealWorld app in Lean 4

1Introduction

Lean 4 is a functional programming language in the same family as Haskell and OCaml. Most people know it as a proof assistant. Lately its standard library has also gained an HTTP server. The community is writing the other libraries that ordinary apps need too, like Postgres drivers, cryptography and HTML rendering.

So can you build a real web app in Lean yet? I built RealWorld in it to find out. RealWorld is a well-known reference app, a Medium clone that comes with official test suites for its API and its website. My version is written entirely in Lean including the frontend, which uses datastar-lean for interactivity. The code is on GitHub.

I’ve written this post like a math paper, mostly because it’s fun and partly because it keeps the structure clear. Most of what follows is still plain engineering of the kind you would do in any language. The few things that are actually proved are marked as propositions. Lean checks those proofs every time the code builds.

2Existence

The first question is whether a RealWorld app can be built in Lean at all. The test suites turn that into something we can check.

The proof is to build one. The test suites define what it has to do. The API tests send HTTP requests and check the JSON that comes back, so we need a server. The data in those answers has to be kept between requests, which means a database. The website tests click through the site in a real browser, so the server has to render pages as well.

route_table Api
  [ ...
    comment := "/api/articles/:slug:String/comments/:id:Nat",
    ... ]

def deleteComment (env : Env) (slug : String) (id : Nat) : Handler := fun req => respond do
  Service.deleteComment env (← requireUser env req) slug id
  noContent

def routes (env : Env) : List (Route Result) :=
  [ ...
    .delete patterns.comment (deleteComment env),
    ... ]

This handler deletes a comment. It checks the user’s login token with requireUser, calls the service layer to delete the comment and replies with 204 No Content. The website calls the same service layer and therefore follows exactly the same rules. Everything else comes from libraries, as it would in any language:

• lean-json for JSON
• lean-libcrypto for hashing passwords with OpenSSL's scrypt
• lean-jose for the login tokens (JSON Web Tokens)
• lean-middleware for CORS, cookies and static files

def userByEmail (db : Conn) (email : String) : IO (Option UserRow) := do
  first (← db sql!"SELECT id, username, email, password_hash, bio, image FROM users
                     WHERE email = {email}")

The {email} inside sql! becomes a query parameter, which Postgres receives separately from the SQL text. So user input can never run as SQL. The database schema is plain SQL that leanmigrate applies when the server starts.

def commentCard (viewer : Option Db.UserRow) (slug : String) (c : Db.CommentRow) : Node .flow :=
  let delete : List (Node .phrasing) :=
    if viewer.any (·.id == c.authorId) then
      [ span [ i [] { class_ := "ion-trash-a" } ] { class_ := "mod-options" }
          [onClick (action "delete" (Site.links.comment slug c.id.toInt.toNat))] ]
    else []
  div [
    div [ p [ c.body ] { class_ := "card-text" } ] { class_ := "card-block" },
    ...
  ] { class_ := "card", id := s!"comment-{c.id}" }

That onClick is all the frontend code needed to delete a comment. Datastar, a small script on the page, sends the DELETE request when you click the icon. It then updates the page with the server’s reply. The server builds that reply with the same function the JSON API uses. There’s no frontend build step because the pages are just HTML plus one script. On the server I use datastar-lean, the official Lean SDK for Datastar that Carlo Hamalainen and I maintain.

3Production

Passing tests on a laptop doesn’t mean an app is ready for real users. So the second question is about production.

There are two problems.

The easiest parts to trust are the types and the theorems, because Lean checks them. Those hold no matter who or what wrote the code. The instructions the libraries give their AI agent push in this direction. They ask for “the strongest form a claim admits: a proven theorem over a property … over an example and an expected result”. They also forbid using sorry as a placeholder for a missing proof. Several of the libraries do include real proofs. Code that no theorem covers is only as reliable as its tests. That goes double for the bindings to C libraries, where Lean can’t check the C code at all.

You still need to read the proved parts, though. Lean checks that each proof is correct, but it can’t check whether the theorem states what you actually need. Agents asked for proofs often prove things that don’t matter. When Dan Luu had coding agents implement Zstd compression and told them to use Lean 4, they mostly proved arithmetic facts that missed the bug-prone code. Those proofs didn’t make the code any more correct⁸. So you still have to read all of it, theorems and proofs included. Check that it does what you need and fix it where it doesn’t. Don’t trust any part you haven’t checked yourself.

Tools like claimcheck can help with that reading. It has an AI model restate each theorem in plain English without knowing what the theorem was meant to say. A second step compares that restatement with the original intent⁹. It’s a useful check, but it doesn’t replace reading.

Partial answer to Question 2. So can the app serve real users? Yes, as long as three things hold: (H1) traffic stays modest, (H2) you pin the toolchain, and (H3) someone actually reads the code. The server’s limits don’t matter while traffic stays modest. You can also run several copies of the app for more load because it keeps no state between requests. A pinned toolchain means a new Lean release can’t break anything until you choose to upgrade. Reading the code is doable where it matters most because the app is only about 1,600 lines. Someone should read its handlers, its SQL and its C bindings carefully before real users see them.

4Correctness

I think correctness by construction is what you should aim for, especially when an AI writes most of your code. It means first writing down exactly what the program should do in a formal language. The code is then derived from that description in steps that are each proved correct.

Today most people rely on tests instead, or hand the agent a spec and hope it follows it. Tests only check the cases someone thought to write. Dan Luu’s experiments also show that agents write poor tests, even when told which technique to use. A spec on its own can’t show that the code actually follows it. Correctness by construction closes that gap, because Lean checks every step from the spec to the code. It’s the only reliable way I see to ship high-quality code while keeping the speed AI gives you.

So the last question is whether this app could be correct by construction. Here is the precise definition.

Definition 2 has two parts, a formal specification and a step-by-step derivation from it. Let’s check each one.

The specification. Does RealWorld have a formal specification? Partly. Its contract is an OpenAPI file plus the test suites. The OpenAPI file is precise about shapes, like which endpoints exist, what fields they take and which status codes they return. What the endpoints actually do is only described in English. The tests pin that down for the specific cases they check, and nowhere else. So RealWorld is formal about types and informal about behavior.

The derivation. Was the app derived from that specification? No. That was a conscious choice. RealWorld is only formal about types, so there’s nothing precise enough to derive the app’s behavior from. Full correctness by construction wasn’t possible with the spec as it stands. So I wrote the app first and tested it afterwards, which is the opposite of what Definition 2 asks for. I picked a few important properties to verify instead. Three of them are guaranteed just because the code compiles. Here they are.

error: Application type mismatch: The argument
  deleteComment env
has type
  String → String → Api.Handler
but is expected to have type
  HandlerType Api.patterns.comment Result

Every handler in Express or Go parses the id itself. A mismatch in Rust’s axum only shows up when a request comes in. One weak spot remains here. I copied the route table from the OpenAPI file by hand. Generating it from the file automatically would close that gap.

Slugs show Definition 2 on a small scale. A slug is the URL-friendly version of a title, like how-to-train-your-dragon. RealWorld doesn’t say what a slug should look like, so I wrote the specification first, as a Lean type called Valid. A single lowercase letter or digit is a valid slug. You can grow a valid slug by putting a letter or digit in front of it, or a letter or digit followed by a hyphen. Nothing else is valid. That rules out empty slugs, hyphens at either end and double hyphens. A Slug is a string bundled with a proof that it follows these rules:

inductive Valid : List Char → Prop where
  | single {c} : isSlugChar c → Valid [c]
  | cons {c rest} : isSlugChar c → Valid rest → Valid (c :: rest)
  | hyphen {c rest} : isSlugChar c → Valid rest → Valid (c :: '-' :: rest)

structure Slug where
  toString : String
  valid : Valid toString.toList

Here’s ofTitle. It calls a helper, chars, which keeps the title’s letters and digits, lowercases them and turns everything in between into single hyphens. Then ofTitle returns that string together with a proof that it’s valid. The proof is the part after by:

def ofTitle (title : String) : Slug :=
  match h : chars title.toList false false with
  | [] => ⟨"article", ...⟩   -- a title with no letters or digits
  | c :: cs =>
    ⟨String.ofList (c :: cs), by
      rw [String.toList_ofList, ← h]
      exact (chars_valid title.toList false).resolve_left (by rw [h]; exact List.cons_ne_nil _ _)⟩

That proof relies on a lemma about chars. It says that for any title, chars returns either nothing or a valid slug. The lemma is proved by induction over the title’s characters:

theorem chars_valid (cs : List Char) (pending : Bool) :
    chars cs false pending = [] ∨ Valid (chars cs false pending) := by
  induction cs generalizing pending with
  | nil => exact Or.inl rfl
  | cons c cs ih => ...

In total that’s about forty lines of proof for ten lines of code. A property-based test would check a few thousand random titles. The proof covers every title including the ones nobody has written yet.

def escapeChar (c : Char) : String :=
  match c with
  | '&' => "&"
  | '<' => "&lt;"
  | '>' => "&gt;"
  | '"' => "&quot;"
  | c    => String.singleton c

theorem escape_safe (s : String) :
    ∀ c ∈ (escape s).toList, c ≠ '<' ∧ c ≠ '>' ∧ c ≠ '"' := ...

RealWorld’s website tests do check for cross-site scripting. They inject malicious text through the API and check that the page shows it as plain text. The suite skips those tests for apps that serve both the API and the pages, like this one. So here the proof is the only check. React escapes text the same way, but there only tests check that the escaping is right.

So this app is not correct by construction. Whether any RealWorld app in Lean can be (Question 3) is still open. Answering it would start with writing RealWorld’s behavior down in Lean. Deriving the app from that would also need a model of SQL, plus proofs about the C libraries and Std.Http underneath. For now, the slug is the only part where the method has been carried all the way through.

Instructions for running the app and both test suites are in the repository.

Acknowledgments. Thanks to Paul Butcher, whose libraries made this possible, and to Carlo Hamalainen for datastar-lean.