# What is Lean? Rethinking software testing with proofs and types > Testing and CI pushed me to look at Lean, deterministic functional programming, and formal verification. The way of thinking reminded me of modeling in TypeDB. Published: 2026-11-12 Canonical: https://layerbase.com/blog/what-is-lean-software-testing Running a database platform changes how you think about correctness. A mistake might mean somebody cannot connect. It might also mean a resource gets assigned to the wrong customer, or a database gets deleted when it should not. My usual response is to add a test. Then another test for the edge case. Eventually, testing and CI became something I had to engineer as carefully as the application itself. I still need confidence in every change, but more tests are not automatically more useful evidence. That is what brought me to Lean. I wanted to understand whether some of the rules I keep testing could be stated precisely enough to prove. Formal verification is not new. What is new to me is considering where it might fit into the everyday work of maintaining [Layerbase](https://layerbase.com). This is an exploration with small, checked examples. I have not replaced our production test suite with Lean or measured a CI speedup from doing so. ## What is Lean? [Lean](https://lean-lang.org/theorem_proving_in_lean4/Introduction/) is a programming language and an interactive theorem prover. You can define a function, state a property of it, and supply a proof that Lean checks. A theorem does not have to be something from a mathematics textbook. It can be a statement about software: > Starting, stopping, or restarting a database must preserve its owner. A test might start with customer 42's database, restart it, and assert that customer 42 still owns it. That is useful. A theorem can quantify over every database value and every operation in a defined model. The phrase "in a defined model" matters. Lean does not read that English sentence and establish that my TypeScript services, database drivers, and infrastructure obey it. I have to describe the behavior I want to reason about. The proof applies to that description. ## Deterministic functional programming gives me a smaller problem A useful starting point is a pure function: give it the same inputs and it produces the same result, without reading a clock, changing shared state, or calling a server. Lean supports this style of [functional programming](https://lean-lang.org/functional_programming_in_lean/). For lifecycle logic, I can separate a decision about the next state from the code that performs an external operation. That makes the decision easier to test and reason about. It does not make the external operation reliable by association. Here is a deliberately small Lean model. `Nat` is a nonnegative integer, used here as a stand-in for a customer ID. `Bool` says whether the database is running. ```lean structure Database where owner : Nat running : Bool inductive Operation where | start | stop | restart def step (db : Database) (op : Operation) : Database := match op with | .start => { db with running := true } | .stop => { db with running := false } | .restart => { db with running := true } theorem step_preserves_owner (db : Database) (op : Operation) : (step db op).owner = db.owner := by cases op <;> rfl ``` `{ db with running := true }` returns an updated record. It leaves the other field alone. The theorem says that the owner after `step` equals the owner before it, for any `db` and `op`. The proof splits on the three operations. In each case, the equality follows directly from the definition. `rfl` closes those equalities; it is not a command to assume that they are true. This is intentionally obvious code. It lets us see the entire guarantee. The model does not include a restart that times out, an invalid customer ID, or a process that reports success before it is ready. In fact, its `restart` merely sets a Boolean. It models an ownership-preservation decision, not a real machine restart. Also, deterministic does not mean correct. A function can return the same wrong owner every time. ## What happens when the implementation breaks the rule? Append this deliberately broken operation and theorem to the same file: ```lean def brokenRestart (db : Database) : Database := { db with owner := 0, running := true } theorem brokenRestart_preserves_owner (db : Database) : (brokenRestart db).owner = db.owner := by rfl ``` Lean rejects this proof. The goal reduces to `0 = db.owner`, which does not hold for an arbitrary owner. An ordinary test using owner 0 would pass, while one using owner 42 would catch the bug. The universal statement requires us to account for both and every other owner. A failed proof attempt does not generally mean a statement is false: sometimes I just have not found the proof. Here there is a straightforward counterexample, any database whose owner is not 0. For a less trivial question, return to the correct version. What if a database is stopped, started, restarted, and stopped again? Add this to the first block, without the deliberately failing theorem: ```lean def run (db : Database) (ops : List Operation) : Database := match ops with | [] => db | op :: rest => run (step db op) rest theorem run_preserves_owner (db : Database) (ops : List Operation) : (run db ops).owner = db.owner := by induction ops generalizing db with | nil => rfl | cons op rest ih => exact (ih (step db op)).trans (step_preserves_owner db op) ``` The reasoning is: an empty sequence changes nothing. For a nonempty sequence, the first operation preserves ownership, and the remaining operations preserve it too. That covers every finite list of these modeled operations, without enumerating a maximum list length. There is no ownership-transfer operation in this model. Adding one would require a different statement, perhaps about who authorized the change. Nor does a sequential list model concurrency or partial failures. Those behaviors need explicit representation before a theorem can say anything about them. **Verification:** the complete correct example checks with Lean 4.35.0 using `lean Ownership.lean`. The broken version fails. Adding `#print axioms run_preserves_owner` reports that this theorem does not depend on any axioms. No extra library is needed. ## Why this reminded me of TypeDB Thinking through what I would have to describe in Lean felt familiar. I was asking questions I ask when modeling in TypeDB: what exists, how can those things relate, and which situations should the system refuse to accept? TypeDB is a typed database with a schema language, TypeQL. Entities and relationships have declared types, relationships have named roles, and constraints restrict how instances can connect. I have written a [longer explanation of its type system](/blog/typedb-type-system-explained); here I want to keep the same ownership example. Run this schema in a schema transaction and commit it in an empty TypeDB 3 database: ```typeql define attribute label, value string; entity customer, owns label @key, plays ownership:owner @card(0..); entity database, owns label @key, plays ownership:resource @card(1); relation ownership, relates owner @card(1), relates resource @card(1); ``` Read it as a description of allowed data. A customer can own multiple databases. Each ownership relationship connects exactly one customer and one database. Each database must participate in exactly one ownership relationship. That last sentence needs its own line in the schema: `plays ownership:resource @card(1)`. Declaring one owner per relationship alone would still allow two separate ownership relationships for the same database. The [`@card` documentation](https://typedb.com/docs/typeql-reference/annotations/card/) explains the difference between constraining a role's players and an entity's participation. In a write transaction, insert a customer, a database, and their relationship, then commit: ```typeql insert $customer isa customer, has label "customer-a"; $database isa database, has label "orders-demo"; ownership (owner: $customer, resource: $database); ``` That commits successfully. Now try this in a new write transaction: ```typeql match $database isa database, has label "orders-demo"; insert $other isa customer, has label "customer-b"; ownership (owner: $other, resource: $database); ``` The query runs, but committing the transaction fails: ```text [CNT5] Constraint '@card(1..1)' has been violated: found 2 instances. ``` Creating a database without an owner also fails at commit: ```typeql insert $database isa database, has label "orphan-demo"; ``` ```text [CNT5] Constraint '@card(1..1)' has been violated: found 0 instances. ``` **Verification:** these examples were run against a disposable local TypeDB 3.12.0 instance. Both invalid transactions failed at commit. This is important: a transaction can pass through an incomplete intermediate state while it constructs a valid final one. ## A valid relationship is not an authorized change The TypeDB schema still allows replacing customer-a's ownership relationship with customer-b's inside one transaction. The final state has exactly one owner. I checked that this commits too. Nothing in this schema identifies the person making the request or asks whether they may transfer the database. Application authorization is still required. A structurally valid record can describe an unauthorized action. Likewise, the Lean model preserves whatever owner it starts with. It does not establish that the initial owner was correct, that the customer exists, or that queries cannot leak another customer's data. Naming a theorem `tenant_isolation` would not give this small proof those additional guarantees. That is the connection I find useful, and also its limit: | Approach | What this example establishes | | --- | --- | | Software tests | Selected executions produce the expected ownership result | | TypeDB schema | Committed ownership data respects the declared structural constraints | | Lean proof | Every finite sequence of the modeled operations preserves the initial owner | These tools check different things. Their shared value for me is the work of stating the rule precisely enough to check it. ## Declarative code still needs the right declaration This is not exclusive to Lean or TypeDB. A SQL foreign key, a unique constraint, or a discriminated union in TypeScript can move a rule out of scattered conditionals and into something enforced consistently. Start there when that is enough. Declarative programming helps when it gives an important rule a clear home and an appropriate checker. Writing a declaration does not make the declaration correct. My TypeDB schema would be weaker without the participation constraint. My Lean theorem could be weakened to cover only owner 0, and the broken restart would satisfy it. That matters if an AI agent helps write proofs. I want assistance finding a proof of the intended statement, not permission to change the statement until something passes. Specifications and assumptions deserve review independently of the proof text. Lean also permits `sorry` placeholders for unfinished proofs. A successful build is not sufficient by itself: inspect the theorem being established and its [axiom dependencies](https://lean-lang.org/doc/reference/latest/Axioms/), including `sorryAx` and any unapproved assumptions. Checking a proof cannot establish that I asked the right question. ## Where this leaves testing and CI The largest gap in applying this to Layerbase is connecting a Lean model to the TypeScript implementation. A separately maintained model can be perfectly proved and still drift away from the code serving requests. Generated implementations, verified translations, or a carefully justified correspondence are substantial work. A handful of matching test cases does not prove that correspondence either. I would keep testing the integrations: database engines, filesystem operations, retries, and interrupted work. Property-based testing is also useful for exploring many inputs without writing each case by hand. It does not become redundant merely because a related Lean file exists. There may be places where a checked proof makes particular tests unnecessary, but that decision needs evidence about the exact property, implementation connection, and remaining failure modes. Proof development and checking also have costs. I do not yet have a measurement showing that this would make our CI cheaper or faster. For now, the useful change is smaller. I can isolate a deterministic decision, write down the rule it must preserve, and find out how much of my confidence comes from the code versus assumptions I never made explicit. If the TypeDB example interests you, [try modeling it in a managed TypeDB database](/create/typedb). The [Lean introduction](https://lean-lang.org/theorem_proving_in_lean4/Introduction/) is where I would start with the proof side. Neither requires treating the other as a replacement for tests. Both give me a reason to be more precise about what I expect the system to do.