Limitations

Single classifier family: affine binary over ℚ.
Single robustness notion: L∞ margin with ‖w‖₁ Lipschitz factor.
Strict inequality required; boundary equality is not certified.
Classification uses strict positivity (score > 0); score 0 is class false.
No floating-point soundness claim.
Docker/CI Lean builds download mathlib on first run (large).
v0.1.0 is unauthorized until independent review (LV-11) and the §14 checklist in release-process.md complete.
Legacy FormalVerifML breadth is intentionally excluded from the supported surface.

FilesExpand file tree