Assurance integration: bind model proofs to server, ABI and protocol conformance evidence #98

Follow-up from the requested four-repository adversarial audit: hyperpolymath/proven-cicd-and-workflows#77 and hyperpolymath/proven-tests-and-benches#103.

This is an integration work item, not a newly demonstrated server vulnerability. The repository's PROOF-NEEDS ledger does not establish a full current build/protocol proof. Pons and panic must not import a model proof as if it proved an Idris → Zig → C ABI → client-binding execution path.

First bounded acceptance slice:

• Select one protocol operation and state its preconditions, failure outcomes and observable postcondition.
• Bind model statement, proof/checker result, source commit and generated/binding digests in a versioned evidence envelope.
• Run positive, denied-transition and malformed/fragmented/coalesced-input conformance cases through the actual server and binding, with time/resource bounds.
• Retain counterexamples and mark unsupported commands and partial adapter coverage explicitly.
• Check that missing proof tools, mismatched source digests, replayed receipts and failed tests cannot become a passing assurance verdict.

The existing proven SafeOrdering law suite compiled and passed 8/8 at 53600326ca31f6f99767c5371cc77af2dade996c during the audit. That scoped result does not establish this repository's implementation correspondence. Neither a full proven-servers build nor its runtime paths were tested in this audit; leave those obligations open.