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

• URL: http://arxiv.org/abs/2604.12172v1
• Date: Tue, 14 Apr 2026 00:56:58 GMT
• Title: COBALT-TLA: A Neuro-Symbolic Verification Loop for Cross-Chain Bridge Vulnerability Discovery
• Abstract summary: COBALT-TLA is a neuro-symbolic verification loop that pairs an LLM with TLC, the TLA+ model checker.<n>We evaluate the system against three cross-chain bridge targets, including a faithful model of the Nomad $190M exploit.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Look Before You Leap: Factual Decoding with Internal Attribution Signals [14.706754790960902]
  Hallucination remains a critical challenge in large language models.<n>We propose DescaPE, a decoding framework that leverages internal model signals to suppress hallucination-prone trajectories at time.
  arXiv  Detail & Related papers  (2026-09-14T15:35:42Z)
• Constraint-Anchored Reasoning Traces [9.39195684989942]
  Autoregressive multimodal large language models (MLLMs) suffer from error snowballing.<n>In state-of-the-art open-source MLLMs, once the first error occurs, the reasoning cascades into failure across all remaining steps in 65% of such cases.<n>We propose Constraint-Anchored Reasoning Traces (CART), a neuro-symbolic framework that trains MLLMs to interleave natural language reasoning steps with symbolic constraint assertions.
  arXiv  Detail & Related papers  (2026-07-18T09:24:45Z)
• Verified Detection and Prevention of Concurrency Anomalies in Multi-Agent Large Language Model Systems [0.0]
  Multi-agent LLM systems state through memory stores, vector indices, and tool registries.<n>We model such sharing as long-running read-generate-write operations under deterministic-generation semantics.<n>We formalize four anomalies in TLA+: stale-generation, phantom-tool, causal-cascade, and tool-effect reordering.
  arXiv  Detail & Related papers  (2026-06-15T18:19:34Z)
• From Attack Simulation to SIEM Rule: Deterministic Detection-as-Code Synthesis with Probe-Level Traceability [51.56484100374058]
  Security teams simulate attacks against their own systems to check whether their monitoring would catch a real intruder.<n>A human bridges that gap by hand, reading each finding and writing the corresponding Sigma rule.<n>We show this translation can be partially automated when probes are drawn from a locked corpus.
  arXiv  Detail & Related papers  (2026-06-03T14:26:25Z)
• A Protocol-Language Model for Network Intrusion (Without Deep Packet Inspection) [0.0]
  We present PLM-NIDS, which proves three claims in sequence.<n>Because it reads only IP/ TCP/UDP headers, it is inherently encryption-agnostic.
  arXiv  Detail & Related papers  (2026-05-29T07:03:11Z)
• Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic [0.0]
  This paper proposes a neuro-symbolic framework for G-code generation that seeks to integrate the neural generative capabilities of the GLLM method with formal verification via a Separation Logic prover.<n>Ultimately, this work aims to develop a self-correcting system that reduces the need for human supervision, leading to safer and verified autonomous manufacturing.
  arXiv  Detail & Related papers  (2026-05-11T13:38:51Z)
• Benchmarking Zero-Shot Reasoning Approaches for Error Detection in Solidity Smart Contracts [0.0]
  This paper evaluates state-of-the-art LLMs on Solidity smart contract analysis using a balanced dataset of 400 contracts.<n>Models are evaluated using zero-shot prompting strategies, including zero-shot, zero-shot Chain-of-Thought (CoT) and zero-shot Tree-of-Thought (ToT)
  arXiv  Detail & Related papers  (2026-02-17T18:08:56Z)
• Trajectory Guard -- A Lightweight, Sequence-Aware Model for Real-Time Anomaly Detection in Agentic AI [0.0]
  Trajectory Guard is a Siamese Recurrent Autoencoder with a hybrid loss function that jointly learns task-trajectory alignment via contrastive learning and sequential validity via reconstruction.<n>At 32 ms latency, our approach runs 17$-27times$ faster than LLM Judge baselines, enabling real-time safety verification in production deployments.
  arXiv  Detail & Related papers  (2026-01-02T00:27:11Z)
• On GRPO Collapse in Search-R1: The Lazy Likelihood-Displacement Death Spiral [59.14787085809595]
  We identify Lazy Likelihood Displacement (LLD) as the core mechanism driving this failure.<n>LLD emerges early and triggers a self-reinforcing LLD Death Spiral, where declining likelihood leads to low-confidence responses.<n>We propose a lightweight likelihood-preserving regularization LLDS for GRPO that activates only when a trajectory's likelihood decreases.
  arXiv  Detail & Related papers  (2025-12-03T19:41:15Z)
• The Trojan Knowledge: Bypassing Commercial LLM Guardrails via Harmless Prompt Weaving and Adaptive Tree Search [58.8834056209347]
  Large language models (LLMs) remain vulnerable to jailbreak attacks that bypass safety guardrails to elicit harmful outputs.<n>We introduce the Correlated Knowledge Attack Agent (CKA-Agent), a dynamic framework that reframes jailbreaking as an adaptive, tree-structured exploration of the target model's knowledge base.
  arXiv  Detail & Related papers  (2025-12-01T07:05:23Z)
• Evaluating Embedding Generalization: How LLMs, LoRA, and SLERP Shape Representational Geometry [0.0]
  We study the extent to which spherical linear (SLERP) model-merging mitigates over-specialization introduced by task-specific adaptation.<n>We compare four families of models: non-LLM encoders trained from scratch or fine-tuned for embeddings, LLM-based encoders adapted with parameter-efficient methods (LoRA), LLM-based encoders with LoRA followed by model souping merging into the base weights, and the same LoRA-adapted LLMs merged using SLERP across checkpoints or stages.
  arXiv  Detail & Related papers  (2025-11-16T17:28:06Z)
• When LLMs Copy to Think: Uncovering Copy-Guided Attacks in Reasoning LLMs [30.532439965854767]
  Large Language Models (LLMs) have become integral to automated code analysis, enabling tasks such as vulnerability detection and code comprehension.<n>In this paper, we identify and investigate a new class of prompt-based attacks, termed Copy-Guided Attacks (CGA)<n>We show that CGA reliably induces infinite loops, premature termination, false refusals, and semantic distortions in code analysis tasks.
  arXiv  Detail & Related papers  (2025-07-22T17:21:36Z)
• Teaching Your Models to Understand Code via Focal Preference Alignment [70.71693365502212]
  In existing approaches, a set of n candidate solutions is evaluated based on test case success rates.<n>Because this approach aligns entire failing code blocks rather than pinpointing specific errors, it lacks the granularity necessary to capture meaningful error-correction relationships.<n>We propose Target-DPO, a new preference alignment framework that mimics human iterative debug to refine Code LLMs.
  arXiv  Detail & Related papers  (2025-03-04T16:56:34Z)
• Attribute Controlled Fine-tuning for Large Language Models: A Case Study on Detoxification [76.14641982122696]
  We propose a constraint learning schema for fine-tuning Large Language Models (LLMs) with attribute control. We show that our approach leads to an LLM that produces fewer inappropriate responses while achieving competitive performance on benchmarks and a toxicity detection task.
  arXiv  Detail & Related papers  (2024-10-07T23:38:58Z)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  Two lines of approaches are adopted for complex reasoning with LLMs.<n>One line of work prompts LLMs with various reasoning structures, while the structural outputs can be naturally regarded as intermediate reasoning steps.<n>The other line of work adopt LLM-free declarative solvers to do the reasoning task, rendering higher reasoning accuracy but lacking interpretability due to the black-box nature of the solvers.<n>We present a simple extension to the latter line of work. Specifically, we showcase that the intermediate search logs generated by Prolog interpreters can be accessed and interpreted into human-readable reasoning.
  arXiv  Detail & Related papers  (2023-11-16T11:26:21Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  We propose a model-free RL algorithm that enables the use of Linear Temporal Logic (LTL) to formulate a goal for unknown continuous-state/action Markov Decision Processes (MDPs) The algorithm is guaranteed to synthesise a control policy whose traces satisfy the specification with maximal probability.
  arXiv  Detail & Related papers  (2019-02-02T20:09:32Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.