Glean#

Verify Gleam functions in Lean 4.

glean translates the functions you mark with a /// @proof doc comment into Lean 4 definitions (via hax), so you can prove properties about them.

Requires Nix with flakes. The engine is currently bundled.

Nix Setup#

Add glean to your project's flake.nix so glean is on your PATH:

# inputs:
glean.url = "git+https://tangled.org/edouard.paris/glean";

# in your devShell's packages:
glean.packages.${system}.default

The steps below assume you run them inside nix develop. To try glean once without adding it, replace glean with nix run git+https://tangled.org/edouard.paris/glean -- in any command.

1. Scaffold a proof project#

In your Gleam project, once:

glean init

This creates proofs/lean/ with a Lake project (lakefile.toml, lean-toolchain) wired to hax's Lean prelude. glean pins the prelude (hax's own proof-libs/legacy-lean) and the matching Lean toolchain for you, so there are no revisions to manage by hand.

2. Mark the functions to extract#

Add a /// @proof doc comment above any function:

/// @proof
pub fn fib(n: Int) -> Int {
  case n {
    0 -> 0
    1 -> 1
    _ -> fib(n - 1) + fib(n - 2)
  }
}

See examples/fibonacci for a complete project (including proofs over Result, Nil, and gleam/option).

3. Extract#

glean prove

With no argument, glean prove extracts every @proof-marked module under your project's src/. Under proofs/lean/Proofs/ it writes, per module:

fibonacci.lean: the generated Lean definitions. Do not edit; glean regenerates it each run. Gleam Int is modeled as Lean's arbitrary-precision Int (as gleam.Int), so proofs reason about true integers, not fixed-width ones. The file imports the shared model library (below); for the fib above it is:

import Hax
import Proofs.GleamModels
-- (Std.Do imports, opens, and set_options elided)

namespace fibonacci

@[spec]
def fib (n : gleam.Int) : RustM gleam.Int := do
  match n with
    | 0 => do (pure (0 : gleam.Int))
    | 1 => do (pure (1 : gleam.Int))
    | _ => do
      (gleam.int.add
        (← (fib (← (gleam.int.sub n (1 : gleam.Int)))))
        (← (fib (← (gleam.int.sub n (2 : gleam.Int))))))
partial_fixpoint

end fibonacci

GleamModels.lean: a shared library, regenerated each run and imported by every generated module, mapping Gleam types and operators onto Lean. It defines gleam.Int and the arithmetic the code above calls:

namespace gleam
abbrev Int := _root_.Int
end gleam

namespace gleam.int
def add (a : gleam.Int) (b : gleam.Int) : RustM gleam.Int := pure (a + b)
def sub (a : gleam.Int) (b : gleam.Int) : RustM gleam.Int := pure (a - b)
-- (mul, div, comparisons, … elided)
end gleam.int

fibonacciProofs.lean: a stub for your theorems. glean creates it once and never overwrites it, so your proofs are safe across re-runs.

4. Prove#

Write your theorems in proofs/lean/Proofs/fibonacciProofs.lean (it already imports the generated module), then:

cd proofs/lean
lake build

The first lake build fetches and builds the prelude (hax's legacy-lean plus Qq); no mathlib, so no lake exe cache get is needed.

Notes

Supported subset: Int (Lean's arbitrary-precision Int) / Float / Bool / String / Nil, generic functions, recursion, case, tuples, records, custom types (including generic ones), and the List / Result / Option types. Unsupported constructs fail with a clear message.
Standard library: pure-Gleam modules are lowered from their real source (option, result, list), so the extracted definitions are faithful with no trusted model. Modules that are @external FFI at runtime (gleam/string, gleam/int, gleam/uri) map to small Lean models (or opaque axioms) instead, since there is no Gleam body to lower.
Because a lowered stdlib function keeps its Gleam recursion shape, proving over it can be verbose. To recover a Lean library (e.g. List's lemmas), prove a one-time bridge lemma relating the lowered function to the Lean one, then rw by it. See fold_eq_foldlM in examples/fibonacci's fibonacciProofs.lean, which proves the lowered list.fold equals List.foldlM.
A @proof function's transitive callees (local or stdlib) are pulled in and extracted automatically; you only mark the top-level targets.
glean (the extractor) is bundled via Nix; proving uses Lean's own tooling (elan + lake), which manages the toolchain and the hax prelude.
glean prove with no file extracts every @proof-marked module in the project's src/. glean prove --help for options (--out-dir, --package, --stdout, --force).

Configure Feed