Skip to content

JACKAL v1.7.4 — spacecraft finite-burn formal certificate

Choose a tag to compare

View all tags
@AnubisQuantumCipher AnubisQuantumCipher released this 25 Aug 00:16
· 48 commits to master since this release
v1.7.4
9a0aaca
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

JACKAL v1.7.4 — spacecraft finite-burn formal certificate

This release adds a machine-checked certificate with the qualified verdict:

CERTIFIED SAFE under the stated finite-burn ODE model, supplied input bounds, and machine-checked interval-certificate assumptions.

The authoritative Lean theorem is JackalIv.Spacecraft.spacecraft_burn_certified_safe. The exact audited axiom set is propext, Classical.choice, and Quot.sound; the 57-file source admission scan covers 27 release theorems and reports zero logical admissions.

The release bundle binds the 35,939,138-byte witness, receipt, request, native macOS arm64 checker, proof-source closure, independent replay, instrument validation, mutation A-B-A evidence, and 16-pass independent review. Use SHA256SUMS and VERIFICATION.md to reproduce the checks from freshly downloaded assets.

JACKEL remains a mechanically derived 41-tool MCP runtime on runtime package v1.7.3. The bundled skill and plugin identity are updated for this v1.7.4 release surface; spacecraft certification is a release/CLI workflow, not a 42nd MCP tool.

This release does not establish physical-model adequacy, truth of supplied bounds, omitted perturbations, actuator behavior, source-to-native compiler correctness, or universal spacecraft safety. The Python producer is candidate-only; only the pinned Lean checker can mint the formal-bounded result.

Assets 13
Loading