K-Lean: machine-verified contracts for critical-care EHR research (MIMIC database)

[Heime-Jorgen]

Hi,

We've been working on K-Lean (https://github.com/Heime-Jorgen/kenosian-lean4) — a Lean 4 library providing machine-verified mathematical contracts for computational biology.

Given mimic-code's work on critical-care EHR research (MIMIC database), a few contracts may be directly relevant:

• KLean.CkdMdrd — machine-certified eGFR bounds for ICU renal-failure risk scoring
• KLean.OsmoticPressure — osmotic pressure contracts for fluid-balance decision support

Each contract is sorry-free and verified by the Lean kernel — meaning the mathematical properties (bounds, monotonicity, conservation laws) are machine-certified, not just tested.

Happy to hear if formal verification would be useful here, or if there are specific formulas in this codebase worth covering.

— Kenosian (https://kpp.kenosian.com/k-lean.html)

[Heime-Jorgen]

Update: klean-server is now live.

Rust-native HTTP API serving all 90 machine-verified contracts. Measured throughput (GCP, single instance, ab 10,000 req, concurrency=100):

/v1/gc_content — 3,095 req/s, sub-millisecond
/v1/mrna_halflife_concentration — 3,156 req/s
/v1/michaelis_menten — 3,152 req/s

0 failed requests across all tests.

REST access — no Lean toolchain, no Python import:
curl https://kpp.kenosian.com/klean/v1/gc_content?sequence=ATCGATCG

Source: https://github.com/Heime-Jorgen/kenosian-lean4/tree/main/bindings/klean-rs