Formal proofs as infrastructure

Add to your lakefile.lean, (repository re-organizing; install available again shortly)

require KLean from git
  "..." @ "main"

-- then import any contract:
import KLean.Contracts.MichaelisMenten
import KLean.Contracts.PhenoAge

# clone the repository (re-organizing, back shortly)
cd kenosian-lean4
lake build
# Lean 4 elaborates all theorems. No sorry. No trust.

#check KLean.MichaelisMenten.velocity_monotone
#check KLean.HardyWeinberg.hardy_weinberg_equilibrium
#check KLean.ContactProbability.sigmoid_pos

96 contracts across 10 domains. Every theorem is sorry-free, verified by the Lean 4 kernel. No sorry. No trust required.

For every contract, each domain, each key theorem (named exactly as in the Lean source), and what it proves, see the complete library page: Browse all 96 contracts →

K-Lean contracts are in active use for verifying computational models in ongoing research. In one case, a biomedical researcher applied ErythropoiesisODE.lean to formally verify boundary conditions of an erythropoiesis model, confirming RBC count non-negativity and convergence under physiological stimulation rates. The machine-verified contract replaced a manual parameter review step.

K-Lean follows the leanblueprint academic standard:

\appendix
\section{Formal Verification (K-Lean)}
All numerical claims in this paper have been machine-verified using Lean 4.
See FORMALIZATION.md.

Reference as:

@software{klean2026,
  title  = {K-Lean: Machine-Verified Mathematical Contracts for Biology},
  author = {Jang, Peter},
  year   = {2026},
  note   = {Lean 4 formal proofs, sorry-free}
}

K-Lean contracts are mathematical specifications. To connect them to your implementation, no Lean installation required, translate each invariant into a property test.

from hypothesis import given, strategies as st

@given(st.text(alphabet="ACGT", min_size=1))
def test_gc_content_bounds(seq):
    gc = compute_gc_content(seq)
    assert 0.0 <= gc <= 1.0          # KLean.GCContent invariant

@given(st.floats(min_value=0), st.floats(min_value=0))
def test_mrna_halflife_positive(k, t):
    result = mrna_concentration(k, t)
    assert result >= 0               # KLean.MrnaHalfLife invariant

test_that("gc_content bounds", {
  expect_true(gc_content(seq) >= 0 && gc_content(seq) <= 1)
})

# pip install kenoslean   (coming soon)
from klean import gc_content, mrna_halflife, sequence_identity

We are building a Rust implementation of all 96 contracts, compiled to a Python extension via PyO3. This closes the gap between formal Lean specification and running Python code, no Lean toolchain required in your CI.

A Rust-native HTTP API (Axum) serving all 96 contracts at 3,095+ req/s (GCP, single instance), with sub-millisecond per-call latency. No Lean toolchain required.

import requests
r = requests.post("https://kpp.kenosian.com/v1/michaelis_menten",
    json={"substrate": 0.5, "km": 0.1, "vmax": 2.0})
print(r.json())

curl https://kpp.kenosian.com/klean/v1/gc_content?sequence=ATCGATCG

K-Lean contracts are enforced at runtime via the KPP API (kpp.kenosian.com):

curl -X POST https://kpp.kenosian.com/api/v1/verify/klean \
  -H "X-API-Key: YOUR_KEY" \
  -H "Content-Type: application/json" \
  -d '{
    "tool_id": "klean:bloodwork:phenoage:v1",
    "request_payload": {"chronological_age": 45, "albumin": 4.1},
    "response_payload": {"phenotypic_age": 38.2}
  }'

Returns a TTTPS-sealed badge with roughtime_k ≥ 3 (operator-independent timestamp).

All theorems must be sorry-free. CI checks this on every push (grep -r "sorry" KLean/ && exit 1). We welcome contributions, new biology contracts, proof improvements, or domain extensions. Issues and pull requests welcome.

Licensed under Apache 2.0.

K-Lean is the first Lean 4 library for computational biology. Analogous: TLA+ : distributed protocols :: K-Lean : biological computation.