A computation record that carries its own proof chain — formula, input, and timestamp — independently verifiable by any auditor.
Verify that an AI-computed result followed the stated formula — without reading code.
K-Lean audits integrity, provenance, and time — NOT scientific or biological correctness. A verified record proves that a result was produced by the stated formula, from the stated input, at the stated time. It does not prove that the formula is clinically valid, nor that the biological conclusion is true.
Biology AI tools implement published formulas — but there is no way to machine-verify that the implementation matches the paper. A lab running PhenoAge cannot prove whether their software used Levine 2018's exact coefficients or a modified version.
Lean 4 is a proof assistant: it lets a machine check that a function is mathematically identical to a published formula. Not approximately. Not probably. Identical — to the proof engine.
K-Lean applies this to biology. Each contract is a machine-checked
proof that a KPP computation equals its published algorithm.
The proof is public, reproducible, and independent of the operator.
Run lake build yourself — no trust required.
Verifies that coefficients and formula for the selected computation type match the published contract — then seals with a tamper-proof TTTPS timestamp. No code required. Select a type and press Verify.
# Step 1: run your AI tool
RESULT=$(curl -s -X POST https://kpp.kenosian.com/api/v1/analyze/bloodwork \
-H "X-API-Key: YOUR_KEY" \
-H "Content-Type: application/json" \
-d '{"chronological_age": 52}')
# Step 2: submit to K-Lean
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\": 52},
\"response_payload\": $RESULT
}"
# → { "status": "k-lean-verified", "badge_id": "klean-...", "tttps": {...} }
import requests
BASE = "https://kpp.kenosian.com"
HEADERS = {"X-API-Key": "YOUR_KEY", "Content-Type": "application/json"}
# Step 1: compute
kpp = requests.post(f"{BASE}/api/v1/analyze/bloodwork",
headers=HEADERS, json={"chronological_age": 52}).json()
# Step 2: verify
badge = requests.post(f"{BASE}/api/v1/verify/klean", headers=HEADERS, json={
"tool_id": "klean:bloodwork:phenoage:v1",
"request_payload": {"chronological_age": 52},
"response_payload": kpp,
}).json()
print(badge["status"]) # k-lean-verified
print(badge["badge_id"]) # klean-...
# Include badge_id in your FDA submission, publication, or audit trail
klean:bloodwork:phenoage:v1 PhenoAge — Levine 2018 klean:bloodwork:telomere:v1 Telomere — Herrmann 2023 klean:bloodwork:biological_age:v1 Biological Age Ensemble klean:riboswitch:design:v1 Riboswitch Design — ViennaRNA klean:synnotch:design:v1 SynNotch AND-gate klean:longevity:protocol:v1 Longevity Protocol — full pipeline
All KPP computations are K-Lean verifiable.
No trust required. Clone the repo and run lake build to machine-check all theorems locally.
# lakefile.lean require KLean from git "https://github.com/Heime-Jorgen/kenosian-lean4" @ "main"
lake update lake build # Lean 4 elaborates all theorems. No sorry. No trust.
import KLean.Contracts.PhenoAge import KLean.Contracts.Telomere import KLean.Contracts.SynNotch -- Every theorem is sorry-free and machine-checked #check KLean.PhenoAge.mortalityScore_pos -- ∀ (xb : ℝ), 0 < mortalityScore xb #check KLean.Telomere.telomere_decreasing -- ∀ (age₁ age₂ : ℝ), age₁ ≤ age₂ → telomereLength age₂ ≤ telomereLength age₁ #check KLean.SynNotch.and_gate_logic -- andGateActivated input = true ↔ ligand1_present = true ∧ ligand2_present = true
Attaching both seals to a result produces an end-to-end verifiable audit chain — proof of which formula was used, combined with an operator-independent timestamp of which input was submitted and when.
This combined record is designed to attach directly to FDA 21 CFR Part 11 §11.10(e) audit trails and DoH audit submissions.
§11.10(e) requires secure, computer-generated timestamp audit trails but does not specify operator independence of the time source. TTTPS supplies that missing independent time; K-Lean (Phase B) supplies the formula proof.
No Mathlib PR required. K-Lean is published as a standalone Lake package under Apache 2.0.
Add one line to your lakefile.lean and all 64 contracts are available.
require KLean from git "https://github.com/Heime-Jorgen/kenosian-lean4" @ "v0.1.0"
OsmoticPressure.lean via GitHub
import Mathlib across all 64 contracts
K-Lean’s sorry-free Lean 4 contracts provide machine-verified mathematical guarantees over every computation. TTTPS-certified adds the time axis: a tamper-rejecting, operator-independent record of when each computation ran — refused at ingress if backdated. Conditional on TTTPS being adopted as the standard, with Kenosian as the root of trust.
Illustrative mark for explanation only. Any certification authority, mark, or “certified” status is conditional (“could / if adopted”) and would operate under the Kenosian root — not a present-day certification program.