An EVM-Cosmos Bridge for Atomic, Semantic-Preserving Transfer of Environmental Tokens

An EVM–Cosmos Bridge for Atomic, Semantic-Preserving Transfer of Environmental Tokens Sebastian Pandolfi∗ , Guzmán Llambı́as∗† , Laura González∗ ∗ Facultad de Ingenierı́a, Universidad de la República, Montevideo, Uruguay

arXiv:2610.37663v1 [cs.SE] 27 Oct 2026

{sebastian.pandolfi, gllambi, lauragon}@fing.edu.uy † Pyxis Research, Pyxis, Montevideo, Uruguay guzman.llambias@pyxis.tech

Abstract—Transferring semantically typed tokens between heterogeneous blockchains—EVM and Cosmos ecosystems—raises two problems: semantic mixing, the loss of a token’s domainspecific meaning in transit (e.g., CO2 removals issued under different methodologies), and atomicity despite divergent consensus and timing assumptions. We propose a bridge that addresses both. A deterministic indicator identity derived from cryptographic commitments, mirrored in class registries on both chains and checked at mint time, preventing semantic mixing by construction. For atomicity, we extend hash time-locked contracts (HTLCs) from two-party exchange to single-owner transfer with an automatic callback that burns the source escrow after a destination claim, and a protocol-minimum bounty that makes the fallback burn incentive-compatible even against adversarial senders. We machine-check the protocol’s invariants with TLC— supply conservation fails without the rational-monitor assumption and holds with it—and validate a bidirectional prototype on Polygon and Neutron mainnets over Axelar GMP: fully automatic transfers with a median end-to-end latency of 97 s over 50 Polygon→Neutron transfers across 7 days (all completed by the on-chain automatic callback) and 93 s in the reverse direction, and semantic-validation overhead below 0.4% of messaging cost. We also document the integration failure modes of Cosmosoriginated messaging, whose dominant operational risk proves to be relay eligibility rather than latency. Index Terms—Blockchain interoperability, cross-chain bridge, semantic mixing, environmental indicators, HTLC, ERC-1155, Axelar GMP, EVM, Cosmos, CosmWasm

I. I NTRODUCTION The proliferation of blockchain networks has created a fragmented ecosystem in which assets and data remain siloed across distinct consensus mechanisms, execution environments, and communication protocols [1], [2]. Cross-chain interoperability has therefore emerged as critical infrastructure, while bridges have become prime attack targets: Zhang et al. document 35 attacks and ten vulnerability classes [3], and Chainalysis estimates $2B stolen across 13 bridge hacks in 2022 alone [4]. A particularly challenging case arises with domain-specific tokens—tokens whose units carry application-level meaning rather than being fully fungible. Pandolfi et al. [5] survey this challenge for environmental indicator tokens, the focus of

this paper. These tokens represent quantitative measurements of environmental impact such as CO2 removals, renewable energy generation, or treated-water volumes [6]. Unlike fully fungible assets, they have meaning: 1 kgCO2 e of carbon removal issued under Verra VM0007 is not interchangeable with one issued under Gold Standard GS-AFOLU, let alone with 1 kWh of energy. We call such tokens multi-class tokens: grouped into discrete classes that are fungible within a class and non-interchangeable across classes. Transferring them across architecturally dissimilar chains poses two problems. Problem 1 (Atomicity across heterogeneous chains). Domain-independent: any cross-chain transfer must avoid leaving tokens on both chains or on neither. Classical twophase commit [7] requires a trusted coordinator; HTLCs [8] provide a trustless alternative but suffer from a timeout race condition when relay latency stretches between heterogeneous ecosystems [9]. Problem 2 (Semantic mixing). A bridge treating all tokens as fungible merges distinct classes into a single balance: Verra- and Gold-Standard-issued CO2 bridged through a standard ERC-20 bridge arrive indistinguishable, with no way to recover methodology, registry, or vintage. The mechanism is documented at the application layer—Toucan’s Base Carbon Tonne (BCT) pool aggregated heterogeneous credits into one fungible ERC-20, creating a “lemons” market in which low-quality “zombie” credits displaced higher-integrity ones [10]. The cross-chain instance has not yet materialised at scale, but the BCT episode confirms the underlying dynamics; the bridge is the natural place to forestall it by design. To our knowledge, no existing cross-chain approach simultaneously addresses both problems for multi-class tokens across heterogeneous EVM–Cosmos environments [11], [1], [12], [13], [14], [15], [16]. We propose a bridge that combines relay-based messaging with an HTLC atomic-transfer protocol augmented by an automatic callback mechanism. After the destination claim reveals the secret, the destination contract emits a relayed message that burns the escrowed source tokens, closing the timeout-race window in a bounded delay rather than at Te ;

a bounty escrowed at lock time and paid to whoever finalises the source-side burn makes the fallback path incentivecompatible. While HTLCs have traditionally been used for atomic exchange (two-party swap), we adapt them to atomic transfer (single-owner burn-and-mint) and explicitly handle heterogeneous-chain timing. Semantic mixing is prevented by deriving a deterministic indicator identity from cryptographic commitments and mirroring a class registry on both chains, restricting destination mints to pre-registered classes. The five contributions, used as a comparison framework with related work (Table II), are: HTLC-based atomicity for cross-chain transfer (F1), automatic callback (F2), deterministic indicator identity (F3), cross-chain semantic-consistency enforcement (F4), and multi-class transfer with mirrored registry (F5). We instantiate the design as a bidirectional prototype using ERC-1155 tokens on Polygon and CosmWasm contracts on Neutron, with Axelar GMP as the relay. Mainnet evaluation demonstrates fully automatic transfers in both directions (108 s and 93 s in representative runs), characterizes latency over 50 transfers across 7 days, exercises the refund and monitorrecovery paths, and reports the integration failure modes encountered during deployment; semantic-validation overhead stays below 0.4% of cross-chain messaging cost. Sections II– VIII present background, related work, design, prototype, evaluation, discussion, and conclusions. II. BACKGROUND A. Cross-Chain Transactions, Relayers, and Bridges A cross-chain transaction spans independent ledgers; because no ledger natively observes another, an external relayer forwards messages, and the surrounding protocol is a bridge. Zamyatin et al. [11] systematise bridges as notary, relay/sidechain, and HTLC categories—not mutually exclusive; ours combines a relay scheme with HTLCs—and define the atomicity, consistency, and liveness properties we use throughout. Transfers reconcile supply via burn-and-mint (irreversible, supply-conserving; our choice) or custodial lockand-mint [11], [18]. Axelar [19] exemplifies a relay-scheme bridge: a proof-ofstake validator network verifies and forwards messages, exposing General Message Passing (GMP) on EVM and delivering to Cosmos destinations over IBC [20]. The EVM–Cosmos pair is heterogeneous in three ways that shape the protocol: (i) serialisation—EVM consumes ABI-encoded bytes, CosmWasm JSON, forcing an explicit encoding boundary (Section V); (ii) finality—probabilistic on the EVM side vs. instant BFT, forcing an asymmetric confirmation policy visible in the leg latencies (Section VI); and (iii) relayer infrastructure— EVM→Cosmos legs are delivered end-to-end by Axelar’s own relayer, whereas Cosmos-originated messages depend on public IBC relayers plus fee-incentivised executors, and must carry an explicit relayer fee in an Axelar-registered asset or they are routed but never executed (Section VI-D).

B. Hash Time-Locked Contracts and the Timeout Race Condition A hash time-locked contract (HTLC) [8] releases escrowed assets either on timely revelation of a preimage of a cryptographic hash or on expiration of a time bound. A sender escrows under hashlock H = hash(S) with deadline T ; the recipient claims by revealing S before T , else the sender refunds after T . HTLCs underpin the Lightning Network and were formalised by Herlihy [8] for atomic cross-chain swaps. Across two chains, an HTLC uses paired deadlines Te (source refund) and Tc (destination claim) with Tc < Te ; safety relies on the source chain learning of a destination claim before Te . Across heterogeneous chains this assumption is fragile: if the destination claim lands near Tc and secret propagation exceeds (Te − Tc ), a malicious user can claim on the destination and still refund on the source—the timeout race condition, documented in security surveys [3], [21] and addressed cryptographically only for swap protocols [9]. Twophase commit [7] removes the race via a trusted coordinator, the single point of trust bridges seek to avoid. C. Environmental Indicator Tokens Environmental indicator tokens represent quantitative environmental measurements—tonnes of CO2 removed, kilowatthours generated, litres of water treated [5], [6]. Each class carries metadata (indicator type, canonical unit, issuance methodology, and cryptographic commitments to a profile document and evidence bundle), and fungibility holds only within a class: methodologies differ in additionality, monitoring, and verification stringency [6], [5], and differing units are non-interchangeable a fortiori. The BCT episode of Section I shows the consequence of collapsing this structure— and Toucan’s reactive countermeasures (gating, redemption fees) show why prevention-by-design beats ex-post remediation [10]. The ERC-1155 multi-token standard [22] represents non-interchangeable classes within one contract via distinct tokenId values; our design uses ERC-1155 on the source and a mirrored registry on the destination (Section IV). D. System Model and Assumptions The protocol’s safety claims rest on six assumptions. A1 (cryptographic strength): keccak256 is collision- and second-preimage-resistant on 32-byte inputs. A2 (consensus safety): each chain produces a single canonical history once finality is reached; the source-chain finality is enforced by the relay’s confirmation policy (Section VI). A3 (forwardrelay liveness): the relay delivers the prepare message to the destination at least once within Te ; A2+A3 ensure that an initiated transfer can always be either claimed or refunded. A4 (rational-monitor callback safety): if the callback fails, safety requires at least one party with knowledge of S to invoke claimBurn on the source chain before Te (Section VII-B); the capable set is unbounded in principle, and the protocol escrows a bounty of at least a protocol-enforced minimum bmin —sized above the monitor’s execution cost— paid to whichever party does so, reducing the assumption to

TABLE I: Assumption dependencies of the safety properties. “cond.” marks properties that depend on A4 only in the callback-failure regime (Section VII-B). Property

A1

A2

A3

A4

A5

P1 atomicity (per transfer) P2 supply conservation P3 semantic pres. (class identity) Thm. 1 (identity + amount backing)

✓ ✓ ✓ ✓

✓ ✓ – –

– ✓ – –

cond. cond. – –

– – ✓ ✓

TABLE II: Comparison of cross-chain approaches against the proposed features. “No” denotes absence as a protocol-layer primitive; features F1–F2 can in principle be obtained by composing application-layer contracts on top of any generalA6 purpose messaging bridge. – ✓ Feature (protocol layer) – F1: HTLC atomicity ✓ F2: Auto. callback

the existence of one rational, live observer of the destination chain. A5 (honest profile distributor at registration): the issuer publishes a profile matching the on-chain profileHash at registration time. A6 (relay message authenticity): an inbound message accepted by either chain’s gateway was emitted by the counterpart bridge contract with the stated payload; in the prototype this is discharged by Axelar’s proofof-stake validator quorum. A relay violating A6 can mint unbacked tokens into registered classes but cannot mix classes and cannot burn escrow before a genuine claim publishes S (the callback handler verifies the preimage). The adversary may control users, message delivery (subject to A3), and observers; it may not break A1, A2, A5, or A6. We do not assume an honest user, an honest issuer past registration, or a live relay; message authenticity is the only property for which the relay is trusted. Table I summarises which assumptions each safety property depends on; all property statements in Sections IV-D and VI-E reference it. III. R ELATED W ORK We compare related work against the five features F1–F5 of Section I, organised into four groups. A. Cross-Chain Protocol Formalisations Herlihy [8] formalises atomic cross-chain swaps for fungible exchanges; we adopt his HTLC foundation (F1) but address its two main limitations under heterogeneous chains: the timeout race (via F2) and the implicit assumption of semantic equivalence (via F3, F4). Thyagarajan et al. [9] harden swaps with adaptor signatures but still assume fungible assets. Our protocol is a relay+HTLC hybrid in Zamyatin et al.’s taxonomy [11]. The major surveys [1], [18], [3], [21] identify semantic preservation in no surveyed system; Guo et al. [23] combine relaying with hash-locking for fungible tokens only (F3, F4 absent). Xie et al. [17] build a trustminimised zero-knowledge Cosmos–Ethereum bridge with generic, semantics-agnostic messaging. Marić et al. [24] formally verify a bridge implementation in Isabelle/HOL; we machine-check our protocol’s state machine with TLC (Section VI-E) but leave implementation-level verification open (Section VII-E). B. Protocol Specifications and Standards The IETF SATP [12] targets atomic burn-and-mint transfers via trusted gateways executing 2PC—conceptually adjacent, but gateway-trusted rather than cryptographically locked,

SATP

Gravity

Worm.

LZ

CCIP

ITS

Ours

F3: Determ. class identity F4: Cross-chain class check F5: Multi-class transfer

Noa No No No No

No No No No No

No No No No No

No No No No No

No No No No No

No No No No No

Yes Yes Yes Yes Yes

Chain coverage Bidirectional

N/Ab Yes

2 Yes

30+ Yes

100+ Yes

60+ Yes

20+ Yes

2 Yes

a

b

SATP uses 2PC via trusted gateways. SATP is specification-stage. Worm.=Wormhole; LZ=LayerZero; CCIP=Chainlink CCIP; ITS=Axelar ITS.

specification-stage rather than deployed, and without semantic preservation (F3, F4). Cosmos IBC [20] natively connects Cosmos SDK chains: ICS-20 [26] moves single-denomination fungible tokens and ICS-721 [27] unique NFTs—neither the semi-fungible multi-class semantics indicators require, and neither with HTLC atomicity (F1) or cryptographic classidentity binding (F3). Our protocol uses IBC indirectly through Axelar and adds both above it. C. Production Bridge Systems Production bridges trade cryptographic mechanisms for chain coverage under validator-quorum trust: Gravity Bridge [28], Wormhole [13], LayerZero [14], Chainlink CCIP [15], and Axelar ITS [16] support fungible (typically single-class) tokens and provide none of F1–F5 as protocol primitives; optimistic designs such as Hop [29] substitute fraud proofs, again without F1 or F3–F4. The exploit record— most prominently the $190M Nomad replay hack [30]—and the broader threat landscape [3] motivate cryptographic locks over pure honest-majority designs. Table II compares these approaches; each “No” denotes absence as a built-in protocol-layer primitive (a generic messaging bridge can compose F1–F4 at the application layer, but none surveyed offers them natively). Two contributions follow: (i) no surveyed bridge integrates HTLC atomicity with an automatic callback closing the heterogeneous-chain timeout race; (ii) no surveyed approach, at any layer, preserves domainspecific token semantics across transfer [3], [21], [1]. D. Tokenised Environmental Assets On the domain side, Toucan [31] tokenises registry-verified carbon credits onto Polygon as pooled assets (BCT, NCT), and KlimaDAO [32], [6] builds carbon DeFi on top. Both distinguish broad credit categories but neither cryptographically binds classes to a methodology and evidence bundle (F3) nor addresses cross-chain transfer with semantic preservation (F4)—the problem our protocol solves. IV. S YSTEM D ESIGN This section describes the architecture (Section IV-A), the indicator-token model that prevents semantic mixing (Section IV-B), the end-to-end protocol (Section IV-C), and its state

1. lockForBurn

User

IndicatorToken1155 (ERC-1155)

Polygon (EVM) escrow/burn

BridgeHTLC

burn

2. GMP1

Axelar GMP

5. GMP2

3. prepare mint

4. claim mint(S)

token bridge receiver (CosmWasm) Neutron (Cosmos)

Fig. 1: Architecture and happy-path flow: (1) lockForBurn escrows tokens; (2–3) the relay delivers the prepare message; (4) claim_mint reveals the secret and mints; (5) the automatic callback (dashed only to distinguish the return leg) burns the source escrow.

machine and invariants (Section IV-D). The design is relayand contract-environment-agnostic, requiring only that the destination support state, contract calls, and inbound/outbound relayed messages; Section V describes one instantiation. A. Architecture Overview Figure 1 shows the components and their interactions. Four components compose the system: the source multitoken contract (class definitions and balances); the source bridge contract (escrow, outbound prepare messages, inbound callbacks); the relay, trusted for message authenticity (A6) but not protocol correctness—it cannot claim without S or mint into unregistered classes, and its unavailability affects liveness only; and the destination bridge-receiver contract (mirrored registry, sender and class validation, mint, callback emission). A per-transfer hash H ties three phases together: class registration (once per class, each chain), transfer (source escrow + destination pending-mint), and claim-and-callback. B. Indicator Token Model: Preventing Semantic Mixing (F3, F5) The model makes class identity content-addressed, immutable, and reproducible without coordination. Each indicator is described by an off-chain profile of its semantic attributes—indicator type (e.g., CO2_REMOVAL), canonical unit (e.g., kgCO2e), methodology identifier (e.g., Verra-VM0007), and an evidence bundle—anchored onchain by two digests, profileHash (canonicalised profile) and dataHash (evidence), which bound storage while binding the class to a verifiable artefact. The class identifier is indicatorId = keccak256(profileHash): under A1, parties on different chains holding the same profile derive the same identifier with no coordination protocol. On the source chain, each tokenId is immutably bound at creation to one indicatorId through a metadata record carrying exactly these fields; on the destination, a mirrored TokenClass

record stores the same fields under the same tokenId. Fungibility holds within a class, never across classes. Issuance and amount semantics. Class creation is owneronly on both chains (destination registration additionally whitelist-gated); minting is restricted to the bridge contracts. Amounts are integers in the class’s canonical unit, identical on both chains; cross-class unit conversion is deliberately not performed—it would itself be semantic mixing—and unit harmonisation is out of scope (Section VII-E). C. End-to-End Flow Registration (once per class): the owner builds the profile (Section IV-B), computes profileHash, dataHash, and indicatorId, and registers the class on both chains with the same metadata (owner-only on both; destination registration additionally whitelist-gated). Content-addressing guarantees both chains derive identical indicatorId values without coordination. Transfer: a user U holding class T generates a 32byte secret S, computes H = keccak256(S), and calls lockForBurn(T, A, H, Te , R, b) with amount A, source timeout Te , destination recipient R, and bounty b ≥ bmin — escrowed alongside the tokens, paid to whoever finalises the source-side burn via the permissionless claimBurn, and returned to U when the automatic callback performs the burn or on refund; the protocol-enforced minimum bmin makes the fallback incentive-compatible against an adversarial sender (Section VII-B). The bridge escrows the tokens, reads indicatorId from the token contract (never from user input), and emits a prepare message embedding H, indicatorId, T , A, R, and the destination claim deadline Tc ; only Tc (not Te ) crosses the wire, so ∆T = Te −Tc remains source-side. The destination validates the inbound sender and the class identity (Section IV-D) and records a pending mint indexed by H. Claim and callback: U calls claim_mint(H, S) before Tc ; the contract verifies the preimage, re-validates the class, mints A to R, and emits the (H, S) callback, which the relay delivers to the source _execute to burn the escrow. Since S is public after the claim, claimBurn(H, S) remains available to any party—the property the failure analysis builds on. Refund: an unclaimed pending mint is cancelled by anyone after Tc ; U recovers escrow and bounty via refundBurn after Te . The callback shortens the source chain’s ignorance of a destination claim from “until Te ” to one relay hop; supply conservation holds under adversarial destination timing as long as callback delay stays materially below ∆T (quantified in Section VI; the prototype uses Te = 2 h, ∆T = 30 min, more than an order of magnitude above observed callback latencies). D. Protocol State Machine, Invariants, and Semantic Preservation Per transfer H, the source lock takes states Σs = {⊥, L OCKED, C LAIMED, R EFUNDED} and the destination Σd = {⊥, P ENDING, M INTED, R EFUNDEDd },

with guarded transitions: lockForBurn (⊥ → L OCKED); prepare_mint (⊥ → P ENDING; guard: A6authentic message referencing a registered class with matching indicator_id); claim_mint (P ENDING → M INTED; guard: keccak256(S) = H ∧ t < Tc ); _execute/claimBurn (L OCKED → C LAIMED; guard: keccak256(S) = H); refund_mint (P ENDING → R EFUNDEDd ; guard: t ≥ Tc ); and refundBurn (L OCKED → R EFUNDED; guard: t ≥ Te , sender-only). C LAIMED, R EFUNDED, M INTED, and R EFUNDEDd are terminal; duplicate or replayed messages target non-⊥ states and are rejected without state change. Three invariants over Σs × Σd capture the paper’s safety claims: I1 (single settlement): each side reaches at most one terminal state; I2 (supply conservation): ¬(R EFUNDED ∧ M INTED); I3 (semantic preservation): M INTED into class c implies a prior L OCKED of equal amount whose source class carries the same indicatorId as c. Assumption dependencies follow Table I: I1 holds under A1–A2; I3 is the model-level projection of Theorem 1 (within the model, whose relay may delay, drop, or duplicate but not forge messages, it is structural; the on-chain guarantee requires A1, A5, and—for amount backing—A6); I2, and therefore per-transfer atomicity as the conjunction I1 ∧ I2, requires A4 in the callback-failure regime (Section VII-B). Section VI-E reports exhaustive model checking of I1–I3. Theorem 1 (Semantic preservation): Under A1, A5, and A6, every destination mint of amount A into class c is preceded by a source escrow of amount A of a class c′ with indicatorId(c′ ) = indicatorId(c), and c and c′ commit to the same profile. Proof sketch: Mints occur only in claim_mint, which requires STATE[H] = P ENDING; P ENDING is set only by prepare_mint, whose guard requires a registered destination class matching the message’s indicator_id and token_id. By A6, the message was emitted by lockForBurn, which reads indicatorId on-chain from the source token contract rather than accepting user input, and escrows exactly the amount embedded in the message. Registration binds indicatorId = keccak256(profileHash) identically on both chains, so by A1 (collision resistance) equal identifiers imply equal profile hashes, and by A5 the anchored profile is the published one. Hence the minted class commits to the same profile as the escrowed class, and amounts coincide. Without A6, the amount clause fails (a forged prepare message can mint unbacked tokens into a registered class), but the class-identity clause survives: no execution path mints into an unregistered or identity-mismatched class. V. P ROTOTYPE I MPLEMENTATION We built a prototype that instantiates the design on Polygon (EVM source) and Neutron (Cosmos destination), with Axelar GMP as the relay. The EVM–Cosmos pair is deliberate: its architectural heterogeneity (Section II-A) exercises every

cross-chain assumption. The design itself is not CosmWasmspecific—the destination component requires only inbound message verification, hashlock-indexed mutable state, and outbound message emission—so a Cosmos SDK chain with a native module or another smart-contract environment with these capabilities would change only the implementation. Source-chain contracts. IndicatorToken1155 extends ERC-1155 with the class metadata of Section IV-B, owner-gated class creation, and bridge-only mint/burn. BridgeHTLC enforces the minimum timelock and minimum bounty, stores locks under H, exposes claimBurn/refundBurn plus a pull-payment withdrawPending for bounty payouts that fail to transfer, and implements the Axelar Executable interface so _execute is the only inbound-callback path; a unit-test suite covers the bounty paths. Both compile with Solidity 0.8.19 (IR pipeline, optimiser at 1000 runs). Destination-chain contract. token_bridge_receiver (CosmWasm) holds the mirrored class registry, sender whitelist, and hashlock state. prepare_mint enforces strict 32-byte hex formats and the semantic-identity equality of Theorem 1’s guard—the message’s indicator_id must equal the registered class’s identity, not merely reference an existing class. Inbound authorisation binds to the IBChook intermediary account deterministically derived from the Axelar GMP account and the canonical channel. Builds are reproducible via cosmwasm/optimizer. Outbound messaging from the Cosmos side. Prepare messages travel as JSON, callbacks as ABI bytes; the reverse direction inverts this boundary exactly. Making Cosmosoriginated messages (the callback and the reverse prepare) onchain—rather than delegating to an off-chain relayer process— required three integration constraints that are undocumented in combination and silently stall delivery when violated (Section VI-D): (i) Neutron’s wrapped MsgTransfer with non-zero acknowledgement/timeout fees for its fee-refunder module; (ii) an explicit relayer fee in the Axelar GMP memo naming the fee-collector account, without which the message is routed but never executed; and (iii) fee denomination in an Axelar-registered asset (we use AXL)—unregistered assets (e.g., NTRN) are error-acknowledged and refunded. Claims therefore attach two coins: native fee-refunder fees plus the AXL relayer fee. Reverse direction. Cosmos → EVM is implemented symmetrically: lock_for_burn escrows tokens and bounty on the CosmWasm side, reads class identity from the registry, and emits an ABI-encoded prepare via the on-chain IBC transfer; the EVM bridge validates counterpart and class identity in _execute, and claimMint mints and emits the JSON claim_burn callback. Both directions are covered by the repository’s unit-test suites. The full source code, deployment scripts (using ethers.js and CosmJS), and the verification artefacts cited in Section VI are publicly available [33].

VI. E VALUATION We evaluate the prototype on Polygon and Neutron mainnets, addressing four questions: (i) atomicity and semantic consistency in practice; (ii) end-to-end latency and its acceptability for environmental-asset workloads; (iii) per-side onchain cost and its decomposition into messaging vs. semanticintegrity layer; (iv) safety and liveness under plausible failure modes. Transaction hashes for every run are published in the repository [33] for independent verification on Polygonscan and Mintscan. Experimental setup. Mainnet Axelar GMP routes were used with default finality: ∼64 Polygon-block confirmations before relaying, instant BFT finality on Neutron. The source-paid relay fee is denominated in the source-chain native gas token (POL after the September 2024 MATIC/POL rebrand) and covers destination execution gas and validator attestation. Each transfer used Te = 2 h, ∆T = 30 min. A. Atomic Transfer Results Fully automatic bidirectional validation. For each transfer we verified escrow-before-any-destination-operation, mintonly-after-reveal, burn-after-callback, and indicatorId consistency between the prepare message and the registered class. EVM→Cosmos completed end-to-end in 108 s (34 s prepare relay, ∼1 s claim, 62 s on-chain automatic callback—the destination’s IBC message travelling Neutron→Axelar→Polygon and executing the source burn with no party’s intervention); Cosmos→EVM completed in 93 s (55 s prepare, ∼1 s claim, 31 s callback). The leg asymmetry is structural (Section II-A): Axelar-relayed legs are faster and less variable than legs riding public IBC relayers, and the EVM-side prepare additionally pays Axelar’s stricter source-finality policy. Latency characterization. We ran a campaign of 50 Polygon→Neutron transfers across 7 distinct days and 9 hours of the day. All 50 succeeded and all were finalised by the on-chain automatic callback—no run required the manual fallback. End-to-end latency was 97 s median (p90 122 s, p95 141 s, max 164 s), split into a 33 s median forward relay and a 47 s median callback leg (Figure 2); the tail is modest (p95 is 1.45× the median) and stays far below the 30-min ∆T . Gas was essentially deterministic (lockForBurn 639,191 gas in 49 of 50 runs). These latencies are orders of magnitude faster than voluntary-carbon-market clearing today [6]. B. Transaction Costs The per-transfer costs in the EVM→Cosmos direction are: on Polygon, lockForBurn (615,645 gas, including bounty escrow and GMP emission) and the callback-executed burn (executed by Axelar’s relayer, paid from the relay fee; the manual claimBurn fallback costs 113,406 gas including the bounty payout); on Neutron, claim_mint (452,000– 467,000 gas, including the on-chain IBC callback emission). In the reverse direction, lock_for_burn costs 457,585 gas on Neutron and claimMint 225,752 gas on Polygon. Per transfer, the user pays the source-chain gas, the forward relay

Fig. 2: Empirical CDF of end-to-end latency over the 50transfer Polygon→Neutron campaign (7 days). Median 97 s; p95 141 s; all runs finalised by the automatic callback.

fee (∼1 POL), the destination fee-refunder fees (0.4 NTRN, half refunded on success), the callback relay fee (∼1 AXL, unused portion refundable by Axelar’s gas service), and the optional bounty (returned unless the fallback path is exercised). The cost is dominated by the two relay fees rather than on-chain gas; at representative mainnet prices during the campaign the total user-paid cost is on the order of US$1– 2 per transfer. The total remains orders of magnitude below the value of typical indicator tokens (dollars per kgCO2 e or per kWh), supporting the viability claim in Section VII-D. The refund path was validated by executing deliberately unclaimed transfers; refund operations recover the escrowed tokens and the bounty, so the timeout path imposes no asymmetric penalty on users. C. Cost Decomposition: Where Does the Overhead Go? Decomposing lockForBurn (639,191 gas), the Axelar GMP gas service dominates (∼56%, ∼345,000 gas), followed by HTLC state storage and JSON payload construction. The semantic-integrity layer—a single SLOAD of indicatorId plus 64 bytes of payload—costs ∼2,100 gas, under 0.4% of the total: against an otherwise-identical HTLC bridge without semantic validation, preserving semantics adds essentially nothing. The cross-chain machinery, not the semantic layer, is what costs. D. Failure-Mode Analysis: Safety and Liveness A bridge must satisfy two informal properties: safety— bad outcomes (double-spend, semantic mixing, theft) do not occur—and liveness—good outcomes (eventual claim or refund) eventually occur. The protocol preserves both unconditionally in four of five failure modes; the fifth weakens safety to a conditional property. (a) Forward relay failure (GMP1 lost): no destination state is created; the user refunds via refundBurn after Te . (b) Callback relay failure with monitor present: S becomes publicly readable on the destination once claim_mint succeeds, and any observer can submit claimBurn(H, S) on the source before Te ; the corrective window of ∆T = 30 min is large relative to typical Axelar latencies (≤1 min). (c) Callback relay failure with no monitor before Te : the only mode in which safety is not unconditional. The user can call refundBurn after Te , leaving destination tokens in existence—supply inflation.

The capable set is unbounded (any destination observer), and the escrowed bounty makes the motivated set nonempty: any rational observer profits from submitting claimBurn. The residual assumption is one rational, live observer acting before Te (A4); we name the regime in which no such observer exists weak supply conservation (Sections VII-B, VII-E). (d) Invalid secret: claim_mint and claimBurn require exactly 32 bytes, 0x-prefixed hex, hashing to H; the fixed-length check rules out secret-encoding malleability, a known source of real HTLC bugs. Invalid secrets are rejected without state change. (e) Unregistered class on destination: prepare_mint rejects messages whose token_id has no registered class with matching identity, no destination state is created, and the user refunds after Te ; semantic mixing is prevented by construction. Deployment fault observations. The deployment exercised several failure paths, with verifiable transaction evidence [33]: an undelivered prepare left no destination state and was recovered via refundBurn; a claim_mint violating the destination chain’s IBC fee rules aborted atomically (no mint, pending state still claimable); and callbacks emitted without a valid relayer fee were routed but never executed (modes b/c)— in one such episode the escrow stayed locked until a monitor collected the bounty via claimBurn 1,258 s after lock, a live demonstration of the incentive-compatible fallback under a genuinely failed callback. Safety held in every episode and every locked asset was recovered through the designed paths. E. Security Argument We argue that the protocol satisfies three properties: P1 (atomicity) a transfer either completes on both chains or leaves no net token movement; P2 (supply conservation) the global token supply across both chains never increases; P3 (semantic preservation) no token of class X on the source ever produces a token of class Y ̸= X on the destination. P2 and P3 correspond to invariants I2 and I3 of Section IV-D; P3 is established by Theorem 1. The arguments below sketch how each property is established and which assumptions (Section II-D) it depends on. Dependencies follow Table I. P1 (atomicity) rests on A1+A2—A1 makes the hashlock binding (no S ′ ̸= S with keccak256(S ′ ) = H), A2 prevents either chain from rewinding a confirmed state transition—and, like P2, is conditional on A4 in the callback-failure regime: in mode (c) a destination mint coexists with a source refund, violating P1 and P2 simultaneously unless a monitor acts. P2 additionally rests on A6 (a relay that can forge prepare messages can mint unbacked tokens into registered classes) and on A3 (the destination eventually learns of the lock so a claim is possible). P3’s classidentity guarantee rests on A1+A5: A1 makes indicatorId a binding commitment to the profile, and A5 ensures the profile published by the issuer at registration is the one the on-chain hash actually commits to; the on-chain identity check in prepare_mint then forecloses any mint into an unregistered or mismatched class. The amount-backing clause of Theorem 1 additionally requires A6.

Modes (a), (b), (d), and (e) of Section VI-D preserve all three properties under these assumptions: in (a) and (e) no destination state is created and the escrow is refundable, so the properties hold vacuously; in (b) the public secret lets any observer restore P2 via claimBurn before Te ; in (d) A1 plus the strict 32-byte preimage check rules out any accepted S ′ ̸= S, and rejected calls leave state unchanged. Mode (c) is the only regime in which P1 and P2 are conditional. Under A1+A2, S is still public on the destination after claim_mint, so the capable set for invoking claimBurn is unbounded; both properties hold iff at least one party in that set acts before Te (assumption A4). Concretely, the dependency reduces to: “with probability 1, some party that observes the destination’s Claimed event submits the sourceside claimBurn within Te − tclaim ≥ ∆T = 30 min”. We refer to this conditional regime as weak supply conservation (Section VII-B) and discuss the three mitigations that close or reduce the conditional in deployment. Model checking. We formalised the state machine of Section IV-D in TLA+ [25] and exhaustively model-checked it with TLC over a discretised clock (Tc =4, Te =6; a second configuration uses Tc =3, Te =5) and a relay that may delay, drop, or duplicate either message (duplicate deliveries are verified to be state no-ops). TLC mechanically confirms the analysis above: without A4, I2 is violated—the checker returns an 11-state counterexample in which the callback is merely delayed past Te and refundBurn then coexists with a destination mint—while I1 and I3 hold over the exhaustive state space (157 distinct states). With A4, modelled as an oracle guard (“if the secret is public, a monitor claims before the refund executes”), all invariants hold exhaustively (145 distinct states). The mechanised claim is therefore I2 holds under A4as-assumption, matching Section VII-B; the monitor’s liveness itself is not verified. Two scope notes bound what the model establishes: I2 is the per-transfer projection of P2—violations of P2 by forged mints (A6) lie outside the model, whose relay is faulty but not Byzantine—and the model covers a single transfer instance. The specification, configurations, and reproducible logs are published in the repository [33]. VII. D ISCUSSION A. Critical Analysis of the Results The principal positive finding is that domain-specific integrity is essentially free once messaging is paid for; the principal unanticipated finding is that the dominant operational risk on the callback path is not relay latency but relay eligibility—a message whose fee is missing or wrongly denominated is routed and then silently never executed, a failure only the monitor path (or the timeout) bounds—though across the 50-transfer campaign every run completed automatically, indicating that under normal relayer conditions the eligibility risk is a deployment-configuration concern rather than a recurring runtime failure. Two scope caveats remain: atomicity is not unconditional (the callback-failure regime of Section VII-B, which we resist rounding to “atomic in practice”), and semantic mixing is prevented at the bridge level

only—downstream pooling after minting reproduces the BCT failure mode, out of scope here. B. Weak Supply Conservation: A Conditional-Safety Property We name the safety property under callback failure weak supply conservation: strictly weaker than Herlihy’s unconditional supply conservation [8] in that it additionally requires A4. The weakening is structural: in a single-owner transfer (unlike a two-party exchange) the user already holds the destination tokens when the source burn is needed, so without an incentive claimBurn would be rewardless. The implemented mitigation is the bountied callback: the escrowed bounty is paid to whoever submits a valid claimBurn (a pull-payment fallback ensures payout failure cannot block settlement), turning the empty motivated set into “any rational observer”—the assumption class watchtower systems (e.g., Lightning) deploy in production, and the one TLC verifies as sufficient (Section VI-E). Adversarial-sender analysis. The party that profits in mode (c) is the sender, who also funds the callback fee as claimer and can thus deliberately induce callback failure (misdenominating that fee, a class we observed operationally). With an optional bounty this defeats incentive compatibility for free (lock with b = 0, claim, sabotage the callback, refund). The protocol therefore enforces b ≥ bmin on both chains, bmin owner-set above the monitor’s execution cost (default 0.05 POL). Since the secret is public after the claim and claimBurn is permissionless, a sabotaged callback funds its own defeat: the attacker’s best case is paying bmin to a monitor for no gain. Two stronger mitigations remain future work: accountable watchtowers [8] and native IBC callbacks, which bypass the relay and collapse A4 into A3. C. Comparison with Existing Approaches We adapt HTLCs from atomic exchange to atomic transfer and replace the timeout-ordering safety argument with a relaydriven callback. When correctly funded, the on-chain callback leg has a 47 s median and a 79 s p95 over the 50-transfer campaign (31 s in the reverse direction)—more than an order of magnitude below the 30-min ∆T , mitigating the timeout race [9] without the cryptographic apparatus of swap-focused work. The price is the relay dependency on the callback hop— and, as the deployment observations show, that dependency includes fee-eligibility conditions under which a callback stalls indefinitely rather than slowly, making the bountied monitor path load-bearing rather than auxiliary (Section VII-B). Against alternatives: SATP [12] reaches the same end state via trusted 2PC gateways—opposite ends of the trust/coordination trade-off. Validator-quorum bridges (Wormhole, LayerZero, CCIP, ITS) offer far broader coverage; we share their honest-majority assumption for message authenticity (A6), but a Byzantine quorum here is confined to inflation within registered classes—it cannot cross class boundaries (Theorem 1) nor release escrow without the published secret. None preserves domain-specific semantics, so the BCT failure

mode could re-emerge if any were used for indicator tokens unmodified. D. Implications A 97 s median latency, a per-transfer cost on the order of US$1–2, and <0.4% semantic overhead make the approach viable for environmental-asset workloads (retirement, compliance reporting, periodic transfers between venues), though not for high-frequency movement. The indicator-identity construction is domain-agnostic: any multi-class asset (fractionalised real-world assets, credentials) faces the same mixing risk and admits the same solution at essentially zero added gas. E. Limitations The user must reveal S before Tc (inherent to HTLC atomicity), and the ≥30-min monitoring window is a real dependency—the bounty makes acting within it rational but still requires a live observer. Only hashes are anchored, so a malicious distributor can equivocate on the off-chain profile; a content-addressed registry (IPFS CID anchoring) would close this vector. Class creation is owner-gated. The latency campaign covers EVM→Cosmos (n = 50); the reverse direction is validated end-to-end but characterised by a smaller sample (n = 2). The prototype is Polygon–Neutron over Axelar only—portability to other pairs is argued as a capability checklist, not demonstrated—and the state machine is machine-checked at the design level only; implementationlevel verification [24] remains open. VIII. C ONCLUSIONS AND F UTURE W ORK We addressed atomicity across heterogeneous chains and semantic mixing during transfer, with two contributions: the automatic callback with an escrowed minimum bounty (HTLCs adapted from exchange to transfer, the failure regime covered by an incentive-compatible monitor path machine-checked as sufficient for supply conservation), and the content-addressed deterministic indicator identity that prevents mixing by construction (Theorem 1), addressed by no existing approach. Mainnet evaluation showed fully automatic bidirectional transfers over 50 runs across 7 days (97 s median) and documented the integration failure modes of Cosmos-originated messaging. Future work: native IBC callbacks (eliminating the monitor assumption), DAO-governed class registration, and implementation-level formal verification [24]. ACKNOWLEDGMENT This work was supported by ANII (Uruguay) under grant POS NAC 2023 4 178540 and by Pyxis. The authors used Claude (Anthropic) in agent mode as a coding assistant for implementation; all AI-assisted code was reviewed, tested, and validated by the authors.

R EFERENCES [1] R. Belchior, A. Vasconcelos, S. Guerreiro, and M. Correia, “A Survey on Blockchain Interoperability: Past, Present, and Future Trends,” ACM Computing Surveys, vol. 54, no. 8, pp. 1–41, 2021. [2] G. Wang, Q. Wang, and S. Chen, “Exploring Blockchains Interoperability: A Systematic Survey,” ACM Computing Surveys, vol. 55, no. 13s, Art. no. 290, Jul. 2023. [3] L. Zhang et al., “Security of Cross-Chain Bridges: Attack Surfaces, Defenses, and Open Problems,” in Proc. 27th Int. Symp. Research in Attacks, Intrusions and Defenses (RAID), 2024. [4] Chainalysis Team, “Cross-Chain Bridge Hacks Emerge as Top Security Risk,” Aug. 2, 2022. https://www.chainalysis.com/blog/ cross-chain-bridge-hacks-2022/ [5] S. Pandolfi, G. Llambı́as, and L. González, “Blockchain Interoperability for Environmental Indicators: a Rapid Review,” in Proc. 7th Int. Conf. Blockchain Computing and Applications (BCCA), Dubrovnik, Croatia, 2025, pp. 857–866, doi: 10.1109/BCCA66705.2025.11229811. [6] A. Ballesteros-Rodrı́guez, J. De-Lucio, and M.-Á. Sicilia, “Tokenized carbon credits in voluntary carbon markets: the case of KlimaDAO,” Frontiers in Blockchain, vol. 7, Art. no. 1474540, Oct. 2024, doi: 10.3389/fbloc.2024.1474540. [7] J. Gray, “Notes on Data Base Operating Systems,” in Operating Systems: An Advanced Course, R. Bayer, R. M. Graham, and G. Seegmüller, Eds. Berlin, Heidelberg: Springer, 1978, pp. 393–481. [8] M. Herlihy, “Atomic Cross-Chain Swaps,” in Proc. 2018 ACM PODC, 2018, pp. 245–254. [9] S. A. K. Thyagarajan, G. Malavolta, and P. Moreno-Sanchez, “Universal Atomic Swaps: Secure Exchange of Coins Across All Blockchains,” in Proc. 2022 IEEE Symp. Security and Privacy (S&P), 2022, pp. 1299– 1316. [10] G. Badgley and D. Cullenward, “Zombies on the Blockchain,” CarbonPlan, Apr. 2022. https://carbonplan.org/research/toucan-crypto-offsets [11] A. Zamyatin et al., “SoK: Communication Across Distributed Ledgers,” in Proc. Financial Cryptography and Data Security (FC), 2021, pp. 3– 36. [12] M. Hargreaves, T. Hardjono, and R. Belchior, “Secure Asset Transfer Protocol (SATP) Core,” Internet Engineering Task Force, Internet-Draft, draft-ietf-satp-core, 2024. https://datatracker.ietf.org/doc/ draft-ietf-satp-core/ [13] Wormhole Foundation, “Wormhole: Generic Message Passing Protocol—Architecture and Security Overview,” https://docs.wormhole.com/wormhole/ [14] R. Zarick, B. Pellegrino, and C. Bhageria, “LayerZero: Trustless Omnichain Interoperability Protocol,” LayerZero Labs, Whitepaper V1.1.0, 2021. https://layerzero.network/publications/LayerZero Whitepaper V1.1.0.pdf

[15] Chainlink Labs, “Chainlink 2.0: Next Steps in the Evolution of Decentralized Oracle Networks,” Whitepaper, Apr. 2021. https://research. chain.link/whitepaper-v2.pdf [16] Axelar Network, “Interchain Token Service Documentation,” https:// docs.axelar.dev/dev/send-tokens/interchain-tokens/intro/ [17] T. Xie et al., “zkBridge: Trustless Cross-chain Bridges Made Practical,” in Proc. 2022 ACM SIGSAC Conf. Computer and Communications Security (CCS), 2022, pp. 3003–3017. [18] P. Robinson, “Survey of Crosschain Communications Protocols,” Computer Networks, vol. 200, Art. no. 108488, Dec. 2021. [19] S. Gorbunov and G. Vlachos, “Axelar Network: Connecting Applications with Blockchain Ecosystems,” Axelar, Whitepaper, Jan. 2021. https:// docs.axelar.dev/axelar whitepaper.pdf [20] C. Goes, “The Interblockchain Communication Protocol: An Overview,” arXiv preprint arXiv:2006.15918, Jun. 2020. [21] N. Li et al., “Blockchain Cross-Chain Bridge Security: Challenges, Solutions, and Future Outlook,” Distrib. Ledger Technol.: Res. Pract., vol. 4, no. 1, Art. no. 8, Feb. 2025. [22] W. Radomski, A. Cooke, P. Castonguay, J. Therien, E. Binet, and R. Sandford, “EIP-1155: Multi Token Standard,” Ethereum Improvement Proposals, 2018. https://eips.ethereum.org/EIPS/eip-1155 [23] H. Guo et al., “A Framework for Efficient Cross-Chain Token Transfers in Blockchain Networks,” J. King Saud Univ.—Comput. Inf. Sci., vol. 36, no. 2, Art. no. 101968, Feb. 2024. [24] O. Marić, B. Scholz, and P. Subotić, “Formal Verification of a Fail-Safe Cross-Chain Bridge,” in Proc. 6th Int. Workshop on Formal Methods for Blockchains (FMBC), 2025. [25] L. Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Boston, MA: Addison-Wesley, 2002. [26] Interchain Foundation, “ICS 20: Fungible Token Transfer,” Cosmos IBC Specification, 2019. https://github.com/cosmos/ibc/blob/main/spec/app/ ics-020-fungible-token-transfer/README.md [27] Interchain Foundation, “ICS 721: Non-Fungible Token Transfer,” Cosmos IBC Specification, 2022. https://github.com/cosmos/ibc/blob/main/ spec/app/ics-721-nft-transfer/README.md [28] Gravity Bridge, “Gravity Bridge Design Overview,” GitHub, 2022. https: //github.com/cosmos/gravity-bridge/blob/main/docs/design/overview.md [29] C. Whinfrey, “Hop: Send Tokens Across Rollups,” Hop Protocol, Whitepaper, 2021. https://hop.exchange/whitepaper.pdf [30] Immunefi, “Hack Analysis: Nomad Bridge, August 2022,” Aug. 2022. https://medium.com/immunefi/ hack-analysis-nomad-bridge-august-2022-5aa63d53814a [31] Toucan Protocol, “Tokenization of Carbon Credits,” 2022. https://toucan. earth/ [32] KlimaDAO, “Digital Carbon Ecosystem,” https://docs.klimadao.finance/ ecosystem/digital-carbon [33] S. Pandolfi, “evm-cosmos-indicator-htlc: Atomic Cross-Chain Bridge for Environmental Indicator Tokens,” GitHub Repository, 2026. https: //github.com/sebapandolfi/evm-cosmos-indicator-htlc

Related documents

• An EVM-Cosmos Bridge for Atomic, Semantic-Preserving Transfer of Environmental Tokens#1469333
• Some Preliminary Notes on the Environmental Humanities as a Possible Shift in the Philosophy of Education#692006
• Environmental and climate policy integration: Targeted strategies for overcoming barriers to nature-based solutions and climate change adaptation#423700
• Interdisciplinary collaboration for sustainability science: the training challenge#118897
• Semantics in Robotics: Environmental Data Can't Yield Conventions of Human Behaviour#86529