Lean on the JVM: proved functions for Java and Clojure

Imagine a pricing service written in Java. Customers request a discount, and the business has two firm rules: a discount may never exceed the order subtotal, and it may never exceed the policy cap. Unit tests check a few dozen combinations of amounts, but the rules speak about every order. Sooner or later, a refactoring or a new promotion meets an input nobody tested.

Lean, a programming language and proof assistant, lets you state such a rule as a theorem and have the computer check a proof that it holds for every input. But adopting it usually means leaving the JVM. Lean compiles to native code, and connecting that code to a Java service is a project of its own.

The Ansatz Lean/JVM SDK removes that step. You write the function and its proofs in Lean, prepare the compiled code during your build, and call it from Java or Clojure like any other library. The deployed service needs no Lean installation. We are introducing this workflow with release 0.2.615, and this post follows the pricing rule from proof to production, then shows how Lean code can call back into the application.

Write the rule down, then prove it

First, the rule itself. Amounts are whole numbers in the currency’s smallest unit, such as cents. Save this as Pricing.lean:

namespace Pricing

def discount (subtotal requested cap : Nat) : Nat :=
  min subtotal (min requested cap)

theorem discount_le_subtotal (subtotal requested cap : Nat) :
    discount subtotal requested cap ≤ subtotal :=
  Nat.min_le_left _ _

theorem discount_le_cap (subtotal requested cap : Nat) :
    discount subtotal requested cap ≤ cap :=
  Nat.le_trans (Nat.min_le_right _ _) (Nat.min_le_right _ _)

theorem discount_eq_requested {subtotal requested cap : Nat}
    (h₁ : requested ≤ subtotal) (h₂ : requested ≤ cap) :
    discount subtotal requested cap = requested := by
  simp only [discount, Nat.min_eq_left h₂, Nat.min_eq_right h₁]

end Pricing

The definition takes one line: the discount is the smallest of the subtotal, the requested amount and the cap. The theorems are the interesting part. The first says that the discount never exceeds the subtotal, and the second that it never exceeds the cap. But a function that always returns zero would satisfy both bounds, so the third theorem adds that a request within both limits is granted unchanged. Lean checks all three for every possible input when it builds the file.

Of course, a proof is only as good as its statement. Lean guarantees that this definition has these properties; whether they are the right properties remains a business question. The guarantee also covers the Lean code only. The compiler, the JVM runtime and the integration that carry the result into Java are trusted rather than proved. Proofs are erased from the compiled code, so the service never runs a theorem prover on a request.

The example is small on purpose. A team can start with one rule like this, keep its database, HTTP handlers and deployment in Java or Clojure, and move more logic into Lean only where proofs pay off.

Prepare the code once, during the build

Next, add the SDK to an existing Maven project:

<repositories>
  <repository>
    <id>clojars</id>
    <url>https://repo.clojars.org/</url>
  </repository>
</repositories>
<dependencies>
  <dependency>
    <groupId>org.replikativ</groupId>
    <artifactId>ansatz-lean-jvm</artifactId>
    <version>0.2.615</version>
  </dependency>
</dependencies>

It runs on JDK 17 or later and brings Clojure and a JSON library along as ordinary Maven dependencies. It does not need the core Ansatz kernel or a Mathlib store. For the commands below, write the resolved classpath to a file:

mvn dependency:build-classpath -Dmdep.outputFile=target/lean-classpath
export SDK_CLASSPATH="$(cat target/lean-classpath)"

Preparation is the only step that needs native tools. It uses the official Lean 4.33.1 toolchain and a published bundle of helper programs that export what the JVM needs. For now, it runs on Linux x86-64 with prlimit available. Set LEAN_SYSROOT, PRODUCER_BUNDLE and COMPILER_CACHE to the toolchain, the extracted bundle and a cache directory. Then place Pricing.lean in a directory named pricing and prepare the function:

java -cp "$SDK_CLASSPATH" ansatz.lean.jvm.LeanPreparation \
  --source ./pricing \
  --sysroot "$LEAN_SYSROOT" \
  --producer-bundle "$PRODUCER_BUNDLE" \
  --cache "$COMPILER_CACHE" \
  --root-module Pricing \
  --entry Pricing.discount \
  --output ./pricing.leanjvm

The result is a single file, pricing.leanjvm. It contains Lean’s compiled intermediate code, together with the function types, data layouts and initialisation steps that the JVM needs. The command also prints two fingerprints, which are SHA-256 hashes. Keep the manifest hash in your application’s configuration. When the service loads the artifact, it checks the file against that fingerprint, so a changed or swapped file is rejected. One caveat applies to proprietary code: the artifact also contains the Lean source files and compiled modules, so treat it like the source itself. The preparation guide covers the details.

Call it like any other Java method

Then, in the deployed application, load the artifact and ask for the function by name. Save this as PricingApp.java:

import ansatz.lean.jvm.*;
import java.math.BigInteger;
import java.nio.file.Files;
import java.nio.file.Path;

public class PricingApp {
    public static void main(String[] args) throws Exception {
        try (Lean runtime = Lean.open();
             var input = Files.newInputStream(Path.of(args[0]));
             LeanProject project = runtime.loadArtifact(input, args[1])) {
            LeanFunction discount = project.function("Pricing.discount");
            BigInteger amount = (BigInteger) discount.invoke(10_000, 1_500, 1_000);
            System.out.println(amount);
        }
    }
}

java --class-path "$SDK_CLASSPATH" PricingApp.java \
  pricing.leanjvm "$EXPECTED_MANIFEST_SHA256"

It prints 1000, because the requested 1,500 is capped at 1,000. Behind the call, the SDK checks the arguments against the Lean signature and converts the result into a BigInteger. The same works for booleans, strings, lists, arrays, pairs, optional values and success-or-error results, and Lean records and recursive datatypes arrive as immutable Java objects.

Clojure developers resolve the same release:

{:deps {org.replikativ/ansatz-lean-jvm {:mvn/version "0.2.615"}}}

{:deps {org.replikativ/ansatz-lean-jvm {:mvn/version "0.2.615"}}}

and can call the function from the REPL:

require('[ansatz.lean.jvm :as lean], '[clojure.java.io :as io])

with-open [runtime lean/open(),
           input io/input-stream("pricing.leanjvm"),
           project lean/load-artifact(runtime,
                     input,
                     System/getenv("EXPECTED_MANIFEST_SHA256"))]:
  discount := lean/function(project, "Pricing.discount")
  [discount(10000, 1500, 1000) discount(200, 1500, 1000)]
end
;; => [1000 200]

(require '[ansatz.lean.jvm :as lean]
         '[clojure.java.io :as io])

(with-open [runtime (lean/open)
            input (io/input-stream "pricing.leanjvm")
            project (lean/load-artifact runtime input
                      (System/getenv "EXPECTED_MANIFEST_SHA256"))]
  (let [discount (lean/function project "Pricing.discount")]
    [(discount 10000 1500 1000)
     (discount 200 1500 1000)]))
;; => [1000 200]

The Superficie tab shows the same Clojure forms in another notation. Both run on the same runtime.

Let Lean call the application

So far, information has flowed in one direction, from Java into Lean. Real business logic, however, also needs the application: a configuration value, a database lookup or an exchange rate. This is where running Lean inside the JVM pays off most. If you compile Lean natively instead, you load a platform-specific library through JNI or Panama, start Lean’s runtime and convert every value by hand, as the lean-android-compose demonstration does for an Android app. Calling back into Java then needs C glue code as well. The harder part is memory. Lean frees its objects by reference counting, while the JVM uses a garbage collector, and neither sees the other’s references. A Java object that holds a Lean value must release it when the collector reclaims the Java object, a Lean value that holds a Java object must keep a JNI reference until Lean frees it, and a cycle across the boundary is reclaimed by neither side. With the SDK, both directions use ordinary Java and Clojure values, and the garbage collector manages all of them.

Suppose the cap depends on the customer’s segment and lives in the application’s configuration. Add a declaration without a body to Pricing.lean, together with a function that uses it:

namespace Pricing

@[extern "ansatz_jvm_policy_cap"] opaque policyCap : String → IO Nat

def quote (subtotal requested : Nat) (segment : String) : IO Nat := do
  pure (discount subtotal requested (← policyCap segment))

end Pricing

Prepare it with --entry Pricing.quote --entry Pricing.policyCap. When the application loads the artifact, it supplies the implementation under the declaration’s name:

HostBindings bindings = HostBindings.builder()
    .io("Pricing.policyCap", "config/1", arguments -> {
        Long cap = caps.get((String) arguments.get(0));
        if (cap == null) throw LeanIOError.userError("Unknown segment");
        return BigInteger.valueOf(cap);
    })
    .build();
LeanProject project = runtime.loadArtifact(input, expectedManifestSHA256, bindings);
IOResult<?> result = (IOResult<?>) project.call("Pricing.quote", 10_000, 1_500, "retail");

With caps of 1,000 for retail and 2,500 for partner, the two quotes are 1000 and 1500. An unknown segment reaches Lean as an ordinary IO error and comes back to Java as a LeanException with its message. In Clojure, the binding is a map entry, {"Pricing.policyCap" {:implementation-id "config/1" :effect :io :fn (fn [segment] (get caps segment))}}, passed to lean/load-artifact.

Notice what happens to the proof. discount_le_cap holds for every cap, so it also covers whatever value the configuration returns, and the quote can never exceed the configured cap. A trust boundary appears only when host code replaces a Lean definition, because type checking a binding does not prove that it behaves like the code it replaces. For now, bindings are first-order and synchronous, so they cannot take functions as arguments or run asynchronously. The host-binding guide covers pure bindings, replacements with a Lean fallback and custom result types.

Run it in a service

In production, a few more questions come up. The first is lifetime. Open the Project, as the SDK calls a loaded artifact, once and reuse its function handles. Calls share its code and initialised globals and run one at a time, so use several Projects for parallel work. A new version of the code means loading a new Project; state migration and public execution forks are separate work.

The second is runaway computation. Each call runs under a budget, by default two million interpreter instructions and five seconds. When a workload needs more, raise the budget per call with InvocationOptions.empty().withBudget(instructions, duration) and invokeWith.

The third is failure. Invalid arguments are rejected before anything runs, and an IO function that returns an error reports it as a LeanException. In both cases, the Project stays usable. But when a call fails halfway, for example because it exhausted its budget, the SDK cannot know what state the Lean code left behind. It therefore refuses further calls with ProjectFailed until you call project.restart(). The restart builds a fresh engine from the same verified artifact and keeps your function handles. Module initialisers run again, so globals start over.

Finally, panics behave as in native Lean. panic! and an out-of-bounds xs[i]! print a message to stderr and continue with a default value. If you prefer a hard stop, an option turns a reached panic into a failure instead. The SDK guide covers all four questions.

Bring an existing Lean project

Most teams will not start from a blank file, so we also tried real library code. The insertion-sort module from Functional Programming in Lean uses polymorphic arrays, typeclass comparison, proofs about array size and a termination argument. We load the unchanged module as a dependency of a small Lake project and add one function for the JVM to call:

import Examples.ProgramsProofs.InstrumentedInsertionSort
namespace LakeTutorial

def sortAndOriginal (xs : Array Nat) : IO (Array Nat × Array Nat) :=
  pure (insertionSort xs, xs)

end LakeTutorial

The caller’s Lake configuration requires the pinned fp-lean examples package, which Lake builds first. The SDK’s builtLakeWorkspace() option, or the CLI flag --source-mode built-lake, then takes the built workspace as it is, without fetching or building anything itself. A Java call with List.of(3, 1, 2) returns [[1, 2, 3], [3, 1, 2]] as BigInteger values, and Clojure receives the same pair of vectors. Keeping the original array next to the sorted one also exercises the runtime’s copy-on-write behaviour. Because insertion sort is quadratic, a few hundred elements fit the default budget, while larger inputs need a raised one.

The module proves that sorting preserves the array’s size and terminates, although it does not prove that the result is sorted. It is the work of David Thrane Christiansen and the Functional Programming in Lean contributors. Our corpus pins the revision, and the attribution and CC BY 4.0 source licence document the original work. The Lake guide explains this path, and our native CI also runs selected argument-parsing functions from the unchanged lean4-cli library.

Why the interpreter can fork

Why interpret Lean at all, instead of only calling native code? The answer comes from our own product. Simmis is designed so that people and agents can try a change in a separate branch before anyone accepts it, and that branching should reach running computations as well as stored data. For Clojure, we have already extended SCI, a Clojure interpreter, so that a session can fork into independent histories. Simulations need the same ability. In our Stuttgart city model, a policy question is an intervention evaluated with the same random draws as the baseline, which is easiest when the what-if continues from the very same state.

We are not the first to run Lean’s compiled code on the JVM. Lean4J exports it as JSON and interprets it on GraalVM’s Truffle framework, which compiles hot code to machine code and lets Java, JavaScript and Python pass callbacks in. Its focus is speed and polyglot tooling such as debugging and profiling, it requires GraalVM, and its README states that it is not meant as a faithful drop-in for native Lean. Our SDK makes different trade-offs. It runs on any JDK 17, loads only artifacts that match a trusted fingerprint, takes its Java and Clojure types from Lean’s checked signatures, and refuses unsupported operations before a program starts. It also keeps the whole execution state forkable, which matters most for Simmis. Truffle-style compilation remains a promising route to speed, and we see it as a possible later backend rather than a competing design.

Because the SDK keeps Lean’s entire execution state as JVM objects, it can copy that state. Its engine can already fork a paused computation, at any point in its execution, into two engines that continue independently, and the engine tests check that control state, ownership and output stay separate. The public SDK does not expose forks yet, so this is groundwork rather than a feature of this release.

Internally, we also write most of our verified code in Clojure rather than in Lean’s own syntax. Core Ansatz implements Lean 4’s kernel in Java and offers the same type theory as Clojure forms, so definitions and theorems written in Clojure are checked against the same libraries, such as Mathlib. That lets us add types and proofs to existing Clojure code gradually, one function at a time, and call the results as ordinary Clojure. The SDK described here complements it for code that already exists in Lean. The two can run in the same application, although loading executable code with the SDK does not import its theorems into the Ansatz kernel.

What comes next

This release is a starting point, and two goals guide the next ones. The first is speed. Today the SDK interprets Lean’s compiled code, and the JVM’s just-in-time compiler optimises that interpreter. Our near-term aim is to be competitive with Lean’s own interpreter, lean --run. For workloads that need more, the direction is to compile and specialise Lean code for the JVM, aiming at compiled Lean performance for selected workloads. We have not yet published representative benchmarks. Startup is already cheaper: the SDK’s own Clojure layer ships precompiled, so a fresh JVM pays Clojure’s startup cost but does not compile the SDK.

The second goal is coverage of Lean’s language, standard libraries and runtime services. The current release supports common application types, custom datatypes, explicit IO services and Lean’s Nat, Int and unsigned fixed-width arithmetic. A program that needs an operation outside this profile is refused before it starts, not partway through. Public entry points use closed first-order signatures, and tasks, public forks and Mathlib-heavy projects remain outside this release. A prepared project may contain at most 128 modules besides Lean’s core library, Init. The compatibility ledger records the details.

Lean libraries written partly in C need more work still. Java’s Foreign Function and Memory API, available in JDK 22 and later, offers a route to native libraries. However, Lean’s object representation and ownership rules still need explicit bridges, and this release includes none.

The next useful compatibility target may be your application. Bring us the Lean project and the functions you want to run, together with the JVM environment and workload that matter to you. That tells us which language features, runtime operations and performance requirements to prioritise.