Stiff 0.4.0

Stiff 0.4.0 adds pure HTTP contracts and a proven two-account ledger example, pinned to Bend 2.0.35.

• Compiler-checked route laws cover selected protected routes, complete modeled GET/HEAD state preservation, and 404/405 decisions. Applications can prove their declared statuses and response bodies.
• Ledger laws cover conservation, overdraft rejection, unchanged rejection and idempotency. Twelve ordinarily typechecked mistakes fail the proof gate before any mutant binary is built. Fifteen native ledger journeys passed.
• Fresh consumer setup runs in CI; load and shutdown timing checks tolerate scheduler stalls while retaining arrival accounting and deadline checks.
• Native example archives are available for macOS arm64 and Linux x64/arm64. Linux builds run on hosted Ubuntu 24.04 runners. Each exact archive passed provenance/checksum checks, supervised application health, create/read/restart checks and all six persistent notes journeys with no build tools on PATH.

BendHub package: 0x4ee0ec16258e9b8ad6ef37e5b8c4f95e. Empty-cache verification matched all 20 published files, required ALL PROOFS CHECK, exercised authenticated HTTPS and passed six persistent application journeys. The copied hub client passed HTTPS and cached-source tamper rejection. Consumer source/build-tool pins name be078621ad69303546de258fd8db578fc8c9b0f6; the tagged library and native build sources match that anchor.

The archives contain app, notes, stiff-run, deployment examples, licenses, dependency provenance and SHA-256 checksums. They dynamically require libcurl, json-c and SQLite; patched libevent 2.2.2-alpha is included statically. They are platform-specific examples, not static executables.

Proofs cover pure modeled decisions. Credential validation, decoding, path matching, original receipt selection, serialization, SQLite integration, native effects, the compiler/runtime, dependencies and operating system remain trusted/tested. A modeled status law does not prove every socket response has that status. ALL PROOFS CHECK denotes compiler checking; this release verification does not repeat the ledger's earlier independent BendTT check or establish end-to-end verification or memory safety. The sanitizer profile retains its documented Clang calling-convention mitigation. Hard resident-memory isolation is a Linux cgroup contract. The ledger is a bounded demo, with no real authentication system or external payments. Local durable receipts do not establish distributed exactly-once behavior.

The local suite ran 147 tests: 145 passed, fresh setup was skipped, and the RSS benchmark failed because the sandbox blocks /bin/ps. Hosted CI supplies the full-suite result. Historical workload measurements are not new 0.4.0 capacity measurements. Release evidence records exact revisions and separate verification scopes.

Release source: 945e73b4fd2a2b3b25e41fa696f3b908b7677e7e. Pinned CI passed all eight Linux/macOS platform/profile jobs. Final Linux archive workflow built and verified both Linux assets; workflow rehearsal passed before release use.