COBALT-TLA: A Neuro-Symbolic Verification Loop for Cross-Chain Bridge Vulnerability Discovery

TL;DR

COBALT-TLA is a neuro-symbolic verification system combining LLMs and TLA+ model checking to efficiently discover vulnerabilities in cross-chain bridges, including novel attack classes.

Contribution

The paper introduces COBALT-TLA, a novel neuro-symbolic loop that automates vulnerability discovery in blockchain bridges using LLMs and formal verification, achieving rapid convergence and uncovering new attack types.

Findings

COBALT-TLA verified bugs in three cross-chain bridge models within 2 iterations.

The system discovered a new vulnerability class, the Optimistic Relay Attack.

TLA+ model checking execution times remained below 0.30 seconds per run.

Abstract

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 at most 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.