provably.lean4¶

Lean4 backend — generate and check Lean4 proofs from @verified contracts.

from provably import verify_with_lean4, export_lean4, HAS_LEAN4, LEAN4_VERSION

`HAS_LEAN4`¶

bool — True if the lean command is available on $PATH.

from provably import HAS_LEAN4
if HAS_LEAN4:
    print("Lean4 available")

`LEAN4_VERSION`¶

str — version string from lean --version, or "" if Lean4 is not installed.

`verify_with_lean4()`¶

Verify a function using Lean4 instead of (or in addition to) Z3. Returns a ProofCertificate with z3_version set to "lean4:<version>".

from provably import verify_with_lean4

def clamp(val: float, lo: float, hi: float) -> float:
    if val < lo: return lo
    elif val > hi: return hi
    else: return val

cert = verify_with_lean4(
    clamp,
    pre=lambda val, lo, hi: lo <= hi,
    post=lambda val, lo, hi, result: (result >= lo) & (result <= hi),
)
cert.status          # Status.VERIFIED (if Lean4 closes the proof)
cert.z3_version      # "lean4:leanprover/lean4:v4.x.0"
cert.solver_time_ms  # wall-clock ms in lean

Parameter	Type	Default	Description
`func`	`Callable`	required	The function to verify
`pre`	`Callable \\| None`	`None`	Precondition lambda
`post`	`Callable \\| None`	`None`	Postcondition lambda
`timeout_s`	`float`	`60.0`	Lean4 type-check timeout in seconds

When Lean4 is not installed, returns a SKIPPED certificate with an installation hint.

`export_lean4()`¶

Export a @verified function as a Lean4 theorem file. Returns the Lean4 source code as a string. Optionally writes to a file.

from provably import export_lean4

lean_code = export_lean4(
    clamp,
    pre=lambda val, lo, hi: lo <= hi,
    post=lambda val, lo, hi, result: (result >= lo) & (result <= hi),
    output_path="clamp.lean",
)
print(lean_code)
# -- Auto-generated by provably.lean4
# import Mathlib.Tactic
# noncomputable def clamp_impl ...
# theorem clamp_verified ...

Parameter	Type	Default	Description
`func`	`Callable`	required	The function to export
`pre`	`Callable \\| None`	`None`	Precondition lambda
`post`	`Callable \\| None`	`None`	Postcondition lambda
`output_path`	`str \\| Path \\| None`	`None`	Write Lean4 source to this path

Does not require Lean4 to be installed (generates code only).

Pipeline¶

The Lean4 backend follows the same flow as the Z3 backend:

Parse function AST + contracts
Generate Lean4 noncomputable def from the function body
Generate theorem ... := by unfold; split_ifs <;> nlinarith
Write to a temp .lean file
Run lean to type-check
Return ProofCertificate with outcome

Limitations¶

Same arithmetic subset as Z3 translator (no recursion, no data structures)
Transcendental functions (exp, cos, log) are axiomatized
For-loop unrolling produces verbose Lean4 proofs
Slower than Z3 (compiles to native code)
Requires Lean4 + Mathlib for nlinarith tactic

Installation¶

# Install elan (Lean4 version manager)
brew install elan-init   # macOS
# or: curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh

# Set stable toolchain
elan default stable

provably.lean4 ¶

Lean4 backend — generate and check Lean4 proofs from @verified contracts.

Translates Python functions with pre/post conditions into Lean4 theorem statements + tactic proofs. The Lean4 type checker then serves as an independent verification oracle (cross-checking Z3 results).

Pipeline

Parse function AST + contracts (same as Z3 backend)
Generate Lean4 theorem statement from pre/post
Generate tactic proof sketch (nlinarith/omega/simp/linarith)
Write to temp .lean file
Run lean to type-check
Return ProofCertificate with status and lean4 proof text

Requirements

Lean4 installed (via elan): brew install elan-init && elan default stable
No Mathlib needed for basic arithmetic theorems (uses Lean4 stdlib)

Limitations

Only supports the same arithmetic subset as the Z3 translator
Transcendental functions (exp, cos, log) are axiomatized
For-loop unrolling produces verbose proofs
Slower than Z3 (compiles to native code)

Classes¶

Functions¶

check_lean4_proof ¶

check_lean4_proof(lean_code: str, timeout_s: float = 60.0) -> tuple[bool, str]

Write Lean4 code to a temp file and check it.

Returns (success, output).

Source code in src/provably/lean4.py

def check_lean4_proof(lean_code: str, timeout_s: float = 60.0) -> tuple[bool, str]:
    """Write Lean4 code to a temp file and check it.

    Returns (success, output).
    """
    if not HAS_LEAN4:
        return False, "Lean4 not installed"

    with tempfile.NamedTemporaryFile(
        mode="w", suffix=".lean", delete=False, prefix="provably_"
    ) as f:
        f.write(lean_code)
        tmp_path = f.name

    try:
        result = subprocess.run(
            ["lean", tmp_path],
            capture_output=True,
            text=True,
            timeout=timeout_s,
        )
        output = (result.stdout + result.stderr).strip()
        return result.returncode == 0, output
    except subprocess.TimeoutExpired:
        return False, f"Lean4 timed out after {timeout_s}s"
    except FileNotFoundError:
        return False, "lean command not found"
    finally:
        Path(tmp_path).unlink(missing_ok=True)

export_lean4 ¶

export_lean4(func: Any, pre: Any | None = None, post: Any | None = None, output_path: str | Path | None = None) -> str

Export a @verified function as a Lean4 theorem file.

Returns the Lean4 source code. Optionally writes to output_path.

Source code in src/provably/lean4.py

def export_lean4(
    func: Any,
    pre: Any | None = None,
    post: Any | None = None,
    output_path: str | Path | None = None,
) -> str:
    """Export a @verified function as a Lean4 theorem file.

    Returns the Lean4 source code. Optionally writes to output_path.
    """
    import z3 as _z3

    from .types import extract_refinements, make_z3_var

    fname = getattr(func, "__name__", str(func))
    source = textwrap.dedent(inspect.getsource(func))

    tree = ast.parse(source)
    func_ast = tree.body[0]
    if not isinstance(func_ast, ast.FunctionDef):
        return "-- Error: not a function definition\n"

    try:
        from typing import get_type_hints

        hints = get_type_hints(func, include_extras=True)
    except Exception:
        hints = {}

    param_names = [arg.arg for arg in func_ast.args.args]
    param_types: dict[str, type] = {}
    param_vars: dict[str, Any] = {}
    for name in param_names:
        typ = hints.get(name, float)
        param_types[name] = typ
        param_vars[name] = make_z3_var(name, typ)

    param_list = [param_vars[n] for n in param_names]
    pre_strs: list[str] = []
    post_strs: list[str] = []

    # Soundness: the exporter must refuse to emit an incomplete theorem
    # when the user's pre/post raises. A silently-dropped pre becomes a
    # Lean theorem stronger than the user asked for, which will either
    # fail to type-check (OK) or type-check spuriously if the post is
    # trivially true (NOT OK).
    if pre is not None:
        try:
            pre_z3 = pre(*param_list)
        except Exception as e:  # noqa: BLE001 — re-raised as ValueError
            raise ValueError(f"Precondition raised when exporting: {e}") from e
        if isinstance(pre_z3, _z3.BoolRef):
            pre_strs.append(str(pre_z3))

    for name, var in param_vars.items():
        typ = hints.get(name)
        if typ is not None:
            for constraint in extract_refinements(typ, var):
                pre_strs.append(str(constraint))

    if post is not None:
        result_var = _z3.Real("result")
        try:
            post_z3 = post(*param_list, result_var)
        except Exception as e:  # noqa: BLE001 — re-raised as ValueError
            raise ValueError(f"Postcondition raised when exporting: {e}") from e
        if isinstance(post_z3, _z3.BoolRef):
            post_strs.append(str(post_z3))

    pre_lean = (
        " ∧ ".join(f"({_z3_str_to_lean(s, param_names)})" for s in pre_strs) if pre_strs else None
    )
    post_lean = (
        " ∧ ".join(f"({_z3_str_to_lean(s, param_names)})" for s in post_strs)
        if post_strs
        else None
    )

    if post_lean:
        post_lean = post_lean.replace("result", f"({fname}_impl {' '.join(param_names)})")

    lean_code = generate_lean4_theorem(
        func_name=fname,
        param_names=param_names,
        param_types=param_types,
        pre_str=pre_lean,
        post_str=post_lean,
        source=source,
    )

    if output_path is not None:
        Path(output_path).write_text(lean_code)

    return lean_code

generate_lean4_theorem ¶

generate_lean4_theorem(func_name: str, param_names: list[str], param_types: dict[str, type], pre_str: str | None, post_str: str | None, source: str) -> str

Generate a complete Lean4 file with theorem statement + proof attempt.

Chooses between TWO output modes:

core (kernel-clean, no Mathlib): emitted whenever every parameter and the return are Int or Bool. Returns an Int/Bool def and uses only core tactics (omega, decide, split, rfl). The output is independent of Mathlib and passes #print axioms with only the standard foundational axioms.
mathlib (requires Mathlib on the Lean search path): emitted when any parameter or the return is float and we therefore need ℝ. Uses nlinarith/linarith from Mathlib. If Mathlib isn't available at check time, check_lean4_proof will report the missing-import failure honestly rather than silently "passing".

Source code in src/provably/lean4.py

def generate_lean4_theorem(
    func_name: str,
    param_names: list[str],
    param_types: dict[str, type],
    pre_str: str | None,
    post_str: str | None,
    source: str,
) -> str:
    """Generate a complete Lean4 file with theorem statement + proof attempt.

    Chooses between TWO output modes:

    * **core** (kernel-clean, no Mathlib): emitted whenever every parameter
      and the return are ``Int`` or ``Bool``. Returns an ``Int``/``Bool``
      def and uses only core tactics (``omega``, ``decide``, ``split``,
      ``rfl``). The output is independent of Mathlib and passes
      ``#print axioms`` with only the standard foundational axioms.

    * **mathlib** (requires Mathlib on the Lean search path): emitted when
      any parameter or the return is ``float`` and we therefore need ℝ.
      Uses ``nlinarith``/``linarith`` from Mathlib. If Mathlib isn't
      available at check time, ``check_lean4_proof`` will report the
      missing-import failure honestly rather than silently "passing".
    """
    tree = ast.parse(source)
    func_ast = tree.body[0]
    if not isinstance(func_ast, ast.FunctionDef):
        return "-- Error: not a function definition\nsorry"

    # Pick the output mode from parameter types.
    all_int_or_bool = all(param_types.get(name, float) in (int, bool) for name in param_names)
    # Crude return-type check — the decorator already filters out
    # unsupported annotations so ``float`` is the only 'must use ℝ'.
    ret_hint: type | None = None
    returns = getattr(func_ast, "returns", None)
    if isinstance(returns, ast.Name):
        if returns.id == "int":
            ret_hint = int
        elif returns.id == "bool":
            ret_hint = bool
        elif returns.id == "float":
            ret_hint = float
    core_mode = all_int_or_bool and ret_hint in (int, bool, None)

    params = []
    for name in param_names:
        typ = param_types.get(name, float)
        lean_type = _py_type_to_lean(typ)
        if core_mode:
            # Keep Int/Bool as-is.
            pass
        elif lean_type == "Float":
            lean_type = "ℝ"
        params.append(f"({name} : {lean_type})")
    param_decl = " ".join(params)

    env = {n: n for n in param_names}
    body = _func_body_to_lean(func_ast, env)

    return_type = (
        "Int"
        if core_mode and ret_hint is int
        else "Bool"
        if core_mode and ret_hint is bool
        else "Int"
        if core_mode
        else "ℝ"
    )
    def_kw = "def" if core_mode else "noncomputable def"

    lean_lines = [
        "-- Auto-generated by provably.lean4",
        f"-- Source: @verified function '{func_name}'",
        f"-- Mode: {'core (kernel-clean, no Mathlib)' if core_mode else 'mathlib (requires Mathlib)'}",
        "",
    ]
    if not core_mode:
        lean_lines.append("import Mathlib.Tactic")
        lean_lines.append("")
    lean_lines.extend(
        [
            f"{def_kw} {func_name}_impl {param_decl} : {return_type} :=",
            f"  {body}",
            "",
        ]
    )

    # Pick a tactic that stays in the chosen mode.
    if core_mode:
        tactic = "split <;> first | omega | decide | rfl | (intro h_pre; omega)"
    else:
        tactic = "split_ifs <;> nlinarith"

    if pre_str and post_str:
        lean_lines.extend(
            [
                f"theorem {func_name}_verified {param_decl}",
                f"  (h_pre : {pre_str})",
                f"  : {post_str} := by",
                f"  unfold {func_name}_impl",
                f"  {tactic}",
            ]
        )
    elif post_str:
        lean_lines.extend(
            [
                f"theorem {func_name}_verified {param_decl}",
                f"  : {post_str} := by",
                f"  unfold {func_name}_impl",
                f"  {tactic}",
            ]
        )
    else:
        lean_lines.append(f"-- No postcondition to prove for {func_name}")

    if core_mode:
        # Helps the reader audit kernel-cleanness.
        lean_lines.extend(
            [
                "",
                f"-- To audit: #print axioms {func_name}_verified",
                "-- A kernel-clean proof depends only on propext, Quot.sound,",
                "-- Classical.choice (and their ilk) — never 'sorry' or Mathlib.",
            ]
        )

    return "\n".join(lean_lines)

verify_with_lean4 ¶

verify_with_lean4(func: Any, pre: Any | None = None, post: Any | None = None, timeout_s: float = 60.0) -> ProofCertificate

Verify a function using Lean4 instead of (or in addition to) Z3.

Same interface as verify_function but uses Lean4 type checker.

Source code in src/provably/lean4.py

def verify_with_lean4(
    func: Any,
    pre: Any | None = None,
    post: Any | None = None,
    timeout_s: float = 60.0,
) -> ProofCertificate:
    """Verify a function using Lean4 instead of (or in addition to) Z3.

    Same interface as verify_function but uses Lean4 type checker.
    """
    import z3 as _z3

    from .types import extract_refinements, make_z3_var

    fname = getattr(func, "__name__", str(func))

    if not HAS_LEAN4:
        return ProofCertificate(
            function_name=fname,
            source_hash="",
            status=Status.SKIPPED,
            preconditions=(),
            postconditions=(),
            message="Lean4 not installed (install via: brew install elan-init && elan default stable)",
        )

    # Get source
    try:
        source = textwrap.dedent(inspect.getsource(func))
    except (OSError, TypeError) as e:
        return ProofCertificate(
            function_name=fname,
            source_hash="",
            status=Status.SKIPPED,
            preconditions=(),
            postconditions=(),
            message=f"Cannot get source: {e}",
        )

    # Parse
    tree = ast.parse(source)
    func_ast_raw = tree.body[0]
    if not isinstance(func_ast_raw, ast.FunctionDef):
        return ProofCertificate(
            function_name=fname,
            source_hash="",
            status=Status.TRANSLATION_ERROR,
            preconditions=(),
            postconditions=(),
            message="Not a function definition",
        )
    func_ast: ast.FunctionDef = func_ast_raw

    # Extract param info
    try:
        from typing import get_type_hints

        hints = get_type_hints(func, include_extras=True)
    except Exception:
        hints = {}

    param_names = [arg.arg for arg in func_ast.args.args]
    param_types: dict[str, type] = {}
    param_vars: dict[str, Any] = {}
    for name in param_names:
        typ = hints.get(name, float)
        param_types[name] = typ
        param_vars[name] = make_z3_var(name, typ)

    # Build Z3 string representations of pre/post.
    #
    # Soundness rule: if the user's pre/post lambdas raise when evaluated
    # against symbolic Z3 variables we must NOT silently discard the
    # constraint — doing so would let Lean4 "prove" too much (pre = True).
    # Return a translation-error certificate instead so the caller can see
    # WHY verification refused.
    pre_strs: list[str] = []
    post_strs: list[str] = []
    param_list = [param_vars[n] for n in param_names]

    if pre is not None:
        try:
            pre_z3 = pre(*param_list)
        except Exception as e:  # noqa: BLE001 — surfaced as cert
            return ProofCertificate(
                function_name=fname,
                source_hash="",
                status=Status.TRANSLATION_ERROR,
                preconditions=(),
                postconditions=(),
                message=f"Precondition error: {e}",
            )
        if isinstance(pre_z3, _z3.BoolRef):
            pre_strs.append(str(pre_z3))

    # Add refinement constraints
    try:
        for name, var in param_vars.items():
            typ = hints.get(name)
            if typ is not None:
                for constraint in extract_refinements(typ, var):
                    pre_strs.append(str(constraint))
    except TypeError as e:
        return ProofCertificate(
            function_name=fname,
            source_hash="",
            status=Status.TRANSLATION_ERROR,
            preconditions=(),
            postconditions=(),
            message=f"Refinement error: {e}",
        )

    if post is not None:
        # Create a result variable for postcondition
        result_var = _z3.Real("result")
        try:
            post_z3 = post(*param_list, result_var)
        except Exception as e:  # noqa: BLE001 — surfaced as cert
            return ProofCertificate(
                function_name=fname,
                source_hash="",
                status=Status.TRANSLATION_ERROR,
                preconditions=(),
                postconditions=(),
                message=f"Postcondition error: {e}",
            )
        if isinstance(post_z3, _z3.BoolRef):
            post_strs.append(str(post_z3))

    # Convert to Lean4 syntax
    pre_lean = (
        " ∧ ".join(f"({_z3_str_to_lean(s, param_names)})" for s in pre_strs) if pre_strs else None
    )
    post_lean = (
        " ∧ ".join(f"({_z3_str_to_lean(s, param_names)})" for s in post_strs)
        if post_strs
        else None
    )

    # Replace 'result' with the actual function definition body
    if post_lean:
        post_lean = post_lean.replace("result", f"({fname}_impl {' '.join(param_names)})")

    # Generate Lean4 code
    lean_code = generate_lean4_theorem(
        func_name=fname,
        param_names=param_names,
        param_types=param_types,
        pre_str=pre_lean,
        post_str=post_lean,
        source=source,
    )

    # Check with Lean4
    t0 = time.monotonic()
    success, output = check_lean4_proof(lean_code, timeout_s=timeout_s)
    elapsed = (time.monotonic() - t0) * 1000

    source_hash = hashlib.sha256(source.encode()).hexdigest()[:16]

    if success:
        return ProofCertificate(
            function_name=fname,
            source_hash=source_hash,
            status=Status.VERIFIED,
            preconditions=tuple(pre_strs),
            postconditions=tuple(post_strs),
            solver_time_ms=elapsed,
            z3_version=f"lean4:{LEAN4_VERSION}",
            message="Lean4 type-checked successfully",
        )
    else:
        return ProofCertificate(
            function_name=fname,
            source_hash=source_hash,
            status=Status.UNKNOWN,
            preconditions=tuple(pre_strs),
            postconditions=tuple(post_strs),
            solver_time_ms=elapsed,
            z3_version=f"lean4:{LEAN4_VERSION}",
            message=f"Lean4 proof failed: {output[:500]}",
        )

provably.lean4¶

HAS_LEAN4¶

LEAN4_VERSION¶

verify_with_lean4()¶

export_lean4()¶

Pipeline¶

Limitations¶

Installation¶

provably.lean4 ¶

Classes¶

Functions¶

check_lean4_proof ¶

export_lean4 ¶

generate_lean4_theorem ¶

verify_with_lean4 ¶

`HAS_LEAN4`¶

`LEAN4_VERSION`¶

`verify_with_lean4()`¶

`export_lean4()`¶