Introducing LeanPort: Bring Proven Lean 4 Modules into Your Go Projects

Imagine you maintain a small Go service. One function decides whether a customer can withdraw money:

func canWithdraw(balance, amount, fee uint64) bool {
	return amount <= balance
}

Read the signature. It takes a fee. Read the body. It never uses the fee.

Call the function with balance 100, amount 30, and fee 2. It returns true. Call it with balance 100, amount 99, and fee 2. It also returns true. But 99 + 2 = 101, and 101 is more than 100. The customer cannot pay the fee. The function says yes.

You can fix the body:

return amount+fee <= balance

Now the function gives the right answer for these two calls. But how do you know it is correct for every balance, amount, and fee?

A test checks one input. A specification states the rule for all inputs. The specification here is simple: a withdrawal is allowed exactly when amount + fee <= balance.

This article is about a tool that can check that specification before you ship the Go program. The tool is LeanPort. It connects Lean 4, a programming language with a proof checker, to Go. You write the rule and the proof in Lean. LeanPort checks the proof, compiles the Lean code, and generates a Go package. Your Go program calls the package like any other Go package.

You do not need to know Lean to read this article. Basic Go is enough. We will define each Lean term when it appears. The article follows six small examples. Each example adds one layer. By the end, you will understand how a proof works, how LeanPort moves code from Lean to Go, and where the limits are.

Why a test is not a proof

A test gives one input and checks one output. A specification gives a rule for all allowed inputs. A proof shows that the code follows the specification.

For a single uint64 input, there are 2^64 possible values, or about 1.8e19. A uint64 is a 64-bit unsigned integer. A test suite with 10,000 cases covers about 5.4e-16 of those values:

10,000 / 2^64 = about 5.4e-16

The withdrawal rule has three uint64 inputs. The input space is (2^64)^3 = 2^192, or about 6.3e57 cases. You cannot test all of them.

This is not an argument against tests. Tests are the right tool for parsing, routing, database calls, and serialization. The problem starts when a test suite is the only evidence for a rule that must hold for every input.

Lean lets you write the rule as a theorem and prove it. The proof covers all inputs of the stated type. The proof is checked before the build.

Go still does the rest of the work. You prove the decision rule. You test the wiring around it. LeanPort connects the two.

What Lean is

Lean is a programming language and a proof assistant. A proof assistant is a tool that checks proofs. A theorem is a statement with a proof. You can run Lean code. You can also state a theorem and prove it.

Leonardo de Moura created Lean in 2013. He worked on automated reasoning at Microsoft Research and SRI. He also helped create Z3, a program that solves logical formulas. Engineers use Z3 to check software and hardware designs.

Lean has two parts: a language for code and a small checker for proofs. The checker is called the kernel. Lean uses the kernel to accept or reject a proof.

Here is a short timeline:

• July 2013: the first commit to the Lean repository.
• June 2014: Lean 0.1.
• January 2015: the first university course that uses Lean, at Carnegie Mellon University.
• January 2017: Lean 3.0.
• July 2017: Mathlib3 is created. Mathlib is a large library of mathematics for Lean.
• April 2018: Lean 4 development starts.
• July 2023: the Lean FRO starts. The Lean FRO is a non-profit group that supports Lean.
• September 2023: Lean 4.0.
• 2025: Lean receives the ACM SIGPLAN Programming Languages Software Award.

Lean 4 is written in Lean. It compiles to native code. This matters for LeanPort: the same language states the theorem and runs the code.

Amazon Web Services uses Lean for Cedar. Cedar is an open-source language for authorization rules. The AWS team wrote a Lean model of Cedar, Lean code that describes Cedar. They proved properties about the model. They also used random tests to compare the model with the Rust code that runs in production.

You do not need Mathlib to start. The examples use standard tactics such as simp, omega, cases, and rfl. All of them come with Lean. The first proof in the examples is a single simp tactic.

Your first Lean function

This is Example 1. A Lean function looks like this:

def increment (n : UInt64) : UInt64 :=
  n + 1

def starts a definition. increment is the function name. n is the input. UInt64 is a 64-bit unsigned integer. The body is n + 1.

You can run the function without Go. A small Main.lean file with #eval and an IO entry point prints:

42
increment 41 = 42

#eval evaluates an expression at compile time. IO is Lean's type for input and output.

The first line is compile-time evaluation. The second line is runtime execution. Both call the same function. There is no theorem, no tactic, and no Mathlib in this step.

This is ordinary code. Lean is not only a language for mathematics. It is a general-purpose programming language. You can write loops, data structures, and programs that print output.

The difference is that Lean can also state and check theorems about the code.

Calling Lean from Go

Now finish Example 1. Go cannot call Lean directly. Lean compiles to C. C is a low-level programming language. Go can call C through cgo. cgo is Go's tool for calling C code.

You could write the C bridge by hand. You would need to know Lean's C interface, set up the Lean runtime, compile the C code, and write cgo directives. That work is different for each operating system and CPU.

LeanPort does that work for you. The rule is simple: leanport build does the complex work. go build stays a normal Go build.

You add a small function at the boundary. The boundary is the place where Go values become Lean values and Lean values become Go values.

import LeanPort.Basics.Policy

namespace LeanPort.Basics

@[export leanport_basics_increment]
def incrementForC (n : UInt64) : UInt64 :=
  increment n

end LeanPort.Basics

The @[export ...] line gives the function a C name. The boundary does not implement the rule again. It changes the Lean function to a form that C can call.

import loads another Lean file. namespace groups names. end closes the group.

A small configuration file, leanport.toml, links the C name to a Go package and a Go name:

[[binding]]
  package = "learn"
  module = "Basics"
  export = "leanport_basics_increment"
  go_name = "Increment"
  args = ["uint64"]
  result = "uint64"
  runtime = "auto"

Each field has one job:

• package: the Go package name.
• module: the Lean module name.
• export: the C name from @[export].
• go_name: the Go function name.
• args: the input types.
• result: the output type.
• runtime: let LeanPort choose the smallest library.

You run two commands:

leanport check
leanport build

leanport check checks the Lean code and the export. leanport build compiles the Lean code, builds a library file, and writes the Go package. A library file contains compiled code that the Go program can use.

The generated Go function is normal Go:

func Increment(a0 uint64) uint64 {
	return uint64(C.lp_go_Increment(C.uint64_t(a0)))
}

Your application imports the package and calls it:

fmt.Println(learn.Increment(41))

42

The Go program keeps control. Lean is a library behind it. The boundary always returns a value. It does not panic.

If you stop here, the library has no Lean runtime. It is about 14 KB. The Lean runtime is the support code that Lean needs at run time. Later examples use Nat, Option, and Fin. That adds the Lean runtime. The library grows to about 30 MB.

LeanPort calls these two modes runtime-free and runtime-linked. Runtime-free means the library does not contain the Lean runtime. Runtime-linked means the library contains it. The linked mode is for text (String) and byte buffers (ByteArray).

The application needs Go, cgo, and a C compiler. It does not need Lean, Lake, elan, or Lean C header files. Lake is Lean's build tool. elan is the Lean version manager.

After you change Lean code or the binding, run leanport check && leanport build. Then run go build. LeanPort does not watch files. go build does not read the Lean code. It only compiles the generated package.

Functions that compute

Example 2 adds recursion, pattern matching, and higher-order functions:

def sumTo : Nat → Nat
  | 0 => 0
  | n + 1 => (n + 1) + sumTo n

def twice (f : Nat → Nat) (n : Nat) : Nat :=
  f (f n)

def double (n : Nat) : Nat :=
  n + n

def quadruple (n : Nat) : Nat :=
  twice double n

def isEven : Nat → Bool
  | 0 => true
  | n + 1 => !isEven n

This example teaches four ideas:

• sumTo uses recursion. It calls itself on a smaller number.
• sumTo uses pattern matching. The two patterns are 0 and n + 1.
• twice takes a function as an input. A function that takes another function is called a higher-order function.
• isEven also uses recursion and pattern matching.

Bool is a type with two values: true and false.

Lean checks that each recursive call uses a smaller input. A function that does not terminate is rejected at compile time. This is one reason Lean is useful for code that must be reliable.

Go has fixed-width numbers. uint64 is a 64-bit unsigned integer. Nat is a natural number with no upper limit. The boundary converts uint64 to Nat, runs the function, and encodes the result for Go.

The Go calls look like this:

fmt.Println(learn.SumTo(4))
fmt.Println(learn.IsEven(7))
fmt.Println(learn.Quadruple(3))

10
false
12

Three functions share one Go package. The caller sees only SumTo, IsEven, and Quadruple. The implementation can use recursion and higher-order functions without changing the Go API.

There are no proofs in this step. This is still ordinary computation. The next step adds the specification.

Your first proof

Example 3 adds a specification and a proof. A specification is a statement of what the code must do. A theorem is a statement with a proof. A proof shows that the statement is true for all allowed inputs.

A type is a set of values. Bool has two values: true and false. Nat has 0, 1, 2, and so on. Lean also uses types for statements.

Lean uses an idea called the Curry-Howard correspondence. The idea is simple:

a statement P        is a type P
a proof of P         is a value p : P
to check the proof   check that p has type P

This is why a proof can be a function. A statement like

forall n : UInt64, safeDivide n 0 = none

means "for every n, safeDivide n 0 is none." In Lean, a proof of this statement takes any n and returns a proof for that n.

A test uses one n at a time. The proof works for all n.

Implication works the same way. P -> Q means "if P, then Q." A proof of P -> Q is a function. It takes a proof of P and returns a proof of Q.

The basic forms are:

P -> Q          a proof takes a proof of P and returns a proof of Q
forall x, P x   a proof takes x and returns a proof of P x
P /\ Q          a pair of proofs
True            a type with one value
False           a type with no values

Lean uses helper programs called tactics to build proofs. simp simplifies a goal. omega solves arithmetic goals. A goal is the statement that Lean still must prove. The kernel checks the final proof. The kernel is the small part you must trust. A tactic can fail. The kernel still checks the result.

LeanPort rejects sorry and admit. These words leave a proof incomplete.

Now look at the example. The function safeDivide returns Option UInt64:

def safeDivide (n d : UInt64) : Option UInt64 :=
  if d = 0 then none else some (n / d)

def divideOrZero (n d : UInt64) : UInt64 :=
  (safeDivide n d).getD 0

Option has two cases: none and some value. none means there is no result. some 4 means the result is 4.

Option does not use 0 to mean failure. divideOrZero chooses 0 for the Go API when the result is none.

The core specification is two theorems:

theorem safeDivide_zero (n : UInt64) :
    safeDivide n 0 = none := by
  simp [safeDivide]

theorem safeDivide_nonzero (n d : UInt64) (h : d ≠ 0) :
    safeDivide n d = some (n / d) := by
  simp [safeDivide, h]

The first theorem says: for all n, safeDivide n 0 is none. The second theorem says: for all n and d, if d != 0, then safeDivide n d = some (n / d). If d = 0, the second theorem does not apply.

simp replaces the function call with its body and closes the goal. Lean checks the proof. If the statement is false, Lean rejects the proof.

LeanPort rejects an incomplete proof:

leanport: unproved holes found (remove sorry/admit):
  /home/you/project/lean/LeanPort/Division/Proofs.lean:...: sorry

The boundary is also part of the specification. Version 0.1.1 does not pass Option to Go. The example uses divideOrZero and proves the conversion. The theorem divideOrZero_nonzero says that a valid input returns the quotient.

Not proved: that 0 is the right error value. That is an API choice. If the caller must know about failure, add a second function or wait for Option support.

This is the turning point. Before this step, the code only computed. Now the code has a stated contract. A contract is a statement of what the code must do.

A rule about money

Example 4 returns to the withdrawal rule from the start. In Lean, the rule looks like this:

def withdraw (balance amount fee : Nat) : Option Nat :=
  if amount + fee ≤ balance then
    some (balance - (amount + fee))
  else
    none

The inputs use Nat, a natural number with no upper limit. amount + fee cannot wrap around. The boundary converts uint64 to Nat before the call.

The fee is part of the check. A withdrawal that cannot pay the fee is rejected. Failure is none. If the withdrawal fails, balanceAfter returns the old balance.

The main theorem is:

theorem withdraw_charges_fee (balance amount fee remaining : Nat)
    (h : withdraw balance amount fee = some remaining) :
    remaining + amount + fee = balance := by
  unfold withdraw at h
  split at h
  · injection h with h'
    omega
  · contradiction

The theorem says: if the result is some remaining, then remaining + amount + fee = balance. This proves two things. The bank does not create money. The fee is accounted for in the new balance.

The proof is short. unfold replaces withdraw with its body. split splits the if into two cases. In the success case, injection extracts the equality inside some, and omega solves the arithmetic. In the failure case, contradiction closes the goal.

Do not worry if you cannot write this proof yet. The important part is the statement and what it says.

omega is a tactic for arithmetic with +, -, and comparisons.

A second theorem, withdraw_never_exceeds_balance, says that a successful withdrawal never makes the balance larger.

From Go, the result is:

fmt.Printf("allowed(100, 30, 2) = %v\n", learn.Allowed(100, 30, 2))
fmt.Printf("balanceAfter(100, 30, 2) = %d\n", learn.BalanceAfter(100, 30, 2))
fmt.Printf("allowed(100, 99, 2) = %v\n", learn.Allowed(100, 99, 2))
fmt.Printf("balanceAfter(100, 99, 2) = %d\n", learn.BalanceAfter(100, 99, 2))

allowed(100, 30, 2) = true
balanceAfter(100, 30, 2) = 68
allowed(100, 99, 2) = false
balanceAfter(100, 99, 2) = 100

The second withdrawal is rejected because 99 + 2 = 101, and 101 is more than 100. Even though 99 is less than 100, the fee does not fit. The balance stays 100.

The Go API has two functions: Allowed and BalanceAfter. Use Allowed first. BalanceAfter alone cannot tell you if the withdrawal failed. A rejected withdrawal returns the old balance.

Not proved: that the balance is the customer's real balance. Not proved: that the database applies the new balance atomically. Those are application concerns.

This is the rule from the start of the article. The Go test could check two cases. The theorem covers every Nat input. That is the difference between a test and a proof.

Types that prevent mistakes

Example 5 changes the question. Instead of "did we test enough inputs?", it asks "can a caller make an invalid input?"

The core division function takes a proof that d != 0:

def divideBy (n d : Nat) (_h : d ≠ 0) : Nat :=
  n / d

The function body has no zero check. A caller cannot call divideBy with d = 0, because the caller cannot provide the proof.

checkedDivide is the adapter for raw input:

def checkedDivide (n d : Nat) : Nat :=
  if h : d = 0 then 0 else divideBy n d h

The same idea works on the result side. Fin n is a number less than n:

Fin n = { i : Nat // i < n }

percent returns Fin 101. It cannot return 150.

def percent (n : Nat) : Fin 101 :=
  ⟨min n 100, by omega⟩

percent limits the input with min n 100. omega proves that the result is less than 101. The theorem percent_bounded states that the result is at most 100. percent_of_le says that an input in range does not change. percent_of_gt says that an input above the range becomes 100.

Fin is also useful for an index. slot uses Fin 3:

def slot (a b c : Nat) (i : Fin 3) : Nat :=
  match i with
  | ⟨0, _⟩ => a
  | ⟨1, _⟩ => b
  | _ => c

Fin 3 is 0, 1, or 2. The value 3 is not valid. The term ⟨3, by decide⟩ does not type-check. An invalid slot cannot exist inside Lean.

The boundary checks the input and builds the proof. UInt8 is an 8-bit unsigned integer:

@[export leanport_refined_slot]
def slotForC (a b c : UInt64) (code : UInt8) : UInt64 :=
  if h : code.toNat < 3 then
    (slot a.toNat b.toNat c.toNat ⟨code.toNat, h⟩).toUInt64
  else
    a

A code of 99 is not valid. The boundary returns the first slot. The core function never sees an invalid index.

The pattern is: use strong types in the core. Check the input one time, at the boundary.

The two division functions have different jobs:

divideBy is the safer core function. checkedDivide is the adapter for input from Go. The theorem checkedDivide_nonzero connects the two functions. With a nonzero divisor, checkedDivide returns the same result as divideBy.

Limit: the type proves that percent returns a value at most 100. It does not prove that a limit of 100 is the right product rule. Types enforce the rule you state, not the rule you forgot to state.

A complete authorization tool

Example 6 is a command-line tool called permctl. It answers authorization questions. Authorization means "may this caller do this action?"

The policy, the set of authorization rules, has four access levels and five actions. An access level is a number that shows the caller's access.

inductive Action where
  | create
  | read
  | update
  | delete
  | viewAudit

def effectiveLevel (authenticated isAdmin ownsResource : Bool) : UInt8 :=
  if !authenticated then 0
  else if isAdmin then 3
  else if ownsResource then 2
  else 1

def allows (level : UInt8) : Action → Bool
  | .create => level == 1 || level == 3
  | .read => level == 2 || level == 3
  | .update => level == 2 || level == 3
  | .delete => level == 2 || level == 3
  | .viewAudit => level == 3

An action code is a number that names an action. viewAudit means read the audit log, a record of actions.

The level comes from three facts: authenticated, isAdmin, and ownsResource. It does not come from a text value supplied by the caller. The owner level means the caller owns this resource. It is not an account-wide role.

The boundary decodes action codes 0 through 4. For any other code, it returns 0, which means deny.

The decision table is:

The proofs are ten theorems. Here are two. cases splits a value into its possible cases. rfl proves a goal by computation.

theorem unauthenticated_cannot_become_admin (ownsResource : Bool) (action : Action) :
    authorize false true ownsResource action = false := by
  cases ownsResource <;> cases action <;> rfl

theorem audit_requires_admin (a adm own : Bool) :
    authorize a adm own .viewAudit = (a && adm) := by
  cases a <;> cases adm <;> cases own <;> rfl

The first theorem checks both values of ownsResource and all five actions. The second theorem checks all eight combinations of three true/false values. rfl closes each case by computation.

The Go side runs thirty-nine checks:

• 20 matrix cells.
• 15 ownership and flag cases.
• 4 invalid action codes.

The invalid codes return deny.

verified 39 checks
LEVEL            create     read       update     delete     viewAudit
unauthenticated  deny       deny       deny       deny       deny
member           allow      deny       deny       deny       deny
owner            deny       allow      allow      allow      deny
admin            allow      allow      allow      allow      allow

The library is 28,066 bytes. The Go program is 2,351,184 bytes. The program does not load a separate Lean library at run time.

Lean proves the policy. Go tests the wiring. Not proved: that the program checks who the caller is. Not proved: that the resource owner comes from trustworthy data. Not proved: that the database update is atomic. Not proved: that the deployment is correct.

Costs and limits

The measurements in this article are from Lean 4.29.1, Go 1.24.3, and linux/amd64.

The runtime-linked library is about 1,070 times larger than the runtime-free library. The demo program is about 6.1 times larger.

Here is a cost estimate. A container image is a package that contains the program and its files. A system downloads 1,000 container images per day. Each image contains a Go program that is 12.1 MB larger. The extra download is about 12.1 GB per day. At 10,000 images per day, the extra download is about 121 GB per day. This estimate does not include image caching.

AWS published numbers for Cedar. The Lean model has 1,673 lines. The proofs have 5,714 lines. The production Rust code has 24,915 lines. The most complex proof took 18 days of work by one person. Checking all proofs and compiling the models took 185 seconds. The Lean model processed a random test input in about 5 microseconds, or 5 millionths of a second. The Rust code processed the same kind of input in about 7 microseconds.

These numbers come from one team and one codebase. They show two things. The proof work is paid before release. The runtime can be fast.

For permctl, the Lean code is 94 lines: 31 lines of policy, 40 lines of proof, and 23 lines of boundary. The project has ten theorems and thirty-nine Go checks.

Use proofs for rules that change slowly and have high risk. A stable authorization table is a good candidate. CRUD handlers that change every sprint are not.

The limits are:

• cgo and a C compiler are required. A pure Go build with cgo turned off (CGO_ENABLED=0) does not work.
• Version 0.1.1 builds only the host target. Building for another operating system or CPU needs a target C compiler.
• The generator supports numbers, true/false, strings, and byte arrays. The project checks the low-level conversion for records, arrays, Option, and Except, but the generator does not write them yet. Except is Lean's type for a value or an error. The proof example converts Option to a number.
• Runtime-linked calls do not add a lock. If more than one goroutine calls a runtime-linked binding, add a lock.
• Version 0.1.1 supports only one runtime-linked package per program. Keep String and ByteArray exports in one package.
• The Lean C interface can change. LeanPort pins the Lean version and writes it to MANIFEST.json, a file that records the version and file hashes. A version change changes the library hash, a fingerprint of the file.
• leanport check checks the proof of the rule. It does not prove the full application. Authentication, resource lookup, database consistency, and deployment stay outside the proof.

Try it yourself

If you want to try it, install LeanPort:

go install github.com/shrsv/LeanPort/cmd/leanport@v0.1.1

You need Go 1.24+, a C compiler, and Lean 4 through elan. Then run the last example:

git clone https://github.com/shrsv/LeanPort
cd LeanPort/tutorial/permctl
leanport check
leanport build
go test ./...
go build -o permctl ./cmd/permctl
./permctl verify
./permctl matrix

If you want the full learning sequence, start with the first function and work forward. The six examples are:

1. Run Lean and call it from Go.
2. Add functions and recursion.
3. Write a specification and a proof.
4. Prove a fee and balance rule.
5. Use types to block invalid input.
6. Build a verified authorization tool.

Each example ends with a normal Go call.

The code for all six examples is in the LeanPort tutorial.

Conclusion

You have now seen the full path. A Lean function runs on its own. A Go program calls it through a generated package. Recursion and pattern matching handle computation. A theorem states a rule for all inputs. A proof checks the rule. A money rule proves that the fee is accounted for. A type blocks invalid input. A complete tool combines the ideas.

The proofs cover the rules. The tests cover the wiring. The Go program stays a normal Go program.

Which function in your Go service would you prove? What would the theorem say? Tell me in the comments.

References

• History of Lean from the Lean FRO.
• Leonardo de Moura on Lean, Z3, and automated reasoning.
• Lean FAQ on Lean as a programming language, proof values, and the kernel.
• Lean language reference for the language, runtime, and C interface.
• Cedar verification at AWS on the Lean model and the proof effort.
• LeanPort repository for the examples, generated code, and measured sizes.