Formal Specification Verification of Settlement Protocols in Macroeconomic Dynamic Models: Auditing Fiscal Protocols via Mosler's Tax-Driven Production and the Genesis Model

This research article introduces Sequential Provenance Comparison (SPC), a formal audit method for evaluating the institutional executability of macroeconomic settlement protocols. The paper formalizes Warren Mosler’s tax-driven monetary circuit as a discrete-event system and examines the distinction between aggregate accounting identities and sequential settlement causality. Under an explicitly bounded, unassisted Genesis specification beginning from an all-zero balance state, the analysis shows that valid settlement paths satisfy a strict partial order in which tax impost precedes production activation, sovereign disbursement precedes tax settlement and bond settlement, and unassisted tax-first or bond-first sequences ABORT because the required commercial-bank deposits or central-bank reserves are absent. These results are explicitly limited to the specified institutional model and are not presented as a universal historical chronology. SPC extends this analysis by comparing alternative transaction Provenances, auditing Event preconditions, actor-level balances, transition rules, and invariants, and distinguishing between target settlement execution and the lifecycle closure of accommodation credit. It also links historical partial identification with forward reachability auditing, classifying projected macroeconomic paths as valid, under-specified, or unreachable. The broader methodological aim is to provide a formal verification layer between aggregate macroeconomic models and the institutional settlement processes required to implement them. SPC is designed to complement, rather than replace, existing macroeconomic modeling by making transaction order, settlement assets, and institutional constraints explicitly auditable. Note on Related Versions: This article is a substantially revised, generalized, and expanded English version of the author's Japanese manuscript: “マクロ経済動学モデルにおける決済プロトコルの形式仕様検証” (DOI: 10.5281/zenodo.22343357).