2604.12172

# COBALT-TLA: A Neuro-Symbolic Verification Loop for Cross-Chain Bridge Vulnerability Discovery **Authors**: Dominik Blain ## Abstract Cross-chain bridge exploits have caused over $1.1B in losses through a single recurring pathology: temporal ordering violations in distributed state machines. Existing static analyzers and bounded symbolic execution engines lack the semantic vocabulary to reason about concurrency and finality, while TLA+—the formal specification language designed expressly for this class of flaw—remains inaccessible due to prohibitive syntactic and mathematical complexity. Large language models offer theoretical coverage of this gap but produce severely hallucinated TLA+ specifications when applied zero-shot, generating unbounded state spaces that instantly exhaust model checker memory. We present COBALT-TLA, a neuro-symbolic verification loop that pairs an LLM with TLC, the TLA+ model checker, in an automated REPL. The LLM generates bounded TLA+ specifications; TLC acts as a semantic oracle; structured error traces are parsed and injected back into the model’s context to drive convergence. We evaluate the system against three cross-chain bridge targets, including a faithful model of the Nomad $190M exploit. COBALT-TLA reaches a verified BUG_FOUND state in $≤ 2$ iterations on all targets, with TLC execution consistently below 0.30 seconds. Notably, the system autonomously discovers an unprompted vulnerability class—the Optimistic Relay Attack —not present in the human-written baseline specification. We argue that deterministic prover feedback is sufficient to neutralize LLM hallucination in formal methods, transforming zero-shot code generation into a convergent proof-finding strategy. ## I Introduction Cross-chain bridge exploits represent the most catastrophic capital destruction events in the history of decentralized finance. The Ronin Network ($625M), Wormhole ($320M), and Nomad ($190M) exploits share a fundamental pathology: they were not caused by standard cryptographic failures or simple arithmetic overflows. Instead, they were temporal ordering violations and distributed state synchronization failures. These are architectural flaws where the sequencing of individually valid transactions produces a globally invalid state, allowing attackers to spoof messages or bypass finality. The current Web3 security apparatus is structurally blind to this class of vulnerability. Industry-standard static analyzers (e.g., Slither) and bounded symbolic execution engines (e.g., Echidna, Z3) evaluate intra-contract logic but lack the semantic vocabulary to reason about concurrency, distributed consensus, and time. While formal specification languages like TLA+ and its model checker TLC were designed expressly to verify concurrent systems—famously used by Amazon Web Services to verify S3’s consistency [2] —their steep learning curve and esoteric mathematical syntax have prevented their adoption in smart contract security. The Web3 industry possesses the right problem, but lacks the engineering bandwidth to deploy the right tool. Large Language Models present a theoretical bridge to this gap, demonstrating near-expert proficiency in code generation. However, applying zero-shot LLMs to formal verification yields severe hallucinations. When tasked with writing TLA+, LLMs routinely declare unbounded sets or infinite state spaces, causing TLC’s breadth-first search to instantly exhaust available memory. Without a strict, programmatic grounding mechanism, LLMs cannot reliably produce verifiable formal specifications; they generate syntax that looks like math, but fails as a proof. To solve this, we introduce COBALT-TLA, the first neuro-symbolic verification engine that orchestrates a Read-Eval-Print Loop (REPL) between a Large Language Model and the TLC model checker. Rather than relying on zero-shot generation, COBALT-TLA treats the LLM as a hypothesis generator and TLC as an absolute semantic oracle. By deterministically parsing TLC’s raw error traces—including compilation failures and invariant violations—and injecting them back into the model’s context window, the system forces the LLM to autonomously converge on a valid, tightly bounded TLA+ specification. We demonstrate the efficacy of this architecture against three distributed bridge models. COBALT-TLA not only successfully reverse-engineered the exact state-transition trace of the $190M Nomad exploit from a natural language prompt, but also autonomously discovered an unprompted Optimistic Relay Attack in a standard Lock-and-Mint architecture. In all experiments, the neuro-symbolic loop converged on a verified vulnerability trace in a maximum of two iterations, proving that LLM hallucination in formal methods can be effectively neutralized via automated prover feedback. ## II Background ### II-A Temporal Logic and the TLA+ Model Checker TLA+ (Temporal Logic of Actions), introduced by Lamport [1], is a formal specification language designed to model concurrent and distributed systems. Unlike programming languages, TLA+ relies on first-order logic and set theory to describe discrete state transitions over time. A TLA+ specification defines an initial state (Init) and a next-state relation (Next), mapping out every mathematically possible execution path of the system. TLC, the companion model checker, explores this state space via breadth-first search to verify whether a given SafetyInvariant holds across all reachable states. The “small scope hypothesis” [3] supports the practical utility of bounded model checking: most structural errors in protocol design manifest within small instances of the state space. While highly effective at identifying deadlocks, race conditions, and synchronization flaws in complex architectures, TLA+ has seen limited adoption in the smart contract security industry due to its steep learning curve and its lack of direct translation to EVM bytecode. ### II-B Cross-Chain Bridges and Temporal Vulnerabilities Cross-chain bridges are asynchronous, distributed state machines that lock collateral on a source chain and mint equivalent assets on a destination chain, usually coordinated by an off-chain relay or multisignature scheme. Because these events occur across disparate networks with independent consensus mechanisms, they are highly susceptible to temporal ordering violations. If the destination chain executes a state transition (e.g., minting a token) based on a source chain state that is subsequently reverted (e.g., a blockchain reorganization) or spoofed (e.g., initializing an unverified Merkle root as valid, as in the Nomad protocol [4]), the global invariant of the system—the peg between locked and minted assets—is irreparably broken. ## III Methodology ### III-A System Architecture We present COBALT-TLA, a neuro-symbolic verification loop that pairs a large language model with TLC in a REPL. The system operates as a Read-Eval-Print Loop: the LLM generates a formal specification, TLC evaluates it against declared invariants, and the resulting proof state—whether a violation trace or a compilation error—is injected back into the LLM’s conversational context as structured feedback. The loop terminates when TLC either confirms all invariants hold (SAFE) or produces a counterexample (BUG_FOUND), or when the iteration budget is exhausted. The architecture comprises four components: (1) a prompt-engineered specification generator, (2) a bounded state space enforcer embedded in the system prompt, (3) a subprocess execution layer wrapping TLC, and (4) an error trace parser that transforms TLC’s raw output into semantically meaningful feedback. ### III-B Specification Generation The LLM receives a natural language description of a cross-chain protocol and produces two artifacts: a TLA+ module (.tla) and a TLC configuration file (.cfg). The system prompt constrains output to a strict structural template and requires both artifacts as delimited code blocks, enabling deterministic extraction via regular expression. The SafetyInvariant convention inverts the standard verification framing. Rather than asking the LLM to prove a system correct, we ask it to model a system whose known flaw will produce a TLC counterexample. A SAFE result under this convention signals a modeling error, not protocol correctness—a critical distinction that guides the LLM’s self-correction strategy. ### III-C Bounding the State Space Unbounded state spaces are the primary failure mode when LLMs generate TLA+ specifications. We address this through constraint injection in the system prompt: all variables must be typed over finite ranges (0..MaxN), all bounds must be declared as CONSTANTS, and no infinite sets may appear in the specification body. Default constant values (MaxTokens = 3) are prescribed and can be escalated if state coverage is insufficient. The TypeOK invariant serves a secondary bounding function, surfacing type violations before invariant violations. ### III-D Formal Verification Engine TLC is invoked as a child process via subprocess.run, with the TLA+ module and configuration written to an isolated temporary directory per invocation. TLC’s exit code provides coarse classification: 0 (safe), 12 (invariant violation), other (parse/semantic error). We rely on TLC’s breadth-first search, which guarantees that any counterexample is a shortest violation trace—a property exploited in the feedback mechanism to minimize hallucination in the correction step. ### III-E Error Trace Extraction Raw TLC output is unsuitable for direct LLM consumption. Our parser applies the following pipeline: (1) exit code classification into SAFE, VIOLATION, COMPILE_ERROR, or TIMEOUT; (2) state block segmentation on the regex State \d+:; (3) variable extraction matching the pattern /\ <identifier> = <value> (TLC formats variable assignments with a single backslash, discovered empirically via byte inspection of subprocess output); (4) action annotation from the bracketed action name in each state block header. The structured trace is serialized into a compact natural language summary distinguishing two correction directives: confirm the finding (real bug) or tighten the action guard (modeling error). ### III-F The Agentic REPL Loop The loop is implemented as a multi-turn conversation. Each LLM response is appended as an assistant turn and each TLC feedback message as a user turn, preserving the full specification history within the model’s context window. This is analogous to interactive proof development in Coq or Lean 4, where the user and the proof assistant alternate moves. ## IV Experimental Results To evaluate COBALT-TLA, we deployed the system against three cross-chain bridge targets. T1 is a baseline Lock-and-Mint architecture with a human-written ground-truth specification (Reorg Attack). T2 uses the same architecture but tasks the LLM with emergent vulnerability discovery. T3 models the historical authentication flaw in the Nomad bridge ($190M exploit, August 2022). TABLE I: Empirical Verification Results | T1 | Lock-Mint (Reorg Attack) | Reorg / Stale Queue | 0 | 4 | 10 | 0.27 | 0.27 | | --- | --- | --- | --- | --- | --- | --- | --- | | T2 | Lock-Mint (Optimistic Relay) | Pre-finality Mint | 1 | 4 | 15 | 0.30 | 17.9 | | T3 | Nomad-style (Zero-Root Init) | Init. Vulnerability | 1–2 | 3 | 8–25 | 0.29 | 28–49 | Iter = LLM iterations to BUG_FOUND (0 = ground truth, no LLM involved). Depth = shortest counterexample trace length. $t_e2e$ dominated by LLM API latency (~17–28s); $t_tlc$ is effectively constant. ### IV-A Performance Profile and Execution Overhead A critical observation is the asymmetry between LLM generation time ( $t_llm$ ) and TLC execution time ( $t_tlc$ ). Across all targets, TLC resolution remained strictly bounded between 0.26s and 0.30s, regardless of target complexity. End-to-end latency is entirely dominated by LLM API inference ( $∼$ 17–28 seconds per generation). Because TLC acts as a high-speed oracle rather than a computational bottleneck, the system is horizontally scalable: multiple protocol audits can run in parallel without solver contention. ### IV-B Agentic Convergence and Error Recovery For T2, the system reached convergence on the first LLM generation. For T3, we observed a convergence variance of 1 to 2 iterations across runs. In runs requiring 2 iterations, the initial specification contained a TLA+ compilation error. Rather than failing, the REPL successfully captured the parse error, injected the stack trace back into the LLM context, and prompted a correction. The model resolved the syntax error and generated the exploit trace on the subsequent attempt. This empirical variance validates the core hypothesis: the subprocess feedback loop acts as a self-healing mechanism for LLM syntax failures. ### IV-C Qualitative Vulnerability Discovery Beyond compilation metrics, the system demonstrated non-trivial semantic reasoning. During the T2 run, the LLM-generated specification identified an Optimistic Relay Attack —a pre-finality minting vulnerability entirely distinct from the T1 ground truth and not present in the target description. TLC validated this vulnerability with a 4-state trace across 15 explored states. For T3, the agent modeled the Zero-Root Initialization flaw, reproducing the exact causal chain of the 2022 Nomad exploit (ActivateZeroRoot $→$ ExploitProcessWithoutProof) in a minimum of 3 states. ## V Threats to Validity ### V-A State Space Truncation All targets use small constant bounds (MaxTokens = 3). We note that all violation traces have depth $≤ 4$ , meaning the attack sequence requires at most four protocol transitions regardless of supply bounds. This is consistent with the small scope hypothesis: increasing MaxTokens increases explored states without changing violation depth. T3 required only 2 transitions at MaxMessages = 3 —a property of initialization logic, not of the bound. ### V-B Model Fidelity The TLA+ specifications abstract away gas limits, nonce management, and EVM opcode semantics. For T3, this abstraction is validated externally: the Nomad exploit was publicly confirmed and our trace reproduces the post-mortem causal chain. For T1 and T2, the vulnerability patterns are structural properties documented in bridge security literature. ### V-C LLM Non-Determinism LLM outputs are stochastic. The relevant reproducibility claim is: for these target classes, the loop reaches BUG_FOUND within 2 iterations across all observed runs. A 5-run statistical analysis of T3’s iteration distribution is left to extended evaluation. ### V-D Prompt Engineering Dependency The system prompt constrains syntax, not semantics. It does not name protocol actions, specify state variables, or describe attack vectors for any particular target. The Optimistic Relay Attack (T2) was generated entirely from the protocol description, without prompting. Reviewers may replicate this by submitting the T2 description to any TLA+-capable LLM with a structurally equivalent system prompt. ### V-E Target Scope Limitation All three targets are cross-chain bridge protocols. COBALT-TLA targets temporal ordering violations in distributed state machines. Arithmetic bugs remain in Z3’s domain; reentrancy is better handled by symbolic execution. The contribution demonstrates that LLM-guided TLA+ verification is sufficient and appropriate for the temporal class—not that it supersedes other tools. ### V-F Absence of Production Code Analysis The system operates on protocol descriptions, not deployed contract bytecode. COBALT-TLA is a protocol-level verifier analogous to how AWS used TLA+ to verify S3’s consistency before implementation. Closing the gap to EVM bytecode via KEVM integration is future work. ## VI Related Work ### VI-A Formal Verification in Decentralized Finance The Web3 security landscape utilizes static analysis (Slither) and bounded symbolic execution (Echidna, Z3) for arithmetic overflows, reentrancy, and invariant breaches at the EVM level [5]. These are intra-contract analyzers; they struggle to model cross-contract concurrency and off-chain relay dynamics. The K Framework and KEVM offer robust EVM semantic modeling, yet specifying protocol architecture in K remains highly manual. Our work shifts the verification target from bytecode execution to architectural design, catching logic flaws before implementation. ### VI-B LLM-Assisted Formal Methods LeanDojo [6] uses language models to generate tactics for Lean 4 interactive theorem proving. AUTOSPEC [7] explores LLM-generated property specifications for model checking. COBALT-TLA diverges from these approaches by focusing on fully autonomous REPL orchestration rather than human-in-the-loop assistance, and by demonstrating that deterministic prover feedback alone is sufficient to correct LLM hallucinations in TLA+ for a high-value security domain. ## VII Conclusion The persistent frequency and severity of cross-chain bridge exploits underscore a critical gap in decentralized finance security: current automated tools evaluate code, but fail to reason about time, concurrency, and distributed state. While TLA+ provides the theoretical rigor to close this gap, its practical deployment is bottlenecked by syntactic complexity. COBALT-TLA demonstrates that Large Language Models can bridge this usability gap, provided they are tightly coupled with a deterministic semantic oracle. By structuring a neuro-symbolic REPL between an LLM and TLC, we neutralize the stochastic hallucination inherent in zero-shot code generation. Our empirical results show that the system autonomously generates valid, bounded TLA+ specifications and discovers complex temporal vulnerabilities—including the historic $190M Nomad exploit and an emergent Optimistic Relay Attack—within a minimal number of iterations. Future work will explore extending this neuro-symbolic loop to full EVM semantics via KEVM, moving automated formal verification from the architectural layer down to production bytecode. ## References - [1] L. Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002. - [2] C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker, and M. Deardeuff, “How Amazon web services uses formal methods,” Communications of the ACM, vol. 58, no. 4, pp. 66–73, 2015. - [3] D. Jackson, Software Abstractions: Logic, Language, and Analysis. MIT Press, 2006. - [4] Nomad Team, “Nomad bridge exploit post-mortem,” Aug. 2022. [Online]. Available: https://medium.com/nomad-xyz-blog/nomad-bridge-hack-root-cause-analysis-875ad2e5aacd - [5] D. Perez and B. Livshits, “Smart contract vulnerabilities: Vulnerable does not imply exploited,” in Proc. USENIX Security, 2021. - [6] K. Yang et al., “LeanDojo: Theorem proving with retrieval-augmented language models,” in Proc. NeurIPS, 2023. - [7] H. Sun et al., “AUTOSPEC: Automated specification generation for formal model checking via large language models,” 2024. [Preprint]