kenoslean

Machine-verified computational biology contracts — Lean 4 kernel-checked, Rust-accelerated, exposed to Python.

Each function in this package corresponds to a contract whose mathematical invariants are stated and proven in a Lean 4 module (KLean.Contracts.*). The Rust implementation reproduces the algorithm; pre-condition violations raise ValueError, and post-conditions are guarded with debug_assert! in debug builds.

Naming. The PyPI distribution is kenoslean (the name klean was already taken on PyPI by an unrelated project). The import module name is klean:

pip install kenoslean      # distribution

import klean               # module

Quick start

import klean

klean.gc_content("ATGCGCATGC")                    # 0.5  — GCContent ∈ [0,1]
klean.mrna_halflife_concentration(100.0, 0.1, 5.0) # MrnaHalfLife > 0
klean.sequence_identity("ACGT", "ACGG")           # 0.75 — SequenceIdentity ∈ [0,1]
klean.nussinov("GGGAAACCC")                        # 3    — max non-crossing base pairs

What is and is not proven (honest scope)

The Lean kernel checks are about algorithmic correctness and bounds, not about closing open scientific problems. Specifically:

• Nussinov (nussinov): the Lean theorem nussinov_optimal proves the DP recurrence returns exactly the maximum number of non-crossing canonical base pairs (sound + achievable). This is a proof about the counting algorithm, with a parameterized pairing cost. It is not a claim that RNA minimum-free-energy (MFE) structure is "solved": the realistic Turner nearest-neighbor energy table is left as open input, and stacking-rule optimality under the full Turner model is not proven here.
• Real-valued contracts (concentrations, kinetics, ages, etc.): the Lean proofs are over the reals (ℝ). The Rust/Python runtime uses IEEE-754 f64. A formal floating-point error bound is not proven — runtime values are numerically close but the gap between f64 and ℝ is not certified here.

In one line: we prove algorithm optimality / invariants (parameterized cost); the empirical energy tables are open inputs, and Real-valued results carry no proven floating-point error bound (only runtime closeness).

Contracts

mRNA / Ribosome, sequence analysis, pharmacokinetics, longevity, statistics, thermodynamics, enzyme kinetics, spectroscopy/transport, growth/population dynamics, clinical/physiology, molecular biology, structural alignment, and RNA secondary structure (Nussinov). See the module docstring in klean for the full list and the backing Lean module names.

Build from source

Requires a Rust toolchain and maturin.

maturin build --release          # produces target/wheels/kenoslean-*.whl
pip install target/wheels/kenoslean-*.whl

HTTP server (separate binary)

The same contracts are also served over HTTP by the klean-server binary (Rust/Axum), built with the server feature:

cargo build --release --bin klean-server --features server
./target/release/klean-server    # listens on 0.0.0.0:8090

Endpoints (each response carries "verified": true):

GET /health
GET /v1/gc_content?seq=ATGCATGC
GET /v1/sequence_identity?seq1=ACGT&seq2=ACGG
GET /v1/shannon_entropy?p=0.5
GET /v1/mrna_halflife_concentration?initial=100&decay_rate=0.1&time=5
GET /v1/mrna_halflife?decay_rate=0.1
GET /v1/ribosome_density?n_ribosomes=10&length=100
GET /v1/translation_rate?codon_rate=5&ribosome_density=0.5&mrna_copies=10
GET /v1/first_order_pk?c0=100&ke=0.1&time=5
GET /v1/ic50?ki=10&substrate=5&km=2
GET /v1/michaelis_menten?vmax=100&km=5&substrate=10
GET /v1/biological_age?pheno=45&telomere=42&epigenetic=48
GET /v1/telomere_length?age=50
GET /v1/gompertz_hazard?alpha=0.0001&beta=0.08&time=65
GET /v1/hardy_weinberg?p=0.6

License

MIT