Skip to content

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

Choose a tag to compare

View all tags
@AnubisQuantumCipher AnubisQuantumCipher released this 15 Aug 06:21
· 183 commits to master since this release
v1.2.0
cc53390

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.

Assets 11
Loading