BELMA: An Intelligent Contract Security Framework Combining Formal Verification and Large Language Models

BELMA is a two-layer smart contract vulnerability detection and automatic repair framework that innovatively combines the rigor of formal verification with the flexibility of Large Language Models (LLMs). The first layer performs vulnerability detection using word vector models, symbolic execution, and the SWC rule base; the second layer uses fine-tuned LLMs to generate candidate patches, and ensures patch correctness through a closed-loop refinement cycle (generate-verify-feedback-regenerate). This framework can not only handle known SWC vulnerabilities but also has the ability to explore zero-day vulnerabilities, providing a complete solution for smart contract security.

Smart contracts are difficult to modify once deployed, and vulnerabilities can easily lead to huge losses. Traditional security audit methods have limitations: formal verification is rigorous but hard to handle complex contracts; static analysis tools have high false positive rates; LLMs understand semantics but lack mathematical guarantees. The BELMA framework, published in IEEE TDSC 2025, aims to resolve this contradiction by combining formal verification and LLMs to build a two-layer security detection and repair system.

BELMA adopts a two-layer collaborative design:

1. Vulnerability Detection Layer: Integrates Word2Vec word vectors (to understand semantic patterns), symbolic execution engine (to explore path space), and SWC rule base (to identify known vulnerabilities), which can detect known and potential abnormal patterns.
2. Automatic Repair Layer: Uses fine-tuned LLMs to generate patches, introducing two key mechanisms:
   • BiasScore: Analyzes historical repair patterns and adjusts prompts to reduce LLM's systematic bias;
   • ErrorScore: Evaluates patch boundary cases through bounded verification (k=16) to avoid introducing new vulnerabilities. After detecting a vulnerability, the system passes structured context (AST nodes, data flow, etc.) to the repair module.

BELMA uses a closed-loop refinement process: Candidate patches generated by LLMs are re-verified with bounded verification (k=16). If verification fails or ErrorScore exceeds the threshold, feedback is sent to the LLM for re-generation, with a maximum of 5 cycles. This solves the hallucination and lack of verification issues of pure LLMs. In addition, the beyond_swc module identifies abnormal patterns through an anomaly filter, uses LLM reasoning to generate hypotheses and verify them, and has the ability to explore zero-day vulnerabilities to address the evolving attack methods in the blockchain field.

BELMA provides complete experiment reproduction scripts, covering baseline data for RQ1-RQ4, with a clear module structure (detection, repair, optimization, etc.). Configuration is centralized in belma_config.yaml to ensure reproducibility. The project includes comparative experiments with tools like Echidna and sFuzz, as well as sensitivity analyses such as complexity stratification and single-node ablation, reflecting the verifiability standards of academic research.

Practical deployment needs to consider:

• Computational cost: Symbolic execution and multiple LLM calls have significant overhead;
• Latency issue: The closed-loop refinement cycle may extend repair time;
• Platform support: Mainly optimized for Ethereum; the maturity of Fabric/EOS adapters needs to be improved. The project documentation provides DEPLOYMENT.md and FAILURE_TAXONOMY.md, which discuss failure modes and response strategies.

BELMA represents an important direction in the field of smart contract security: combining the rigor of formal methods with the flexibility of LLMs to achieve complementary advantages. It provides developers with a complete path from vulnerability discovery to repair; for researchers, it demonstrates the engineering integration of LLMs and formal verification. As LLM capabilities improve, this hybrid paradigm of 'AI generation + formal verification' is expected to be applied in more safety-critical fields.