JACKAL v1.7.5 - Spacecraft finite-burn certification

JACKAL v1.7.5 - Spacecraft finite-burn certification

This corrective release publishes the review-cleared spacecraft finite-burn
certificate, its pinned Lean checker identity, the full witness, independent
outer replay, adversarial mutation evidence, and a self-contained macOS arm64
verification archive.

Qualified result

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

The checker-accepted exact dyadic safety-margin interval has a strictly positive
lower endpoint. The result is conditional on the encoded model and supplied
input intervals; it is not a claim that the model captures every physical
spacecraft effect or that the inputs are true for a mission.

Verification boundary

• The pinned Lean checker independently validates every accepted tube, cutoff
  cell, orbital bound, and final positive margin.
• The Python Picard witness generator and its source are not formally verified.
  They remain trusted for termination, witness search, completeness, and
  reproducible generation, but cannot authorize formal-bounded without the
  checker and outer-verifier gates.
• The proof identity binds the admitted Lean source closure, pinned dependency
  trees, complete private Lean toolchain tree, checker bytes, and generator
  closure. Platform/runtime and physical-model assumptions remain explicit.
• VERIFICATION.md and SHA256SUMS describe the exact offline replay for all
  twelve release assets.

Publication is complete only when fresh public downloads reproduce the tagged
commit, asset roster, sizes, checksums, checker result, outer replay, and this
exact release title and notes body.

JACKAL v1.7.4 — spacecraft finite-burn formal certificate

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.

JACKEL Codex Plugin 0.1.0+codex.20260824111802

Publishes the JACKEL Codex wrapper and operational skill aligned to the existing sealed JACKAL v1.7.3 41-tool runtime.

Highlights:

• published-runtime wording replaces stale candidate guidance
• canonical exact-claim syntax uses command: mod-pow with ordered string arguments
• fresh Codex-host claim issuance and independent replay now pass using the sandbox authority required for private runtime snapshots, without bypassing approvals
• adapter-only cachebuster lineage advances without rewriting the sealed v1.7.3 kernel inventory

Plugin aggregate SHA-256: 6b7d17fff5056838f13877953157ca841cf4d542cf25300950420350971254f6
Plugin archive SHA-256: d4e56fc9a8697fc665b18c6bf5ec516f96513262eb33ac936b3de4920cb8fc5b
Bound runtime SHA-256: 68b0e7850fcb60358633908f70ffcf405cbbef103b04d3d93dd1298789e505ae

Verification: 35/35 inventory and drift tests, 220/220 Codex plugin tests, isolated 41-tool acceptance, and fresh Codex 0.146.0 host claim/replay acceptance.

Boundary: this release contains the Codex plugin only. It does not replace or modify the v1.7.3 runtime, formal checkers, capability inventory, or assurance ceilings.

JACKAL v1.7.3 — Unified 41-Tool Evidence Surface

JACKAL v1.7.3 — Unified 41-Tool Evidence Surface

JACKAL v1.7.3 promotes one mechanically generated 41-tool catalog across the kernel, Hermes contract, and Codex plugin. Profiles are core=3, formal=13, and full=41.

Merge commit: a43919e83fe141320fbc041f9be649b5ebe9e82c
Annotated tag object: 45a2534e3288d9b43ff453161e567d0158ea0ea6
PR: #12

What is added

• Canonical generated capability inventory with exact schemas, profile exposure, evidence classes, dependencies, admitted fragments, and refusal boundaries.
• Full Hermes/Codex parity for all 41 tools, including claim/bundle replay, domain-pack operations, and the three Anubis program-evidence routes.
• inventory-safe-v1 program evidence with strict source/compiler/artifact/policy pins, Z3 UNSAT replay, independent RUP replay, and explicit residual non-claims.
• Published Codex runtime provisioning bound to the exact package size, package digest, and internal SHA256SUMS digest.
• Documentation and skill drift gates that reject stale counts, tool names, status vocabulary, package pins, and release-state claims.

Assets

Asset	Size	SHA-256
jackal-v1.7.3-macos-arm64.tar.gz	158,363,786 bytes	68b0e7850fcb60358633908f70ffcf405cbbef103b04d3d93dd1298789e505ae
jackal-v1.7.3-evidence.tar.gz	562,653 bytes	32c0ceffdfb347f25bcb57f2f4fefc7a688dc048a10e64312d65930a675d7e90
jackal-v1.7.3-release-receipt.json	5,828 bytes	fef6a8ba3ab99c27f67e8d901d852ea52ef35c0474683bbd6daa4f229fe4f372
SHA256SUMS	296 bytes	1c5fd0526231f462028917be3d802de39ec73ddce9c2b11806e86983370c09ba

Package internals:

• 106 regular files; 119 extracted entries excluding the package root
• 555,511,970 extracted regular-file bytes
• internal SHA256SUMS SHA-256: a78fc05e2ebd56f31263d54ccdbf7fcc2ff92d270758720c3e235d5a3121568a
• MANIFEST.sha256: ac52dafc0e9edbf74dde56b358c3c55ab5b705d3b66811558156c480b3530509
• capability inventory: e2a4984329b3fd2fecc8de738dce20a5f046e0a876119569e72e41a04192a8f5

Verification

• Two clean detached builds produced byte-identical tarballs and identical extracted trees.
• Inventory/drift 31/31; Lean admission 26/26; program verifier 15/15; hostile program controls 15/15; skill contracts 5/5.
• Package 15/15 with zero skips; rebuild/parity campaign 60/60; Codex repository suite 218/218.
• Isolated provisioned Codex live acceptance discovered exactly 41 tools and passed exact, formal-bounded, refusal, claim-bundle, and formal-receipt checks.
• All hosted Codex, Lean source/axiom, claim-kernel, and CodeRabbit checks passed on the merged head.

First-run verification

shasum -a 256 -c SHA256SUMS
tar -xzf jackal-v1.7.3-macos-arm64.tar.gz
cd jackal-v1.7.3-macos-arm64
shasum -a 256 -c SHA256SUMS
./plugin/hermes/jackal_hermes selftest

Trust boundary and non-claims

• Apple-Silicon macOS only; unsigned and not notarized.
• formal-bounded is limited to checker-admitted fragments; it is not arbitrary-expression formal correctness.
• inventory-safe-v1 does not establish policy-construct totality, source-to-VC, SMT-to-CNF, source-native refinement, runtime behavior, or universal language soundness.
• No compiler-correctness, input-truth, operating-system, hardware, supply-chain, or authenticated-builder claim is made.

JACKAL v1.7.2 — Closed-Premise Range + Int-Cert Checker Request Contracts

JACKAL v1.7.2 — Closed-Premise Range + Int-Cert Checker Request Contracts

Discharges the eight Gate-0 semantic-premise blockers documented in
docs/superpowers/plans/2026-08-17-jackal-gate0-checker-contract.md.
Ships a coherent v1.7.2 package for Apple Silicon macOS with the
archival inventory tuple pinned across code, docs, and gates.

Merge commit: 54461bbc8f135cdfa281919f3175e739b6d56cf0
PR: #9

Assets

Asset	Size	SHA-256
jackal-v1.7.2-macos-arm64.tar.gz	158,210,905 bytes	6b5f09eb82aa4257dda3e4dca09eed1b6f8b8834b19a4d852e50dd8250f04518
jackal-v1.7.2-evidence.tar.gz	45,471 bytes	7d486de9a242e305f06d33e798ca241a2be11bf399c761502f71406f8f635ffb
jackal-v1.7.2-release-receipt.json	9,386 bytes	1f3425b1fadc3d8a791ba358b797964eb2386400339be1d6b18fafcce2fadddf
SHA256SUMS	—	12ce8d4a60b69cf38667973c9277c7d22db445e2bece284781f995357e04b019

Package internals (v1.7.2 macOS arm64):

• files = 79
• SHA256SUMS root = 328121533382ed9b9d3e58315bb90e867ea4c24e0520b18c3268f7f8e27b9300
• MANIFEST.sha256 = b8927e72606ca103f1b5eb39b2da2a0a7306047d8365b55001bb15fdb252c149

First-run verification

shasum -a 256 -c SHA256SUMS
tar -xzf jackal-v1.7.2-macos-arm64.tar.gz
cd jackal-v1.7.2-macos-arm64
shasum -a 256 -c SHA256SUMS
./plugin/hermes/jackal_hermes selftest

Load-bearing pinned identities

• Anubis compiler a733565f237df171e7cf93b9b37700a42d8713576818fd92f8cd23a8ad7a69e2
• jackal-native evaluator 20b80827d3c5c2a5d0d5d6f5a84c692f230fb0f55b9c7d1fcad02a1d0b3a1083
• current range checker f7a82524d082b51a8d66f9bed653b9c8da51b5424386659c9048b9c0ae276545
• current int checker f8347cbd18d520852aff56920d41f5e5b496ff192f584e41d84d1a818ff29617
• archival range checker 05c3518b836f239712f897c483a2ddadad9f544e0887b1b7bb1424a27289de8a
• archival range inventory 18ff7b1d428dbc6f807fd4de27751ba415b33ef0b356088d7fa316ed74bb0ba6
• revoked v1.7.0 int checker c858e3bfc0ff2809a808170caabbf090077cb54996e76f065dbcd26ffb067d49 (deliberately absent from package)

Aggregate evidence

Local aggregate: python3.11 release/tools/run_gates_v172.py → GATES: PASS (68 gates) in ~44 min.

Hosted CI on the PR head commit 9a81b4c…:

• Gaussian/range source closures and axiom audits — pass
• claim-kernel admission and surface locks (engine-free) — pass
• macOS arm64 plugin gates — pass

Non-claims (unchanged)

• Apple-Silicon macOS only; unsigned, not notarized.
• No universal correctness, source-to-native refinement, input-truth,
  operating-system, or authenticated-builder claim.
• Archived v1 range identity replay requires the exact historical
  checker AND historical coverage inventory bytes; reversed intervals
  refuse.
• Archived v1 composed-integral identity is historical revocation
  evidence only; request-unbound checker is not shipped or admitted;
  every v1.7.0 int-certificate receipt refuses formal replay.

JACKAL v1.7.0 — Certified bound_step Composition

JACKAL v1.7.0 — Certified bound_step Composition

Ledger roadmap item (4) — composing bound_step's acceptance policy over
runs_encloses + the Taylor bridges — is closed for the certificate lane
and shipped as a public proof-carrying tool. This release completes the arc
from the shadow mechanization (PR #3, deliberately non-authoritative) to the
public surface (PR #6), and fixes issue #4.

The new certified lane

./jackal-int-cert-release "sin(x)" 0 1 1/100 receipt.json
# status=formal-bounded enclosure=[…] theorem=int_cert_sound … receipt_reverified=true

• Theorem int_cert_sound (JackalIv.IntCert, Lean 4 + Mathlib): an
  artifact accepted by the proved computable checker yields a genuine
  enclosure of the exact integral of the reconstructed integrand over the
  requested interval, under the named TreeTCB (a Prop hypothesis — never
  an axiom — vacuous on the pure-rational fragment). Axioms: exactly
  [propext, Classical.choice, Quot.sound].
• Fourth pinned checker executable jackal_int_cert_check
  (c858e3bfc0ff2809a808170caabbf090077cb54996e76f065dbcd26ffb067d49),
  compiled from the proved parseIntCert + checkIntCert — no
  native_decide, no @[implemented_by] on the path. The lakefile edit
  re-pinned both existing proof identities; the range and gaussian checker
  binaries reproduced byte-identical (05c3518b…, ccac690b…).
• Untrusted producer tools/int_cert_producer.py (b4240fda…): an
  identity-pinned exact-rational mirror of the shipped bound_step
  (float midpoints, exact-ℚ acceptance, budget 60000, depth 60) emitting
  jackal-int-cert v1 subdivision-tree artifacts whose leaves embed ordinary
  jackal-eval-cert v2 certificates. Same architecture as the seven *_rat
  lanes: trust lives ONLY in checker acceptance.
• Fail-closed release binding: request commitment
  (jackal-req-v3-int-cert), producer/checker identity pins with TOCTOU
  stability, checker-echo enclosure binding, formal-status derivation against
  the digest-bound coverage inventory, receipt variant int_cert, and
  independent re-verification before success.
• Plugin surface: 33 → 34 tools — jackal_integrate_bound_cert, plus
  jackal_verify_receipt int_cert mode (expected_tolerance required). The
  weaker float lane integrate-bound / jackal_integrate_bound remains
  bounded/CONDITIONAL and never inherits formal language.

Issue #4 fixed — rat approx= presentation

approx= is now a rendering of the final normalized exact rational
(exact long division to ≥30 significant digits + one correctly-rounded
decimal→f64 parse), never an independently computed float path. Algebraically
equivalent inputs print identical decimals by construction; the verified
repro is pinned as a black-box regression pair. Presentation layer only —
certified lanes, the exact engine, and the checkers are untouched. The
evaluator was rebuilt with the pinned Anubis compiler after the baseline
rebuild of the unmodified source reproduced the v1.6.0 binary 8617ad08…
byte-identically (instrument validated first).

Migration (33 → 34)

Additive only: every v1.6.0 tool, schema, receipt format, and CLI command is
byte-compatible (mechanically locked: COMPAT_FLOOR_PASS frozen_tools=31 live_tools=34). Users of jackal_integrate_bound who need a proof-carrying
enclosure should call jackal_integrate_bound_cert (certified fragment:
num/var/neg/add/sub/mul/div/pow(0..4096)/sin/cos/abs in x; everything
else refuses). Full guidance: release/claim/MIGRATION-v1.7.0.md.
rat approx= semantics changed from "independent f64 evaluation of the
input" to "rendering of exact=" — the honest independent-float lane
remains eval.

Gates

Local sealed aggregate (Apple Silicon):
python3 release/tools/run_gates_v170.py → GATES: PASS (43 gates)
(full log in the evidence asset, sha256
cb614ff388df65b3bb42639e1ae491c808c8c73ace12645ee40b774668bc9caa):

• black-box 202/202 (incl. the issue-#4 regression pair); parser
  differential 78/78
• int-cert matrix 31/31 (6 positive, 7 refusal, 18 semantic poisons)
  against the compiled checker
• int-cert A→B→A: the tolerance guard is load-bearing (poison admitted
  under the mutated, rebuilt checker; original bytes restored hash-verified);
  the enclosure guards are proof-load-bearing — disabling them does not
  compile (int_cert_sound consumes them)
• engine differential 5/5: mpmath 60-dps oracle inside BOTH the engine's
  float enclosure and the certified enclosure
• claim gates: hostile 108/108, package parity 49/49 over this package,
  evidence determinism, frozen v1.6.0 claim fixture replays green
• package double-build byte-identical

Hosted CI (PR #6): Lean source closures + proof-identity/axiom audits for
all three lanes (now incl. int-cert, --proof-only) and the engine-free
34-tool/compat-floor/claim-admission job — all green.

Assets

asset	sha256	bytes
jackal-v1.7.0-macos-arm64.tar.gz	21c7ede586f30a58772f321f7dbb36ab66213e199785489f99133710ac56096e	118862060
jackal-v1.7.0-release-receipt.json	9474b801757b4833597702f60404c2c7f1acbca47a6a2552d0581a9f9922e06b	7354
jackal-v1.7.0-evidence.tar.gz	a62b86c91be50fff423f13d7b662865272a413a08aae2962ac1738d31d647ee2	3965
SHA256SUMS	—	296

Residual non-claims

• Producer fidelity to the shipped engine's bound_step control flow is
  differential-tested, never proved; certified derivative chains are
  Lean's D (no simplify_bound interleave — integer-power integrands may
  refuse taylor4 through 0-crossing domains; fail closed, never unsound).
• Source→native refinement (roadmap item 5) remains OPEN — the last
  bridge.
• Claim-bundle formal-receipt evidence replay stays pinned to the range
  lane; gaussian and int_cert receipts verify directly via
  jackal_verify_receipt, not yet inside bundles (SPEC §6/§12).
• The engine's float integrate-bound lane remains
  implementation-tested-not-mechanized.
• SHA-256 identifies bytes; it does not authenticate an author. The artifact
  is unsigned and has not received an independent external proof audit.

JACKAL v1.6.0 — Mathematical Evidence Kernel

JACKAL v1.6.0 — Mathematical Evidence Kernel

JACKAL is now a deterministic, offline mathematical evidence kernel: an epistemic claim compiler whose every answer carries its assurance class (exact / checked / estimated / bounded / formal-bounded / model-based) — or a named refusal.

Tool inventory: 33

• 31 legacy v1.5.0 tools, unchanged — names, parameters, return/status meanings, and accepted legacy evidence are mechanically locked by release/compat/v150_floor.json + tools/compat_floor.py --check (additive-only floor; COMPAT_FLOOR_PASS frozen_tools=31 live_tools=33 errors=0).
• 2 new claim-kernel front doors:
  • jackal_claim — compiles a typed claim request into a content-addressed jackal-claim-bundle-v1 evidence graph (15 registered inference rules; multidimensional assurance axes propagated by pointwise meet; consequence-class floors; deterministic rendering — never a bare VERIFIED).
  • jackal_verify_bundle — independent, dependency-light, caller-pinned replay: recomputes every hash, rule application, assurance axis, floor, and rendering; producer-authored statuses/digests are never accepted merely because they are present.

Compatibility

Migrating from a v1.4.2 (10-tool) or v1.5.0 (31-tool) epoch: both surfaces are strict subsets of the 33-tool surface; previously emitted formal receipts keep verifying under their original expected epoch/request. See release/claim/MIGRATION-v1.6.0.md. Hermes callers need a new session after upgrading.

Evidence (local full aggregate, Apple Silicon macOS)

release/tools/run_gates_v160.py on the exact release bytes: GATES: PASS (38 gates) — including lake-build (Lean proof closures), black-box acceptance 200/200, claim hostile matrix 108/108, claim A→B→A tamper gates over 7 trust layers, receipt-semantic mutations 42/42, and claim-package parity 47/47 (all 33 tools exercised from the fresh-extracted package). Full per-gate log: jackal-v1.6.0-evidence.tar.gz (sha256 b568b728e72468b6cc1fb09196add5123f4ce58f47bd751eca51148f4961eb5f).

Hosted CI (scope stated exactly)

The Formal proof identity gate workflow ran green on the exact PR head (5773931, runs 31980005167 / 31980003007) and the exact merge commit (19b763e, run 31980165734): Lean source closures + proof-identity/axiom audits (--proof-only) and the engine-free claim-kernel admission job (mechanical 33-tool lock, compat floor, committed-fixture replay to verified, one semantic tamper refusing node-id-mismatch). Hosted CI does not run the macOS engine or the full 38-gate aggregate; those are local sealed evidence above.

Package

• jackal-v1.6.0-macos-arm64.tar.gz — sha256 0cdacf56bb83d65454330973280cde7da0b9262d6163ccd7efbbbb47bc88e39a, 79,519,523 bytes, two consecutive builds byte-identical (deterministic USTAR + fixed mtimes).
• Apple Silicon macOS only; no cross-platform native execution is claimed.
• Verify: shasum -a 256 -c SHA256SUMS, then inside the extracted package shasum -a 256 -c SHA256SUMS again (packaged checksums), ./jackal-native self-test (104/104).
• JACKAL execution is local/offline after download; no first-call network fetch.

Security / TCB boundary (non-claims preserved)

No source→native formal refinement; no end-to-end formally verified executable; no one-time replay prevention without an external nonce store; no claim that supplied inputs are true in the world; no probabilistic confidence from intervals; no universal soundness outside admitted fragments; composed interval graphs remain bounded; SHA-256 identifies exact bytes only; finite hostile campaigns are strong bounded evidence, not universal theorems.

Install / migrate

GETTING-STARTED.md (install + first commands) · release/claim/MIGRATION-v1.6.0.md (epoch migration) · release/claim/SPEC.md (claim-kernel data model + assurance matrix §4) · PROVENANCE.md (full seal, frozen identities, hosted-CI scope).

The Hermes plugin epoch derived from this exact release is published separately at AnubisQuantumCipher/hermes-jackal-verified; the trust chain is acyclic (core release → package hash → plugin commit).

JACKAL CALC v1.2.0 — formal receipts and Hermes plugin closure

JACKAL CALC v1.2.0 — formal receipts and Hermes plugin closure

Public, unsigned/ad-hoc macOS arm64 release. This epoch binds the declared formal fragment end-to-end through the shared release validator, canonical embedded-certificate receipt, independent checker-reexecuting verifier, fresh-extractable release package, and Hermes plugin surface.

Identities

• Source/tag commit: cc533906182c887a8617cc741b91b926bcb41e22
• Archive: jackal-v1.2.0-macos-arm64.tar.gz
• Archive SHA-256: 3b63e86bd9d2cffafa33dde813c40919cc754343db2232b1c33072a3ec41e0a7
• Archive bytes: 39929946
• Package SHA256SUMS root: 24be9624027b994b6942b82a5a9cbe4acc5af2b2708e7d7a2e2652961b2d45b5
• Evaluator SHA-256: 820c0722e46a0800115c404ea1c9251c6f72fe8c6897bdabe437f342f9310b6c
• Proved checker SHA-256: 2186b43f8e45b7b3e55e189d64e92f15999664f5194caed929d14b29b006f59b
• Anubis source SHA-256: 5d43df8de01adb86bb10a0a6cea28fb79faf03cd58be51654c3fa88c653e4a40
• Hermes bundle SHA-256: daf4e5aa37ab40f16dcd2891aecbd4a81839e351a889323d72eb038098ed93bf

Green gates

• Lean build: 8,679 jobs; flagship theorem axioms [propext, Classical.choice, Quot.sound]
• Positive corpus: 20/20 formal-bounded, all 18 formal operator families covered
• Negative controls: 30/30 refused at the intended boundary
• Hermes plugin smoke: 8 gate groups / 20 evidence rows
• Eleven-category A→B→A: 11/11 gates load-bearing and hash-restored
• Fail-closed sweep: 21/21 wrapper/plugin/verifier poisons refused; no formal-* leak
• Fresh-extraction package: checksum, formal receipt, independent re-verification, plugin call, and refusal controls passed
• Determinism: negative-control evidence is stable across repeated runs; two consecutive package builds were byte-identical

What changed

• Added jackal-formal-receipt-v1 with canonical request framing, embedded certificate bytes, theorem/axiom/coverage metadata, evaluator/checker/plugin identities, assumptions, non-claims, and outer digest.
• Added tools/receipt_verify.py; it rehydrates the exact certificate and re-runs the pinned Lean-proved checker. Recomputing the outer digest cannot launder semantic tampering.
• Added the plugin/hermes stdio/one-shot/HTTP adapter for jackal_range_bound and jackal_verify_receipt, with deterministic bundle hashing pinned in release/MANIFEST.sha256.
• Added permanent plugin, mutation, and fail-closed evidence plus a deterministic fresh-extraction package recipe.

Claim boundary

formal-bounded means: for every checker-accepted request in the declared certified fragment, the accepted certificate implies a Runs derivation and therefore a true enclosure under the recorded ModelTCB. Unsupported strong requests—including exp, sqrt, logarithms, non-integer or negative powers, and %—refuse without a weaker fallback.

This release does not claim unrestricted universal correctness, transcendental coverage beyond the declared fragment, bound_step composition, Anubis source-to-native refinement as a theorem, Apple Developer ID signing/notarization, or authorship authentication from SHA-256 alone.

JACKAL CALC v1.1.1 — immutable public package identity repair

JACKAL CALC v1.1.1 — immutable public package identity repair

Public, unsigned/ad-hoc macOS arm64 release. This epoch preserves the v1.1.0 formal-status implementation, evaluator, proved checker, theorem set, and certificate schema while binding corrected v1.1.1 / public labels to a new tag and archive digest.

Identities

• Source/tag commit: fd1ac8584e463a2ace3c32cfdc6b6a4a77851087
• Archive: jackal-v1.1.1-macos-arm64.tar.gz
• Archive SHA-256: 8ed047183bdd6259fc3d9b22ab87003389eabf9c4da1722024848c016fc4ec09
• Archive bytes: 39912160
• Package SHA256SUMS root: 27c7802da06103b774736ac866344559437d6028cbd2cb57219e26360c002520
• Evaluator: 820c0722e46a0800115c404ea1c9251c6f72fe8c6897bdabe437f342f9310b6c
• Proved checker: 2186b43f8e45b7b3e55e189d64e92f15999664f5194caed929d14b29b006f59b

The archive was built twice from identical inputs and compared byte-for-byte. All 15 internal files passed SHA256SUMS; seven fresh-extraction positive/refusal smokes passed. The evaluator and checker are unchanged from v1.1.0.

Historical scar

The original v1.1.0 package carried stale v1.0.4/private text and was temporarily replaced in place during repair. v1.1.0 has been restored to its original 95588591… identity. v1.1.1 is the corrected immutable successor.

Claim boundary

formal-bounded means a checker-accepted, Runs-derived enclosure of the exact request over the modeled fragment, under the recorded ModelTCB. It does not claim universal correctness, unsupported transcendental operators, bound_step composition, Anubis source-to-native refinement, emitter faithfulness as a theorem, Apple Developer ID signing/notarization, or authorship authentication by SHA-256.

JACKAL CALC v1.1.0 — formal-status epoch

JACKAL CALC v1.1.0 — formal-status epoch

Public, unsigned/ad-hoc macOS arm64 release. This historical epoch introduced the formal coverage inventory and canonical formal-status gate on top of v1.0.4 release bindings.

Immutable identity restored

• Tag commit: d306aed473359362f6333716f806a465bb9cf1b1
• Archive SHA-256: 95588591d4a17e687b9b870d15920c834276059058d38726d1d48640bbbb3c56
• Archive bytes: 40355304
• Evaluator: 820c0722e46a0800115c404ea1c9251c6f72fe8c6897bdabe437f342f9310b6c
• Proved checker: 2186b43f8e45b7b3e55e189d64e92f15999664f5194caed929d14b29b006f59b

The archive contains stale v1.0.4/private label text. That defect is preserved rather than silently rewriting this predecessor again. The corrected public package is v1.1.1.

Claim boundary

formal-bounded remains conditional on the recorded ModelTCB and admitted operator fragment. No universal correctness, source-to-native refinement, unsupported transcendental coverage, Apple signing/notarization, or authorship authentication by SHA-256 is claimed.