21 CFR Part 11 sets the conditions under which the FDA treats electronic records and electronic signatures as trustworthy. TTTPS-K-Lean does not claim to make a system “Part 11 compliant”: it provides verifiable technical controls for the two requirements that are hardest to evidence: system validation (§11.10(a)) and a secure, computer-generated audit trail (§11.10(e)).
Machine-checked validation · tamper-evident time seal21 CFR Part 11 is the FDA rule that lets electronic records and electronic signatures be treated as equivalent to paper records and handwritten signatures. It is the backbone of GxP (Good Laboratory, Clinical, and Manufacturing Practice) computing: any system that creates, modifies, or stores records used to meet FDA requirements falls under it.
For a closed system (one whose access is controlled by the people responsible for the records), §11.10 lists the controls the sponsor must put in place. Two of them are notoriously hard to evidence rather than merely assert: that the system has been validated to perform as intended (§11.10(a)), and that it keeps a secure, computer-generated, time-stamped audit trail (§11.10(e)). Electronic signatures are governed separately under §§11.100 onward, and must be cryptographically bound to their records under §11.70.
Most Part 11 controls are organizational: SOPs, training, access policy. Two are deeply technical, and these are where TTTPS-K-Lean carries weight: it turns “the system was validated” and “the audit trail is trustworthy” from claims into verifiable evidence.
“Validation of systems to ensure accuracy, reliability, consistent intended performance, and the ability to discern invalid or altered records.”
K-Lean's kernel-verified formal proofs establish that a computation matches its stated specification and mathematical properties, checked mechanically by the Lean 4 kernel. Test-based validation demonstrates behaviour on the cases you tried; a formal proof establishes it for all inputs the specification covers.
“Validated” here is not an opinion in a report. It is a proof object the kernel accepted, evidence that can be re-checked independently by anyone with the artifact.
“Use of secure, computer-generated, time-stamped audit trails to independently record the date and time of operator entries and actions that create, modify, or delete electronic records.”
TTTPS tamper-evident timestamps seal the date and time of an action independently of the operator. The seal is computer-generated and cannot be silently back-dated or edited by a person, exactly the “secure, computer-generated, time-stamped” property the regulation asks for.
This is the painkiller: audit-trail integrity is the control most often cited in FDA findings, and the hardest to prove was not altered after the fact.
“Protection of records to enable their accurate and ready retrieval throughout the records retention period.”
“Electronic signatures and handwritten signatures executed to electronic records shall be linked to their respective electronic records to ensure that the signatures cannot be excised, copied, or otherwise transferred to falsify an electronic record by ordinary means.”
The TTTPS seal cryptographically binds the verified computation result to the sealed time. Because the binding is cryptographic, a record cannot be detached from its verification or its timestamp and re-attached elsewhere without detection, supporting record protection under §11.10(c) and the signature/record linking principle of §11.70 by making after-the-fact alteration detectable rather than silent.
TTTPS-K-Lean provides technical controls: verifiable validation evidence (machine-checked proofs) and audit-trail integrity (tamper-evident, computer-generated time seals). These map directly onto the two hardest Part 11 requirements.
It does not replace a sponsor's full Part 11 compliance program: SOPs, personnel training, access controls, and the operating procedures for electronic signatures remain the sponsor's responsibility. It makes no clinical or biological claim.
This page does not assert that any system is “21 CFR Part 11 compliant.” It provides verifiable technical evidence for the two controls that are hardest to demonstrate (validation and the audit trail) and names the boundary of that evidence precisely.
| Part 11 requirement | What TTTPS-K-Lean provides | Status |
|---|---|---|
| §11.10(a) Validation |
Machine-checked formal proof that a computation matches its specification and mathematical properties, re-checkable by the Lean 4 kernel. | technical control provided |
| §11.10(e) Audit trail |
Tamper-evident, computer-generated TTTPS timestamps that independently seal the date and time of record-affecting actions. | technical control provided |
| §11.10(c) Record protection |
Cryptographic binding of verified result to sealed time, making after-the-fact alteration detectable. | supporting control |
| §11.70 Signature/record linking |
Cryptographic linkage so a record cannot be detached from its verification or timestamp without detection. | supporting control |
| SOPs · training · access · e-sig ops |
Out of scope, remains the sponsor's compliance program. | sponsor responsibility |
Deep survival models (e.g. torchsurv) are commonly evaluated with the
time-dependent, censoring-adjusted (IPCW) Brier score. This contract does not validate any specific model
or dataset — it machine-checks the mathematical properties the score itself must satisfy:
non-negativity, the [0,1] upper bound, and that a perfect prediction attains the minimum.
| Theorem | Property |
|---|---|
| brier_nonneg | Score is always ≥ 0 |
| brier_le_one | Score is ≤ 1 when predictions/outcomes lie in [0,1] |
| brier_zero_iff_perfect | Score = 0 iff prediction is exact on every subject |
| brier_perfect_is_min | A perfect prediction attains the minimum possible score |
| survBrier_nonneg / survBrier_zero_iff | Same properties for the IPCW-weighted survival form |
7 theorems, Lean 4 kernel-checked —
sorry count 0, axiom count 0, lake build exit 0.
Source: KLean/Contracts/BrierScore.lean — private repository, available on request:
info@kenosian.com.
Makes no claim about any specific model, dataset, or clinical outcome.