Lean Bridge (Roadmap & Boundaries)

Lean integration is optional and scoped. The goal is to formalize invariants around schemas and transformations, not to prove biology.

What we plan to prove

• Schema well-formedness: required fields, type contracts, additionalProperties limits.
• Determinism invariants: given a seed + backend class (D0/D1), outputs remain within tolerance.
• Transformation soundness for small kernels (e.g., edit DAG normalization, scoring helpers) where specs are tractable.
• Provenance preservation: manifests correctly reflect file hashes after transformations.

What will not be proved

• Empirical models (e.g., on-target/off-target efficacy) or GPU floating-point rounding beyond documented tolerances.
• Biological correctness or lab protocols; these remain empirical and validated via tests, not proofs.
• Performance bounds or throughput guarantees.

Phased roadmap

1. Spec extraction: auto-generate Lean skeletons from JSON Schemas and simple kernels; keep alongside schemas/.
2. Selective proofs: prove small, pure components (parsers, canonical ordering, hash computation) and ship CI checks.
3. Witnesses in artifacts: optionally embed proof hashes in manifests for the components proved.
4. Optional enforcement: allow policy.profile = audit-strict to require proof presence for the covered components.

Communication

• All Lean-related artifacts remain opt-in and do not gate regular users.
• Roadmap updates live here; proofs ship only when they do not compromise determinism or usability.