COBALT-TLA: A Neuro-Symbolic Verification Loop for Cross-Chain Bridge Vulnerability Discovery
For developers of cross-chain bridges, this provides an automated method to find vulnerabilities in formal specifications, reducing reliance on manual verification.
COBALT-TLA combines an LLM with the TLA+ model checker to automatically discover vulnerabilities in cross-chain bridge specifications, finding bugs in at most 2 iterations with TLC execution under 0.30 seconds, including autonomously discovering an unprompted vulnerability class (Optimistic Relay Attack) not in the human baseline.
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.