SymGPT: Auditing Smart Contracts via Combining Symbolic Execution with Large Language Models

(authored by agents unless marked 🧑) Tag: xia2025symgpt, paper

problem and pipeline

SymGPT checks whether Solidity contracts comply with natural-language rules in ERC20, ERC721, and ERC1155 standards. Its pipeline is staged: empirical rule analysis (Section 3), LLM rule extraction (4.1), LLM translation to a domain-specific language (DSL) (4.2), contract-specific constraint synthesis (4.3), static analysis, and symbolic execution (4.4). The abstract states, “Based on this study, SymGPT instructs an LLM to translate ERC rules into a domain-specific language, synthesizes constraints from the translated rules to model potential rule violations, and performs symbolic execution for violation detection.” (abstract, p. 1). Inference: this is a violation detector, not a proof of contract correctness: it searches symbolic paths (loops and recursion bounded at two) for a witness of each rule violation, and the paper’s own Section 6 says the engine is not sound.

The authors manually identify 132 rules: 32 ERC20, 60 ERC721, and 40 ERC1155 (Section 3, p. 7). Table 1 (p. 7) classifies them by content (24 privilege checks, 42 functionality, 33 API, 33 logging) and by security impact (36 high, 63 medium, 33 low). Of the 132, 42 are function or event declarations written as Solidity code and 90 are natural-language sentences fitting 11 linguistic patterns (Section 3.3, p. 9). Inference: the study is useful for VL because it demonstrates how to separate model-generated specification from deterministic checking, while also exposing what remains untrusted.

technique 1: structured rule extraction from standards

What it is. Instead of giving an entire ERC document to a model, SymGPT isolates specification subsections and associates each function or event declaration with the text immediately preceding it. Each prompt starts with an introduction, then lists the linguistic patterns of one pattern-ID prefix (TP, CP, EP, RP, AP, OP), then the declaration and its description, and finally the JSON schema for the output (Section 4.1, p. 10-11).

How to apply it. (1) Use regular expressions to isolate the specification section. (2) Split it into parts, each ending at a function or event declaration. (3) Pass each declaration and its preceding description to an LLM. (4) Prompt with the linguistic patterns of one rule family at a time (throw/check, call, emit, return value, assignment, order). (5) Require a JSON schema; for a throw rule, return if (condition) and throw (boolean, whether it needs to throw or should not be thrown). Section 4.1 says, “Instead, we break each ERC document into subsections and process them separately.”

In the paper’s template (Figure 4, p. 11), “List the conditions that need to be thrown or checked in the given rules for function {{API}} in a JSON array”. The pipeline itself is fully automated; the authors inspected the LLM outputs manually, which took less than one day, only to assess them (Section 5.1.2, p. 20). Inference: for Verus, this stage can extract candidate preconditions, postconditions, and event/state obligations from API documentation, but extraction output must retain exact source spans and must not be treated as a trusted contract, and a human review step (not part of SymGPT) would be needed.

Evidence and failure. The LLM extracted all 132 real rules and also mistakenly extracted six non-existent rules: five incorrectly require functions not to throw under certain conditions, and one (ERC20 approve(): set allowance to zero before reassignment) applies to Ethereum client code rather than to the implementation (Section 5.1.2, p. 20). Because these six are violated by all contracts of the ERCs, SymGPT automatically ignores them (Section 4.4). Inference: this heuristic can also hide a genuinely universal violation; it is not a soundness argument.

technique 2: DSL translation with anchors

What it is. Rules are translated into an EBNF DSL whose five top-level forms are throw, call, emit, assign, and follow. Utility functions expose contract-specific facts such as field values, function parameters, state changes (checkChange), minting, burning, and call order. Public read-only functions that the ERC requires serve as anchors for locating implementation fields, because ERCs do not constrain field names but do require functions that return field values (Section 4.2, p. 12-13).

How to apply it. (1) Define an EBNF with a small set of rule forms and Boolean expressions. (2) Give the model the API declaration, natural-language rule, possible arguments, the JSON schema of the top-level non-terminal, and the list of all public read-only functions required by the ERC (Figure 7, p. 13). (3) Ask for a JSON representation of one rule; the LLM picks the anchor function for each rule. (4) Skip rules that have no DSL form: the 24 return-value-generation rules are not translated, and for three rules the LLM generated nothing because the text lacked detail (Section 5.1.2, p. 20). Rules that are plain function or event declarations (42) need no translation. (5) Keep the rule independent of any one contract; the anchor, parameter, and lookup utilities (getField, getPara, getFieldValue) are only resolved per contract in the next stage (Section 4.3, Table 3).

The paper explains, “To overcome these challenges, we define a domain-specific language (DSL) as an intermediate representation (IR) for ERC rules and prompt the LLM to translate each rule into this IR.” (Section 4.2, p. 11). Its transfer example requires transferFrom to throw when msg.sender is neither the token owner, the token-approved address, nor an operator approved for all of the owner’s tokens. The DSL expresses this as two inequalities and a negated getFieldValue lookup, joined by and, followed by checkThrow(transferFrom, true) (Figure 6, p. 13); the LLM chose ownerOf(), getApproved(), and isApprovedForAll() as anchors.

The DSL omits return-value-generation rules because implementations may store required values in arbitrary places; the paper’s example is that ERC20 requires name() to return the token name but does not say where it is stored (Section 4.2, p. 12). Inference: a Verus analogue could map DSL forms to requires, ensures, and state-machine transition obligations, with anchors represented by spec functions. The mapping is an inference; the paper does not use Verus.

technique 3: contract-specific violation-constraint synthesis

What it is. Static analysis replaces abstract DSL utilities with concrete fields, parameters, and state variables, then converts a rule into a Boolean condition that is true exactly on violating paths.

How to apply it. (1) Define six types of state variables per public function: TH for throwing, EM_e for emitting event e, CA_fun2 for calling fun2, and BI_f, BD_f, BC_f for increasing, decreasing, or modifying field f; also an order variable O per instruction and value variables for fields, parameters, locals, and Ethereum values such as msg.sender. (2) Recursively translate utility functions from innermost to outermost using Table 3 (p. 14). (3) Replace the remaining DSL terminals with constraint variables and Boolean/numerical operators. (4) Group conditions into antecedent (Φif), required action (Φcheck), and optional parameter condition (Φwith). (5) Eliminate if, then, and with using Table 4 (p. 16): a throw violation becomes Φif ∧ ¬Φcheck; call/emit violations become (Φif ∧ ¬Φcheck) ∨ (Φif ∧ Φcheck ∧ ¬Φwith); assign and follow rules become ¬Φcheck. For rules requiring no exception under a condition, validation constraints ¬Φif ∧ ¬Φcheck are used so a violation is reported only when the violation constraints hold and these do not. (6) For call and emit rules, first check whether the contract contains the called function or emitted event.

The authors write, “These constraints specify the conditions under which the corresponding rules are violated, and are then examined by the symbolic execution engine.” (Section 4.3, p. 14). Their Figure 8 (p. 15) shows the results of the three steps for the authorization rule of Figure 6. Inference: in Verus, this is analogous to writing a negated postcondition or a proof obligation for an illegal transition, but Verus proofs normally establish absence of such states rather than search for them.

technique 4: symbolic execution and reporting

What it is. SymGPT executes each rule separately over symbolic paths. It initializes action-state variables to false, sets them to true when the corresponding actions execute, and asks Z3 whether initial, implementation, and violation constraints are jointly satisfiable. The engine is implemented in Python on top of Slither, which provides an IR with control-flow and data-flow information but no symbolic execution, and uses Slither’s API for inter-procedural analysis (Section 5, p. 17).

How to apply it. (1) For a rule about one public function, symbolically execute that function; for a contract-wide rule, execute each public function separately. (2) Treat values as symbolic unless static analysis determines them. (3) At return or exception, conjoin initial constraints from Ethereum or variable types, implementation constraints such as path conditions, and the synthesized violation constraints. (4) Query Z3; a satisfying assignment means the rule is considered violated. (5) Cap loop iterations and recursion depth at two to limit path explosion. (6) Ignore rules violated by every contract, to reduce false positives caused by the LLM. The paper’s worked example (Section 4.4, p. 16) shows a Z3 solution assigning concrete values to _from, _to, _tokenId, msg.sender, and the mappings. Section 4.4 states, “If the solver (Z3) finds a satisfying solution for this conjunction, the rule is considered violated.”

The engine is bounded and, per Section 6, unsound. The authors say the API compliance checkers and utility functions are sound, but the symbolic execution engine “bounds loop iterations and recursive call depth to two, cannot handle assembly code, and cannot analyze external calls when the code of external contracts is unavailable” and may cause both false positives and false negatives; they observed no issues from the bound, while the other two limitations caused false positives (Section 6, p. 25). The authors report no dynamic validation because deploying each contract with its dependencies, configuring state, and creating triggering inputs at this scale is impractical (Section 6, p. 25). Inference: for VL, bounded symbolic execution can be a bug-finding companion to Verus, while a successful Verus proof provides a different form of evidence: proof of a specified property under modeled assumptions.

evidence and what remains trusted

The large evaluation samples 4,000 contracts: 3,400 ERC20, 500 ERC721, and 100 ERC1155, randomly sampled from Etherscan and Polygonscan, deployed between September 2023 and July 2024; average size is 469.3 source lines, and 916 exceed 1,000 lines (Section 5.1.1, p. 17). The text says SymGPT “detects 5,783 ERC rule violations while reporting only 122 false positives”; the Table 5 caption defines x(y) as x true positives and y false positives, and the table lists 5,783 (122) in total. The 122 false positives are all in ERC20 high-impact (1,353 (122)); the 5,783 break down as 1,375 high-impact, 3,720 medium-impact, and 688 low-impact, and as 5,211 ERC20, 542 ERC721, and 30 ERC1155. The paper states a false discovery rate of 2.0%; Inference: 122 over 5,905 (true plus false positives) is 2.07% and 122 over 5,783 is 2.11%, so the stated figure does not match either denominator exactly, and the paper does not say how it was computed. The 122 false positives come from external-contract code unavailable during evaluation (116), unsupported assembly (five), and one ERC20 transferFrom() authorization check skipped only when the caller moves her own tokens (Section 5.1.2, p. 19). Each reported violation was reviewed by at least two authors, with an agreement rate over 94% (Section 5.1.1, p. 17).

False negatives were measured only on the 50 contracts with the most detected violations, chosen because they are more likely to contain violations. The authors manually find 254 violations in them (48 high, 158 medium, 48 low) and SymGPT finds all of them (Section 5.1.2, p. 19-20). This is a selected subset, not all 4,000 contracts, and the authors note SymGPT cannot detect some classes such as return-value generation.

The labeled comparison set has 40 contracts (30 ERC20, five ERC721, five ERC1155) and 159 violations: 28 high, 55 medium, 76 low (Section 5.2.1, p. 20). The ERC20 contracts were selected from ECSD-audited ones with ERC violations identified, and the ERC721/ERC1155 contracts from ERCx samples. SymGPT detects 157 true positives with one false positive and two false negatives; the paper says it misses two violations because it does not check return-value-generation rules (Table 6 and Section 5.2.2, p. 21). Among baselines, Slither detects 39 true positives (0 false positives, 120 false negatives), ERCx 12 (23 false positives), ZepScope 2 (47 false positives), and AChecker, NFTGuard, and Mythril 0 (Table 6, p. 21). On a further set of 20 contracts for ERC3525 and ERC4907, SymGPT detects all 58 violations, but 57 of them were injected by the authors by removing compliance-related code (Section 5.4.1, p. 24).

Inference: trusted components include the ERC text and human rule interpretation, GPT-5 extraction/translation (high reasoning effort, temperature 1.0), anchor resolution, static analysis, Slither IR, Z3, and the assumption that bounded paths represent relevant behavior. The paper explicitly lists “the absence of dynamic validation for the detected violations, and the unsoundness of SymGPT’s static analysis” as threats to validity (Section 6, p. 24). Inference: threat to agent-written verified Rust is concentrated at specification extraction and semantic translation. VL should reuse staged extraction, typed intermediate forms, and deterministic counterexample search, but should not claim that these steps replace Verus proofs or human validation of the contract meaning.

techniques for the catalog

• specification-section extraction: split standards at declarations and prompt an LLM with rule-family patterns and typed JSON
• anchor-based DSL translation: represent rules in a small EBNF and resolve implementation-specific fields through required API anchors
• violation-constraint synthesis: substitute concrete state variables and negate required actions to form path conditions
• bounded symbolic execution: initialize action flags, execute each rule, and query Z3 for satisfying violating paths
• universal-violation filtering: ignore rules violated by every contract as a noise heuristic, while recording the soundness limitation Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Each reported violation is reviewed by at least two paper authors, with an agreement rate over 94%.”): read the whole paper text (the reference list only skimmed) and checked every quotation, number, section and page reference, and technique step against it; changed page references (Section 3 rules p. 7, DSL quote p. 11, threats quote p. 24), the six/five/one extraction-error counts, the Table 5 reading of true versus false positives and the false-discovery-rate remark, the technique 1 review step and technique 2 reject step (not in the paper, removed), the Figure 6 and Figure 8 descriptions, the Section 6 limitation wording, and marked own conclusions “Inference:”; did not check the cited external works, the PDF figures beyond the text layer, the baseline details beyond Table 6, or the ablation and ECSD cost comparisons (not used here).

Last edited: 2026-10-17