Repository navigation
Releases
MathCheck Engine 0.3.3
Validated Engine 0.3.3 wheel from native gate source 2556e1f. The unchanged joint native gate passed under QEMU WHPX with stock Lean 4.23.0. Engine live suite: 96 passed, 52 subtests passed. Wheel SHA-256: da94438427e02382c80dcf366c540c3e625e552966d7c873516aaca7790f6782. Full report, environment record, manifest, and stage logs are attached; RL closeout evidence is in https://github.com/stanleyngugi/mathcheck-rl/tree/main/docs/evidence/native-closeout-whpx-20261005-final.
MathCheck Engine 0.3.2
Corrective MathCheck Engine release with truthful Python compatibility metadata.
Changes:
- requires Python 3.11 through 3.13 (
>=3.11,<3.14) - removes the incorrect Python 3.10 classifier and adds Python 3.13
- adds a regression test keeping package metadata and the runtime version aligned
- no verifier semantics or supported mathematical contracts changed
Validation: 71 tests and 42 generated subtests passed, including live checks through an isolated Lean 4.23.0 toolchain. The complete clean release gate passed twice with byte-identical wheels. See release-manifest.json for the exact Lean digest, build-tool versions, and artifact hashes.
MathCheck Engine 0.3.1
First public MathCheck Engine release.
Highlights:
- bounded integer evaluation, sums, counts, and minima
- complete finite-pair certificates
- explicit verdict taxonomy and digest-bound evidence
- opt-in fail-closed Linux isolation with Lean 4.23.0
- documented trust boundary and future contract roadmap
Compatibility: the Python distribution remains lean-kernel-verifier and the import remains lean_kernel_verifier throughout the 0.x line.
Validation: 70 tests and 42 subtests passed. The clean release gate passed twice with byte-identical wheels using Lean 4.23.0. The GitHub-hosted job is pending because the account billing lock prevented a runner from starting; no workflow step failed.