This work presents a formal, state-machine-based treatment of protocol-level quantum safety in Bitcoin under quantum polynomial-time (QPT) adversaries. We model Bitcoin as a deterministic state transition system over the UTXO set and define authorization as a game-based property. We introduce a set of invariants including authorization integrity, no double-spend, and deterministic validation, and formally prove their preservation under valid state transitions. We provide a reduction showing that any unauthorized spend implies either a break of EUF-CMA security of the signature scheme or a violation of hash-based binding properties, in both the classical and quantum random oracle model (QROM), without relying on oracle reprogramming or rewinding techniques. The model explicitly incorporates adversarial network conditions, including mempool observation, transaction reordering, and chain reorganizations, and proves that such capabilities do not enable unauthorized state transitions. We formalize a consensus-semantic equivalence relation over transactions via a normalization function, ensuring that validation and state transitions are invariant under representation-level differences. Additionally, we analyze identifier integrity under quantum collision search (BHT) and provide system-level bounds relative to the active UTXO set. Finally, we prove a no-free-migration result: under purely cryptographic authorization, no transformation of the current UTXO set can simultaneously preserve both safety (no unauthorized spend under quantum adversaries) and liveness (all coins remain spendable), making migration trade-offs unavoidable. This work aims to distinguish between localized constructions and system-wide security guarantees, and to provide a formal foundation for evaluating quantum safety claims at the protocol level.
Mayckon Giovani (Thu,) studied this question.