[h4x3rotab]

A Consul CAS request can outlive the bootstrap process that sent it. If that request wins against the restarted process, the old allocator advances without recognizing its own claim and can assign the same instance a second ordinal. Reread the same slot after a failed CAS and advance only after observing another owner. Use strongly consistent reads, propagate storage errors, and report exhaustion without waiting for permanent records to disappear.

Add Lean proofs for ordered admission-policy selection and allocation without slot reuse, Tamarin models for admission and shared-key signaling authentication, and finite slot-lifecycle models. Preserve the previous allocator as a failing regression control. Add deterministic Go regressions, concurrent-claim tests, pinned verification runners, CI, and a security claim ledger.

Add a separate timed model for Cloud API read retries. Check retry limits, Retry-After, cancellation, termination, and recovery with sufficient retry/time budgets. Controls reproduce the deployment failure without read retries and the failure caused by applying the HTTP timeout to the entire operation. The focused Go SDK client fix reuses the existing retry helper and is in Phala Cloud #535; this repository contains the specification and evidence.

Validation:

• The deterministic delayed-CAS regression failed against the previous allocator by assigning the same instance slots 0 and 1.
• go test -race -count=100 ./... and go vet ./... pass in components/bootstrap-secrets.
• 54 TLC expectations match, including expected counterexamples and reachability witnesses; 11 cover Cloud API read retry scenarios.
• Lean kernel-checks 161 authored declarations across the three specifications, with no placeholders or custom axioms.
• All 19 selected Tamarin outcomes match, including attack controls and documented trust-limit counterexamples.
• Checked-in evidence hashes match the current specifications, runners, and reviewed runtime files.
• The focused Go SDK fix passes its race-enabled suite and vet, a virtual-clock regression with a 60-second quota wait and 30-second HTTP timeout, and the Terraform provider's race-enabled throttled-read regression. The earlier live quota-injection test used a previous SDK revision.

The allocation theorem assumes an initially empty registry with permanent ownership records. Existing duplicates are not repaired automatically. Safe reuse/fencing, exclusive live ownership, per-member compromise resistance, authenticated instance binding, transport channel guarantees, and a project-wide composition theorem remain open. The retry model checks finite scenarios with explicit exchange times; permanent throttling cannot guarantee deployment success. These separate proofs do not establish complete project security or Go refinement. Current Terraform deployments use explicit ordinals and bypass dynamic allocation.