{"id":"c4f5bba8-038f-496f-9e57-e9745359db5e","arxiv_id":"2502.05280","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"A formal smart contract model for cross-chain protocols is introduced, and a two-party atomic swap is shown to meet liveness, safety, and coalition Nash equilibrium.","lead":"The paper defines a formal \"smart contract model\" for cross-chain blockchain protocols, treating parties as potentially Byzantine and contracts as trusted state machines, with correctness expressed through game-theoretic conditions. It then analyzes a two-party asset swap and proves that the swap satisfies the proposed liveness, safety, and coalition Nash equilibrium properties.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The §5.3 proofs verify the stipulated map Ξ, not the automaton-defined protocol: no formal rule connects interface-automaton executions to the asserted outcome sets.","rationale":"The reader's weakest-assumption analysis identifies the same load-bearing concern: the proofs in Section 5.3 reason about the stipulated execution function Ξ, not about the interface-automaton composition that Section 4.3 calls the protocol. I see no reason to move away from the conditional verdict. The paper's definitions are coherent enough as a proposed abstract model, and the two-party swap is a known hash-time-lock protocol whose intended behavior is clear, so the gap is repairable: one can add a formal definition of compliance sets over automaton executions and a proof or mechanical check that Ξ equals the reachable terminal-state projection. Until that is done, the case-study verification is circular relative to the model, because Ξ is both part of the protocol definition and the sole basis for the correctness lemmas. I did not find a separate, stronger objection: the model's game-theoretic correctness conditions are reasonable, the swap example is appropriate, and the remaining notational corruption in the output vectors and utility equation does not change the substantive issue. The concrete test—exhaustive reachability of the automaton versus Ξ—would settle whether the concern lands; if it lands, the proofs must be revised, not merely the exposition.","tokens_in":13218,"tokens_out":2650,"duration_ms":30471,"concrete_test":"Formalize the Section 5.2 protocol as four interface automata (Alice, Bob, CA, CB) with the escrow, timeout, and hash-revelation transitions described in steps 1–4, and exhaustively compute the reachable terminal contract-state vectors for each compliance set Q, especially Q={A}, Q={B}, and Q={A,B}. Then compare these reachable sets exactly against the Ξ values in equations (6)–(8). If any reachable terminal vector is missing from Ξ(Q) or any listed vector is unreachable, then Lemmas 2 and 3 do not apply to the protocol as defined; if the sets match, the gap is expository and the conditional verdict stands.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim that the two-party swap protocol is correct rests on Lemmas 1, 2, and 3 of Section 5.3, and each proof is direct case analysis over the execution function Ξ: liveness uses Ξ({A,B}) = swapped outcome, safety enumerates Ξ({A}) and Ξ({B}), and coalition Nash equilibrium compares the same sets. But Ξ is introduced in Section 4.3 as an unconstrained component of the protocol tuple, and Section 5.2 defines it by fiat: 'we can restrict the execution function to its compliance set argument alone.' Nothing in the paper proves that the terminal states of the interface-automaton product—which Section 4.3 identifies as 'the protocol itself'—coincide with these Ξ sets. Moreover, the formal model gives no rule for what a compliance set Q means for the automaton composition; Q is a parameter of Ξ, not a property of an execution fragment. Consequently, Lemmas 1–3 establish properties of an asserted outcome list, not of the protocol as defined by the automaton model. If the reachable outcomes of the actual automaton differ from the enumerated Ξ values, safety or coalition equilibrium could fail even though the lemmas hold for the stipulated list. This is an internal gap in the correctness argument, not a disagreement with external consensus.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces a formal model, called the smart contract model, for cross-chain protocols in which parties (some possibly Byzantine) interact through trusted smart contracts on distinct ledgers. Parties and contracts are modeled as interface automata; a task is defined by input party vectors, input contract state vectors, output contract state vectors, and a utility function; a protocol is defined by a tuple (IP, IC, OC, Ξ), where Ξ is an execution function mapping inputs and a compliance set to a set of possible output contract states. Correctness of a protocol is defined by coalition Nash equilibrium, liveness, and safety, all formulated in terms of Ξ. The paper then presents a two-party cross-chain swap protocol, specifies Ξ for it, and claims in Lemmas 1–3 that it satisfies liveness, safety, and coalition Nash equilibrium. The central claim is that this swap protocol is correct under the proposed model.","tokens_in":13479,"tokens_out":6149,"duration_ms":58784,"significance":"If the formal connection between the execution function Ξ and the automaton semantics were established, the model would provide a useful abstraction that adapts classical distributed-computing concepts (interface automata, tasks, protocols) to blockchain-based cross-chain settings while incorporating game-theoretic correctness conditions. The related work is broad and the two-party swap case study is well motivated. However, as it stands, the paper does not deliver a rigorous correctness proof of the swap protocol, because the proofs in Section 5.3 verify a stipulated outcome map rather than the automaton-defined protocol. This gap is internal and fixable, but it undermines the central claim; the paper therefore requires substantial revision before the stated results can be accepted.","major_comments":[{"comment":"The correctness conditions (coalition Nash equilibrium, liveness, safety) are stated exclusively over the execution function Ξ, but the protocol is identified with the composed interface automaton. No formal rule is given that maps execution fragments of the automaton product to the output sets Ξ(IP, IC, Q); in particular, the paper never proves that the terminal states of the automaton product coincide with the enumerated Ξ sets. Lemmas 1–3 of Section 5.3 are direct case analyses over the hand-defined Ξ (Lemma 1 uses Ξ(P) = swapped outcome, Lemma 2 enumerates Ξ({A}) and Ξ({B}), and Lemma 3 compares utility values on those same sets). Consequently, the lemmas establish properties of an asserted outcome list, not of the protocol as an automaton. If the automaton's reachable outcomes differ from the listed Ξ values, safety or coalition equilibrium could fail even though the lemmas hold. This is the load-bearing gap in the correctness argument.","section":"Section 4.3, 5.3"},{"comment":"The composition operation is defined only for two composable interface automata, IA_P ⊗ C, with composability conditions involving one party and one contract. The interface automaton of a cross-chain system is then asserted to be the composition 'as proposed by Alfaro and Henzinger' without specifying how the pairwise product extends to m parties and n contracts, how multiple parties sharing actions with the same contract are handled, or how the product state space and transitions are formed. Since the swap protocol of Section 5 involves two parties and two contracts, the existence and semantics of the claimed composed automaton are not formally established. The paper should either define the general composition operation or instantiate the pairwise products for the case study and prove the required properties for that specific automaton.","section":"Section 4.1"},{"comment":"The execution function Ξ for the swap protocol is stipulated by fiat ('we can restrict the execution function to its compliance set argument alone'), and the informal protocol steps (escrow, claim, refund) are never translated into interface automata. The proofs of Lemmas 1–3 therefore verify the utility properties of the chosen Ξ (Equation 6 and the bullet lists in Section 5.2), not that the described protocol actually realizes those outcome sets. Because Ξ is a component of the protocol tuple, the correctness claim risks being tautological: one could choose Ξ to satisfy the three conditions for any desired outcome list regardless of what the automaton does. The revision must define the automaton for the swap protocol and prove that its reachable terminal outcomes are exactly the sets listed for Ξ, or alternatively restate the correctness conditions directly over automaton executions.","section":"Section 5.2, 5.3"}],"minor_comments":[{"comment":"In the first paragraph, 'The contacts receive messages' should be 'The contracts receive messages'.","section":"Section 4.4"},{"comment":"In Step 3, 'If Alice observs that Bob has not escrowed' should be 'observes'; and 'If, b the end of this round' should be 'by the end of this round'.","section":"Section 5.2"},{"comment":"The output contract state vectors are typeset with symbols like '[֒→֒→A]' that are not legible in the provided PDF; readers cannot reliably match the four output vectors to the utility values in Equation (5), which complicates checking the case analysis in Section 5.3. Please use a clear ownership notation (e.g., listing for each asset which party owns it).","section":"Section 5.1, Equation (5)"},{"comment":"In the case 'If Bob alone is compliant' the set is written as Ξ({B}) = {[֒→֒→B], [֒→֒→B]}, where the two symbols appear identical; this should be corrected to the two distinct outcomes described in Section 5.2 (Alice fails to escrow a at Step 1, and Alice fails to claim b at Step 3).","section":"Section 5.3, Lemma 2"},{"comment":"Reference [38] spells 'equilbrium' for 'equilibrium' and cites a Wikipedia page for strong Nash equilibrium; a textbook or peer-reviewed survey reference would be more appropriate.","section":"References"},{"comment":"The figure '2swap.PNG' is listed in the arXiv metadata but is not cited or captioned in the text; it should be either integrated with a proper caption or removed.","section":"General"}],"recommendation":"major_revision","confidential_remarks":"The reader's report and stress-test note correctly identify the central problem: the correctness proofs in Section 5.3 verify the stipulated execution function Ξ, not the interface-automaton composition that Section 4.3 calls 'the protocol itself'. This is not a minor presentation issue; it is determinative for the paper's main claim. The paper is not acceptable in its current form, but the gap is addressable within the manuscript's scope: the authors should either define correctness directly over automaton executions or supply a formal semantics connecting Ξ to automaton executions, and then prove that the swap automaton actually realizes the claimed Ξ sets. The multi-party composition in Section 4.1 also needs a precise definition. If these revisions are made, the paper could be a solid contribution to formal models of cross-chain protocols."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper packages interface automata, utility-based tasks, and coalition Nash equilibrium into a single formal model for cross-chain protocols. That exact combination is new as far as I know, and the high-level idea is sound: contracts are trusted deterministic automata, parties are self-interested, and correctness is stated in game-theoretic terms. The two-party swap case study is a standard hash-time-lock swap, but it is cleanly expressed in the model. The paper also makes sensible simplifications (synchronous rounds, no direct contract-to-contract messaging) and is honest about the model's scope.\n\nThe main problem is the disconnect between the interface automaton composition and the execution function Xi. In Section 4.3, the protocol is formally a tuple that includes Xi, and correctness is defined as properties of Xi. In Section 5.2, Xi is given by flat enumeration of the possible outcomes per compliance set. The proofs of Lemmas 1–3 are then direct case analysis over that enumeration. Nothing in the paper shows that the terminal states of the interface automaton product coincide with the Xi sets, or even gives a rule for deriving Xi from the automaton executions. So the lemmas verify properties of an asserted outcome list, not of the protocol as defined by the automaton model. This is a load-bearing gap for the case study's correctness claim. It should be fixable: either define Xi from the automaton's reachable states, or prove that the automaton product terminates exactly in the enumerated outcomes.\n\nA second gap, related but separate, is that multi-party composition is never actually defined. The paper gives the binary product for two composable interface automata, then refers to Alfaro and Henzinger for the full system. That is fine for two parties and two contracts, but the model is supposed to handle m parties and n contracts, so an explicit n-ary composition rule is needed. There are also some notation typos (for example, the OC set in Section 5.1 seems to omit a separator between what is owned by A and what is owned by B), but those are minor.\n\nI agree with the conditional verdict. The model's ingredients are not new individually, but the packaged synthesis is useful and the paper is clearly written. The gaps are internal and repairable, not signs of a broken approach. I would send this to a serious referee with a request for major revision: the authors need to connect Xi to the automaton semantics, or reframe the correctness claims as properties of the automaton product itself. If that connection is supplied, the model could be a convenient common vocabulary for cross-chain protocol analysis. For now, I would not cite it in my own work, but I would not dismiss it either.","headline":"A useful synthesis of a cross-chain model with game-theoretic correctness, but the case-study proofs verify a stipulated outcome map rather than the automaton-defined protocol.","tokens_in":14001,"tokens_out":1924,"would_cite":false,"duration_ms":19740,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper proposes a smart contract model for cross-chain protocols in which correctness is coalition Nash equilibrium plus liveness plus safety, and proves that a two-party hash-timed swap satisfies all three conditions.","keywords":["smart contract model","cross-chain protocols","Byzantine parties","game theory","coalition Nash equilibrium","atomic swap","blockchain","distributed computing"],"falsifier":"Construct the composed interface automaton for the two-party swap and compute its reachable execution fragments; if any reachable outcome is missing from the paper's $\\Xi$ table, or any listed outcome is unreachable, then Lemmas 1, 2, and 3 do not apply to the protocol as formally defined. A concrete trace to look for: Bob is compliant while Alice deviates after escrowing $a$ but before claiming $b$, and Bob ends up with neither asset, which would violate safety if it is reachable.","tokens_in":13019,"feed_emoji":"🔄","tokens_out":6288,"duration_ms":62076,"temperature":0.7,"pith_summary":"The paper proposes a formal model of cross-chain protocols in which mutually distrusting parties interact only through trusted smart contracts on separate ledgers. It argues that correctness in this setting cannot be classical all-or-nothing atomicity, because a party can deviate in arbitrary ways, so tasks must be specified by a utility function over possible asset-transfer outcomes. A protocol is correct when it satisfies coalition Nash equilibrium, liveness, and safety: no coalition gains by deviating, full compliance achieves every party's preferred transfer, and no compliant party loses value. The paper demonstrates the model on a two-party hash-timed swap and proves the three correctness conditions for that protocol.","feed_headline":"Formal model proves two-party cross-chain swap safe and live","feed_subtitle":"Correctness needs no honest majority: no coalition gains by deviating and compliant parties never lose assets.","key_machinery":"The central object is the execution function $\\Xi : I_P \\times I_C \\times 2^{\\mathcal{P}} \\to 2^{O_C}$, which assigns to each input party vector, input contract vector, and compliance set $Q$ the set of possible output contract-state vectors. It stands in for the protocol's behavior so that correctness can be checked directly on outcomes rather than on individual automaton traces. The formal substrate is the product composition of interface automata, and the evaluation metric is the utility function $U$ defined on transitions. The two-party swap proof then works by case analysis over which party, Alice, Bob, both, or neither, is compliant, using the stipulated $\\Xi$ outcomes and the utility table.","core_discovery":"The central claim is that the smart contract model, with correct protocols defined by three game-theoretic conditions, captures cross-chain tasks and separates the roles of parties and contracts: parties propose, contracts dispose. The paper defines a cross-chain system as interface automata for parties and contracts, a task by input party vectors, input contract vectors, output contract vectors, and a utility function, and a protocol by an execution function $\\Xi$ mapping inputs and compliance sets to possible output contract states. Correctness is coalition Nash equilibrium plus liveness plus safety as formalized in Section 4.3. As evidence, the paper proves Lemmas 1, 2, and 3 for a two-party atomic swap, showing that when both comply the swap occurs and each party gains utility 1, and that no compliant party can be driven negative and no singleton coalition can profit by deviating.","pith_inferences":["A natural extension the paper leaves implicit is to derive $\\Xi$ algorithmically from the composed interface automata, for instance by reachable-state exploration, and then re-check the three conditions against that derived table rather than a hand-asserted one.","The coalition Nash condition is weaker than strong Nash equilibrium: it only requires that a coalition cannot increase its collective utility, so a deviating coalition member could individually lose while the coalition as a whole gains; this distinction matters for multi-party tasks but is not exercised by the two-party case study.","The model implicitly frames smart contracts as trusted third parties for fair exchange, so the well-known impossibility result for fair exchange without a trusted third party explains why contract-mediated protocols can solve tasks that purely peer-to-peer protocols cannot; the paper cites that result but does not develop the connection."],"forward_implications":["If the model is right, cross-chain protocols can be analyzed without assuming an honest majority; the working assumption is only that at least one party is compliant.","Correctness can be checked by finite case analysis over compliance sets for small protocols, making the three conditions a practical design template for new cross-chain tasks.","The formal swap proof gives a baseline for expressing other tasks in the model, such as auctions, loans, options, and multi-party swaps, as the paper itself notes.","Because contracts, not parties, decide executed transfers, Byzantine behavior of parties is contained at the contract boundary, which is the key structural difference from classical distributed computing models."],"supporting_citations":[{"why":"Defines interface automata and the product composition used to model parties and contracts.","marker":"[1]"},{"why":"Introduces the atomic cross-chain swap problem and the hash-timed escrow pattern that the case study implements.","marker":"[23]"},{"why":"Provides the cut-and-choose atomic swap protocol whose steps Section 5.2 formalizes.","marker":"[28]"},{"why":"Establishes the impossibility of fair exchange without a trusted third party, motivating contracts as trusted intermediaries.","marker":"[30]"},{"why":"Supplies a game-theoretic robustness framework whose coalition equilibrium notion the model adapts for cross-chain protocols.","marker":"[41]"}],"fun_headline_variants":["Cross-chain swap safety proven via game-theoretic model","No honest majority needed for safe atomic swaps","Smart contract model guarantees swap fairness formally","Game-theoretic contracts make cross-chain swaps safe"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing assumption is that the hand-written outcome table in Section 5.2 faithfully describes everything the composed contracts and parties can actually do; the paper does not derive that table from the formal automaton definitions.","fun_headline_variants_meta":{"raw":{"variants":["Cross-chain swap safety proven via game-theoretic model","No honest majority needed for safe atomic swaps","Smart contract model guarantees swap fairness formally","Game-theoretic contracts make cross-chain swaps safe"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000148,"raw_usage":{"total_tokens":1166,"prompt_tokens":901,"completion_tokens":265,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":517,"completion_tokens_details":{"reasoning_tokens":208}},"tokens_in":517,"tokens_out":265,"duration_ms":3504,"temperature":1.0,"reasoning_tokens":208,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-08T19:55:17.903582+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Construct the composed interface automaton for the two-party swap and compute its reachable execution fragments; if any reachable outcome is missing from the paper's $\\Xi$ table, or any listed outcome is unreachable, then Lemmas 1, 2, and 3 do not apply to the protocol as formally defined. A concrete trace to look for: Bob is compliant while Alice deviates after escrowing $a$ but before claiming $b$, and Bob ends up with neither asset, which would violate safety if it is reachable.","supporting_citations":[{"cited_title":"In: T joa, A.M., Gruhn, V","cited_arxiv_id":null,"evidence_quote":"Defines interface automata and the product composition used to model parties and contracts."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the cut-and-choose atomic swap protocol whose steps Section 5.2 formalizes."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Establishes the impossibility of fair exchange without a trusted third party, motivating contracts as trusted intermediaries."},{"cited_title":"In: Gilbert, S","cited_arxiv_id":null,"evidence_quote":"Supplies a game-theoretic robustness framework whose coalition equilibrium notion the model adapts for cross-chain protocols."}],"review_version":1}