LeanPort 將 Lean 4 驗證模組整合至 Go

Hello, I'm Shrijith Venkatramana, and I'm building LiveReview — a blast-radius aware AI code review built for your business-critical systems. Star us to help devs discover the project, give it a try, and share your feedback to help improve the product.

A permission check can fit in five lines and still be one of the most consequential functions in a service.

Can a resource owner read the audit log? Does an admin flag count before authentication? What should happen when a caller passes action code 255? These are small rules, but a mistake can expose data or block a legitimate operation.

Tests answer these questions for the inputs we try. Formal verification lets us state a rule precisely and prove properties about every input in its modeled domain.

LeanPort is a small tool with a specific aim: write decision logic and proofs in Lean 4, then consume the result from Go as an ordinary package. The rest of your application can stay Go.

The rule is small; the consequences aren't

Formal verification has a long history, but it has often carried a large integration cost. In 2009, Gerwin Klein and colleagues published work on seL4, a microkernel whose implementation was checked against a formal specification. Their paper is valuable for another reason: it lists what the proof assumes, including the correctness of the compiler, assembly, boot code, cache management, and hardware.

That is the useful lesson for application developers. Verification is not a magic label applied to an entire system. It is a precise claim about a modeled part of a system, under stated assumptions.

LeanPort applies the idea to a much smaller unit: a function that decides whether an operation is allowed, whether a quota transition is valid, or whether a protocol state change preserves an invariant. Such functions are often pure, full of boundary cases, and important enough that a mistaken rule has a disproportionate cost.

The workflow: proofs in Lean, a Go package out

Lean 4 is both a programming language and an interactive theorem prover. A definition can be executable code; a theorem states a proposition about that code; and Lean checks the proof term. LeanPort packages that workflow so application developers do not need to manage the foreign-function interface by hand.

The pipeline is deliberately split into a maintainer path and a consumer path:

• A maintainer edits the Lean policy, proofs, and C-facing boundary. leanport check runs Lean's checker and rejects unproved sorry or admit holes.
• leanport build compiles Lean to C, builds a static archive, and generates the C/cgo bridge plus an idiomatic Go API.
• The generated package and archive are committed to the repository. The application imports the Go package like any other internal dependency.
• A downstream build needs Go, cgo, and a C toolchain. It does not need Lean, Lake, elan, or the LeanPort CLI.

The project principle is simple: leanport build may be complicated; go build should stay boring. The generated files are an output, not a second implementation to edit by hand.

Start with a policy you can inspect

The repository's permctl tutorial builds a command-line tool around an authorization policy with four effective access levels and five actions:

Ownership is a fact about the resource being accessed, not a global role. The Lean function therefore receives facts such as authenticated, isAdmin, and ownsResource, plus the requested action. It does not trust a client-supplied role string.

One of the tutorial's theorems says that audit access is exactly equivalent to being authenticated and an administrator:

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

Read that in plain English: for every combination of the three Boolean inputs, viewAudit is allowed precisely when a and adm are both true. The own flag cannot grant audit access. Lean checks this theorem against the authorize definition; if the implementation changes so the claim no longer follows, the proof stops checking.

The generated Go call stays straightforward:

import "example.com/permctl/internal/verified/authz"

allowed := authz.Authorize(authenticated, isAdmin, ownsResource, authz.Update)

In the checked-in tutorial, the Lean policy has ten machine-checked theorems, and the Go command's conformance check reports 39 runtime checks. The theorem and the tests do different jobs: one reasons about a stated property of the definition; the other exercises the generated binding and application behavior.

What proof adds over tests

For this policy, three Boolean inputs and five valid actions produce 2^3 * 5 = 40 flag/action combinations. That is small enough to test exhaustively, and the tutorial does test many of the important cases. In a real system, however, inputs often include combinations of resource attributes, account states, quota counters, timestamps, retries, and workflow transitions. The state space grows quickly, and regression tests tend to concentrate on cases someone thought to write down.

A theorem can quantify over every value in its domain. For example:

• an unauthenticated caller is denied every action;
• an owner cannot read the audit log;
• an unauthenticated caller cannot become an admin by setting flags;
• a quota update preserves a stated upper bound.

This is not a claim that formal proofs replace testing. Tests still matter for parsing, I/O, the command-line interface, database integration, and other behavior outside the theorem. The distinction is scope: tests run examples; proofs establish the proposition you wrote, for the inputs and assumptions the model covers.

LeanPort also has an explicit failure path. Add an unproved sorry to the tutorial's proof file and leanport check exits non-zero. That makes the proof obligation usable in CI rather than merely a note in a design document.

The boundary is part of the design

A verified function is useful only if the production program calls it correctly. LeanPort keeps the boundary narrow: Lean owns the policy and proofs; LeanPort generates a C adapter and a cgo wrapper; Go calls the generated API. LeanPort does not translate Lean source into Go source.

The adapter is total and fails closed. The tutorial encodes action values as small integers; an unknown action code returns the deny result rather than panicking or accidentally authorizing a request. That is a small example of treating malformed boundary inputs as part of the specification.

The native artifact size depends on the types that cross the boundary. In the Linux/amd64 example, a scalar-only, runtime-free archive is about 27 KB, and the tutorial binary is about 2.3 MB. An example using String or ByteArray links Lean's runtime into the archive, which is about 29 MB in the current example. Think of these as measured examples, not a benchmark: the principal difference is whether the Lean runtime is needed.

There are practical constraints in the current v0.1.1 release:

• The generator supports scalars, strings, and byte arrays. Records, arrays, Option, and Except have ABI mappings validated but do not yet have code generation.
• cgo and a compatible C compiler are required, so a pure-Go build with CGO_ENABLED=0 cannot link the generated package.
• Lean's C ABI is unstable. LeanPort records the toolchain version and generated artifact digests; after changing Lean code, bindings, or toolchain versions, rerun leanport check and leanport build and commit the generated output.
• The proof covers the modeled decision logic, not the entire application. Authentication data, route-to-action mapping, database consistency, and deployment need their own controls unless they are explicitly brought into the model.

This boundary discipline echoes the seL4 story: a strong proof becomes more useful when its assumptions are visible. A formal theorem about the wrong specification is still the wrong business rule.

The economics and operations

Formalization has an upfront cost. It is most promising when a rule changes repeatedly, when its failures are expensive, and when its behavior can be stated clearly enough to prove.

A rough first-year break-even model, measured in engineering hours, is:

V * (p_before - p_after) * C > F + V * M

where:

• V is the number of changes to the rule per year;
• p_before is the probability of a target logic defect escaping the current process per change;
• p_after is the residual probability after formalization, including specification mistakes and gaps outside the model;
• C is the average cost of such a defect in engineering hours;
• F is the one-time cost of writing the specification and proofs;
• M is the additional proof-maintenance effort per change.

Consider illustrative numbers, not LeanPort measurements: 24 changes per year, a reduction in the target defect probability from 5% to 1%, and an average incident cost of 40 engineering hours. The expected avoided cost is 24 * (0.05 - 0.01) * 40 = 38.4 hours. If the initial formalization costs 20 hours and each change adds half an hour of proof maintenance, first-year effort is 20 + 24 * 0.5 = 32 hours. Under those assumptions, formalization clears the first-year break-even point.

The probabilities are placeholders, not universal empirical rates. The model also excludes the value of stronger assurance in high-consequence systems, and it cannot account for errors in an incomplete or mistaken specification. Use data from your own incidents and change history where possible.

Operationally, LeanPort separates the slower verification/build step from ordinary Go development. Maintainers run leanport check && leanport build after changing the Lean code or binding configuration, and commit the regenerated package. Consumer CI can run normal Go tests and builds against that committed artifact. The project pins the Lean toolchain and includes diagnostics to make mismatches visible; Nix support can also help pin the Go and C toolchains.

Try it: pick one rule worth proving

Start with the LeanPort repository and its end-to-end permctl tutorial. With LeanPort installed, try the full loop from the tutorial:

leanport check
leanport build
go test ./...
go build -o permctl ./cmd/permctl
./permctl verify

The best first candidate is rarely an entire application. Choose one compact rule with high consequence: authorization, pricing, quota enforcement, a state transition, or a protocol invariant. Make the intended behavior explicit, prove the property you care about, and keep the rest of the application in its existing language and architecture.

Which rule in your Go service would you formalize first: authorization, billing, quotas, or a state machine?

References

• LeanPort: verified Lean 4 modules for Go
• Lean 4 as a theorem prover and programming language — Leonardo de Moura and Sebastian Ullrich, CADE 2021.
• The seL4 microkernel and machine-checked formal verification — Gerwin Klein et al., SOSP 2009.

Your team's attention is limited, and the deluge of AI-generated code is making it harder to keep production reliable and secure without slowing you down.

I'm building LiveReview, a blast-radius aware AI code review built for your business-critical systems.

Instead of presenting every diff with equal emphasis, LiveReview scores each change by blast radius — how far its impact reaches through your call graph — so you can focus attention where it actually matters.

Spend code review effort where business risk is highest — not spread evenly across every diff.

LiveReview is built for engineering teams that ship often, but also care about keeping production stable for customers. It approves some 40-50% of low-risk changes automatically, and it gives your team the tools to handle the rest:

• Understand risky changes faster.
• Fix problems in those changes, with human attention directed to the work that needs it.
• Enforce your engineering standards.
• Learn from production outcomes, such as incidents, rollbacks, and queue wait times.
• Improve the review process over time and make it more efficient.
• Connect to the major engineering tools that your team already uses.

Auto-Approve: Ship the Safe 50% Without a Human

Auto-Approve Upto 50% of Your Pull Requests, Safely. Risk scoring decides which MRs/PRs are safe enough to ship without a human, so your team only spends review time on risky and critical changes.

demo.mp4

LiveReview auto-approving a low-risk change while…

Click below to try LiveReview with your codebase: