K-Lean is a library of computational-biology contracts whose invariants are stated and proven in Lean 4, reproduced in Rust for speed, and exposed to Python. Every call returns the value and a certificate naming the theorems behind it.
pip · maturin · curl · Lean 4 v4.14.0 · Mathlib dde4f2e
The distribution is kenoslean (the name klean was already taken
on PyPI by an unrelated project). The import module is klean. The Python
wheel embeds a Rust extension, so calls run at native speed.
pip install kenoslean # distribution name
python -c "import klean; print(klean.nussinov('GGGAAACCC'))" # -> 3
Build from source (Rust toolchain + maturin), the path
used to produce the wheel:
git clone <kenosian-lean4 repo> cd kenosian-lean4/bindings/klean-rs maturin build --release # -> target/wheels/kenoslean-*.whl pip install target/wheels/kenoslean-*.whl
The Rust/Python runtime reproduces each algorithm that the Lean module proves things
about; pre-condition violations raise ValueError and post-conditions are guarded with
debug_assert! in debug builds. The Lean kernel checks the specification; the runtime
is a faithful re-implementation of it, not the kernel-checked term itself.
The headline contract is Nussinov base-pair maximisation: proven by nussinov_optimal to
return exactly the maximum number of non-crossing canonical base pairs (sound + achievable, no
sorry/axiom). It returns a plain int:
import klean
klean.nussinov("GGGAAACCC") # 3: max non-crossing canonical base pairs (EXACT, proven optimal)
klean.gc_content("GGCCAT") # 0.6666666666666666
klean.sequence_identity("ACGT", "ACGG") # 0.75
klean.shannon_entropy(0.5) # 1.0 (binary entropy, bits)
# pre-condition violations raise ValueError, never a silent wrong answer:
klean.nussinov("GGGXXXCCC") # ValueError: non-AUGC(T) character
Dozens of contracts ship in the same module: kinetics, pharmacokinetics, sequence/structure analysis, thermodynamics, longevity, statistics. List them and read each one's backing Lean module from the module docstring:
import klean
names = [n for n in dir(klean) if not n.startswith("_")]
print(len(names), "contracts") # e.g. nussinov, gc_content, michaelis_menten, ...
print(klean.nussinov.__doc__) # signature + backing Lean theorem
Only the integer Nussinov result is exact, proven to be the optimum. The
real-valued contracts (concentrations, kinetics, entropy, identity) are computed in IEEE-754
f64; their Lean proofs are over the reals (ℝ), and a formal floating-point error
bound is not proven. Runtime values are numerically close, but the f64↔ℝ gap is not
proven here.
The hosted compute API at kpp.kenosian.com serves the same kernel-verified contracts and
attaches a certificate + provenance to every response. Each call needs an X-API-Key header.
The compute surface produces the value from our own contracts (distinct from the
Phase A verifier at POST /api/v1/verify/klean, which re-checks a result you supply).
List the computable contracts:
curl -s https://kpp.kenosian.com/api/v1/klean/contracts \ -H "X-API-Key: $KPP_API_KEY"
Compute Nussinov (the headline exact contract):
curl -s https://kpp.kenosian.com/api/v1/klean/compute/nussinov \
-H "Content-Type: application/json" \
-H "X-API-Key: $KPP_API_KEY" \
-d '{"sequence": "GGGAAACCC"}'
Response, the exact body from the live endpoint (toolchain and Mathlib revision are real):
{
"contract": "RnaNussinov",
"value": 3,
"value_kind": "exact",
"inputs": { "sequence": "GGGAAACCC" },
"certificate": {
"contract": "RnaNussinov",
"namespace": "KLean.RnaNussinov",
"verified": true,
"key_theorems": ["nussinov_optimal", "nussinov_sound", "nussinov_achievable"],
"theorem_count": 35,
"optimality_status": "proven_optimal",
"provenance": {
"lean_toolchain": "leanprover/lean4:v4.14.0",
"mathlib_rev": "dde4f2ecaec222a1c7db638d7536f0b195d8e953",
"build_time_utc": "2026-06-19T06:43:51Z",
"kernel_verified_source": "olean-existence",
"manifest_schema": "klean.verified_contracts/v1"
}
},
"disclaimer": "Theorems prove properties of the Lean spec that this value
implements; they do not assert biological/clinical correctness."
}
Other compute endpoints follow the same shape, e.g.
POST /api/v1/klean/compute/michaelis_menten with
{"vmax": 10.0, "km": 5.0, "substrate": 2.0}, or
/compute/gc_content, /compute/shannon_entropy,
/compute/sequence_identity,
/compute/first_order_pk_concentration, each returns
value_kind: "f64_approx".
The certificate is the point of K-Lean: it tells you precisely what was proven about the value,
and against which build. Read it field by field, and treat value_kind as the load-bearing one.
| Field | Meaning |
|---|---|
| value_kind | "exact" = the value is proven to be the exact answer (integer optimum, Nussinov).
"f64_approx" = the cited theorems bound the real-valued spec, but the returned
f64 carries no proven error bound. Check this first. |
| verified | true means the named theorems are kernel-verified in the cited build and the value
is the output of the algorithm they describe. Not a biological-correctness claim. |
| key_theorems | The headline Lean theorems backing the result (e.g. nussinov_optimal,
nussinov_sound, nussinov_achievable). |
| theorem_count | Total number of supporting theorems in the contract's namespace (35 for Nussinov). |
| optimality_status | "proven_optimal" for Nussinov, sound and achievable, no sorry/axiom. |
| provenance.lean_toolchain | Exact Lean release the proofs were checked against (leanprover/lean4:v4.14.0). |
| provenance.mathlib_rev | Pinned Mathlib commit (dde4f2e…), the proofs are reproducible against it. |
| kernel_verified_source | "olean-existence": verification is evidenced by the compiled, kernel-checked
.olean artifacts for the cited build. |
| disclaimer | States plainly that theorems prove properties of the Lean spec, not biological/clinical truth. |
We prove algorithm optimality and invariants under a parameterized cost. We do not claim to have solved RNA minimum-free-energy folding, validated the empirical Turner energy tables, or replaced ViennaRNA.
Nussinov. nussinov_optimal proves the DP returns exactly the maximum number
of non-crossing canonical base pairs, a proof about the counting algorithm over a
parameterized pairing cost. It is base-pair-count optimality, not the Turner ΔG (Gibbs free
energy) that production ViennaRNA minimizes.
Zuker / Turner stacking. The context-dependent stacking DP is proven optimal in both directions for an abstract, parameterized cost. No numeric Turner constants are baked in. The empirical energy table (obligation O5) and the affine multi-loop term (O4) remain explicit, named open inputs. Plug your parameters in and the optimality theorem instantiates for them.
Real-valued contracts. Concentrations, kinetics, ages and the rest are proven over ℝ; the
runtime uses IEEE-754 f64. A formal floating-point error bound is not proven.
Values are numerically close, but the gap is not proven.
That precision is the product. We tell you exactly where the machine-checked guarantee ends, so you can cite it without overstating it.