All Artificial, Less Intelligence: GenAI through the Lens of Formal Verification

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

purpose and result

The paper evaluates whether large language models (LLMs) generate SystemVerilog register-transfer-level (RTL) designs containing hardware Common Weakness Enumerations (CWEs). It creates ReFormAI: 30 design problems, each assigned one of 10 CWEs and one of three difficulty levels, with 500 regenerations from each of four LLMs. The resulting 60,000 designs are compiled and checked with Cadence Jasper formal verification, then labelled by vulnerability outcome. The abstract reports: “Our study reveals that approximately 60% of the hardware designs generated by LLMs are prone to CWEs, posing potential safety and security risks.” (Abstract, PDF p.1). The paper compares LLMs and difficulty levels; it does not evaluate Rust or Verus.

The central formal-verification result is an exhaustive property check, rather than a sample of simulation traces. The authors define formal verification as “an exhaustive verification technique that uses mathematical proof methods to verify if the design implementation matches design specifications.” (§II.C, PDF p.3) They report: “At least 60 % of the samples from the 60,000 SystemVerilog designs are found to contain vulnerabilities.” (§IV.B, PDF p.7) Table IV gives Pass@k (functionally correct designs divided by 10 CWEs × 500 generations) by model and difficulty: GPT-3.5-Turbo 0.567/0.311/0.324, Perplexity AI 0.186/0.157/0.258, Text-Davinci-003 0.587/0.269/0.355, and LLaMA 0.289/0.139/0.158 for basic/intermediate/advanced prompts (Table IV, PDF p.9). Inference: if the stated Pass@k formula is applied literally, each denominator is 5,000 generated designs per difficulty/model (10 CWE prompts × 500 runs). The paper also says Fig. 6 adds the non-compilable designs and that the pass rate then “drops significantly” (§IV.B, PDF p.9), which suggests Table IV and Fig. 5 leave them out and the denominators are smaller; the paper does not state the denominators.

technique 1: turn a CWE requirement into an exhaustive assertion

What it is. A design-under-verification (DUV) is converted into a mathematical model. A property written in SystemVerilog Assertions (SVA) is converted into a mathematical formula. The formal tool attempts to prove the formula over the model; failure yields a counterexample (CEX), while no CEX is treated as a proof of the property. The paper states: “The tool then converts these properties into mathematical formulas. In the next step, the tool tries to prove these mathematical formulas in the mathematical model of the DUV.” (§II.C, PDF p.4) The paper states the consequence: “If the properties do not hold, it is said to fail and a Counter Example (CEX) is generated by the tool to further debug. The absence of a CEX proves the properties to hold true.” (§II.C, PDF p.4)

When to use it. Use this technique when the safety or security condition can be stated over all legal input and state sequences, especially when simulation would only sample traces. The paper specifically targets ten hardware CWEs: reserved bits, write-once ordering, timing-sensitive comparisons, single-event-upset handling, debug lock bypass, late access control, alternate access paths, incorrect trusted-peripheral connections, missing security identifiers, and failure to clear sensitive values (Table I, PDF p.3).

How to do it.

1. Define the DUV interface and the intended CWE behavior in the prompt problem set (§III.A, PDF pp.4–5). Each difficulty level has ten prompts; for example, basic CWE-1209 is a register interface with a reserved bit, and advanced CWE-1276 is a SoC with a write-protected peripheral FIFO (Table III, PDF p.5).
2. Write an SVA property that observes the relevant clocked interface and states the required behavior (§III.C, PDF p.7). For the reserved-bit example, the paper gives: “( addr_in == ’h1 ) |-> ##1 ( data_out == ’h0 )” (Listing 4, §III.C, PDF p.7). The assertion is disabled during reset with disable iff (!rst_n_in) and sampled on the positive clock edge.
3. Compile and elaborate each generated RTL design, then run the property in Jasper through an automated script (§III, PDF p.4; §III.C, PDF p.7).
4. Record pass or fail in a log (§III.C, PDF p.7); a failed property yields a CEX (§II.C, PDF p.4). The authors report that the property passed the functionally correct GPT-3.5-Turbo output (Listing 2) and failed the incorrect one (Listing 3); the CEX pointed to line 21 as the root cause (Listings 2–4 and §III.C, PDF pp.6–7).
5. Label the design with the relevant CWE and store the result in the ReFormAI CSV (Fig. 1, §I, PDF p.2; §III, PDF p.4).

Verus form. Inference: A Rust/Verus analogue would model the RTL transition relation as an executable state struct and a one-step transition function, then state a spec fn describing the reserved-address rule and prove a postcondition for every transition. A proof function can establish that an input with address 1 produces zero on the next state; a loop or stream proof would use an invariant over successive transitions. The SVA clock implication itself does not carry over, because Verus reasons about Rust function calls and explicit old/new values rather than SystemVerilog event regions. Inference: The Verus proof would cover the modeled Rust implementation and would require an explicit assumption or model for reset and legal inputs.

Evidence and limits. The paper’s evidence is the automated Jasper pass/fail log over 60,000 designs, with a label “based on the vulnerabilities identified by formal verification with an unbounded proof” claimed in the contribution list (§I, PDF p.1). The authors name three fundamental components of a formal verifier: “a mathematical model, property language, and proof methods” (§II.C, PDF p.4). They warn that formal verification suffers from state-space explosion, which footnote 1 defines as the state-space growing exponentially as the number of state variables grows, and that buggy properties can produce false-positive proofs; they say they prepared the problem set and SVA properties to avoid state-space explosion and inconclusive proofs (§II.C, PDF p.4). They therefore say: “expertise and property reviews, followed by adequate formal coverage, must be considered when verifying a design using FV.” (§II.C, PDF p.4) Inference: A passing assertion proves only the encoded CWE condition under the model; it does not prove requirements omitted from the property.

technique 2: compose temporal properties for access-control attacks

What it is. For a protected FIFO, the authors express an attempted unauthorized write as a temporal sequence and require that the output remain stable. Listing 5 contains the sequence: “( ! rw_in ) [* 8 ] // make sure the fifo is empty ##1 rw_in && ( id_in != ’h03 ) && ( id_in != ’h04 ) && ( id_in != ’h07 ) // try to write ##1 ! rw_in |-> ##1 $stable ( data_out )” (Listing 5, §III.C, PDF p.7). The repetition operator establishes an empty FIFO, the next cycle attempts a write with an untrusted identifier, and the consequent checks that the observable output does not change.

When to use it. Use a sequence property when a CWE depends on an attack trace spanning multiple cycles, rather than one combinational relation. In the paper’s prompt, only IDs 0x3, 0x4, and 0x7 receive security level 1; other IDs must not write to the depth-eight FIFO (prompt query 2, §III.A, PDF p.5).

How to do it. First constrain or construct a known initial state (eight cycles with rw_in low). Next apply the unauthorized identifier and write request for one cycle. Then return to read mode and assert that data_out is stable on the following cycle. Finally run the assertion for every possible state and input allowed by the formal model (§III.C, PDF p.7).

Verus form. Inference: Represent FIFO contents, read/write indices, and security identity in a Rust state struct. Define a transition function whose write branch requires id == 3 || id == 4 || id == 7; otherwise it leaves the FIFO state unchanged. Prove, with a postcondition, that an unauthorized transition preserves the abstract FIFO sequence and output. To represent the eight-cycle precondition, use a sequence lemma or an invariant over a repeated transition; do not use an SVA repetition operator. Inference: The model must specify what “stable” means (same output value, same queue contents, or both), because Verus has no implicit clock event.

Evidence and limits. Listing 5 is an explicit property; the paper does not provide a separate count of failures for this property. Inference: The property can miss unauthorized effects that do not change data_out, such as metadata or timing changes, unless additional assertions observe them. The authors’ general warning about property bugs and false positives applies (§II.C, PDF p.4).

technique 3: generate many variants, then measure proof outcomes

What it is. The automated framework feeds each prompt to four models and regenerates the same prompt 500 times. The paper says: “Each of the query problems was regenerated 500 times with every LLM.” (§III.A, PDF p.6) Fig. 1 shows three outcomes for each generated design: compilation error, verification failed with a counterexample, or verification successful (§I, PDF p.2). Table IV’s caption defines “Pass = functionally correct” (PDF p.9). This produces 30 prompts × 500 runs × 4 models = 60,000 designs (§I, PDF p.1; §III.A, PDF p.6).

When to use it. Use repeated generation when measuring reliability or collecting training data, because one successful response is not representative of stochastic model output. Use a fixed prompt and fixed regeneration count to compare models and difficulty levels.

How to do it. Prepare ten basic, ten intermediate, and ten advanced CWE prompts (§III.A, PDF p.4). Include fixed inputs/outputs and module names so generic SVA and an automated harness can be reused; add the other instructions of §III.B (“Be creative!”, “Do not say I am sorry”, compile without errors, no comments, no explanation) (§III.B, PDF p.6). Generate 500 responses per prompt/model, compile them, run the applicable SVA set, and compute Pass@k as the number of functionally correct designs divided by the number of CWEs evaluated times n (§IV.B, PDF p.7).

Verus form. Inference: The analogous Rust experiment would generate candidate Rust functions, compile each with Verus, run the selected proof obligations, and define a pass fraction over a fixed candidate denominator. Compilation and proof success should remain separate columns, since the paper’s Fig. 6 shows that including non-compilable designs lowers pass rates. Inference: This evaluates candidate-generation reliability, not the soundness of Verus itself.

Evidence and limits. Table IV supplies the model/difficulty fractions, and Fig. 3 plots them by difficulty level (§IV.B, PDF p.9). The authors observe that more verbose descriptions often gave better results, and they say the unexpected result for advanced designs “might be attributed to the choice of problem set” and to the volume of training data (§IV.B, PDF p.9); in the conclusion they say a detailed description “can lead to relatively more functionally correct output, although this is not always the case” (§V, PDF p.10). Inference: The reported fractions should not be generalized to other model versions, sampling settings, prompts, or hardware designs.

technique 4: independent property review and coverage

The paper says: “To further remove the chances of false positives, we implemented the 4-eyes principle from [23].” (§IV.C, PDF p.10) It also states that the properties “take a reasonable runtime to prove in an industrial formal verification tool setup” and “can also be used to verify any generic RTL design based on the query prompt we prepared” (§IV.C, PDF p.9). The paper does not describe a formal-coverage measurement it performed. The authors explicitly limit the claim: “the target of our SVA properties was to primarily check the CWEs and it may happen that the designs that passed formal verification still have functionally incorrect code.” (§IV.C, PDF p.10)

Verus form. Inference: For Verus, an equivalent review process would have a second engineer inspect specifications, assumptions, invariants, and proof lemmas, followed by coverage of distinct security states and transitions. Inference: Passing proof obligations should be reported alongside the unproved environment, specification adequacy, and unsupported code boundary; a proof does not establish that the contract captures the product requirement.

what is proved, trusted, and reusable

The proved artifact is each SVA property over Jasper’s mathematical model of each compiled RTL design. The measured artifact is the pass fraction for each model, CWE, and difficulty. Inference: The trusted base includes the RTL-to-model translation, SVA semantics, Jasper implementation, compilation, reset and input assumptions, and the correctness of the properties themselves (§II.C and §IV.C). Inference: For VL, the direct reusable lesson is a property-first workflow: define a security contract, generate or translate code, compile it, prove the contract exhaustively, inspect CEX traces, and review both contract and coverage before accepting the result.

The authors say of the earlier LLM RTL benchmarks VGen, ChipGPT, RTLLM and Chip-Chat that “none of them evaluated the designs to check against CWEs” (§II.B, PDF p.3), that the VGen testbench “focused on unit testing and did not include exhaustive verification” (§II.B, PDF p.2), and Table II lists ReFormAI at 30 distinct and 60K total designs (PDF p.3). Inference: VL should not claim that merely compiling generated Rust or passing ordinary tests addresses this threat. The paper’s threat to agent-written verified Rust is indirect: CWE-like design omissions can survive code generation when the verifier checks only stated properties. Inference: Verus can reduce this threat only when VL writes security properties that observe all relevant state and transitions; the paper does not evaluate Rust, Verus, or software memory safety.

techniques for the catalog

• SVA-to-mathematical-model checking: express a CWE as a temporal SVA property and prove it exhaustively over a formal DUV model, using a counterexample on failure
• temporal attack-sequence assertion: compose initialization, unauthorized action, and post-state observations into one multi-cycle property
• repeated generation with formal labeling: regenerate each fixed prompt 500 times, compile and prove every candidate, and compute Pass@k over the stated denominator
• property review and coverage: independently review assertions and assess formal coverage because a buggy or incomplete property can produce a misleading pass Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Decreasing the number of unsuccessful queries is an important factor from an efficiency perspective since we also evaluate some paid LLMs.”): read the whole paper text and checked every quotation, number, table value, listing detail and section reference; corrected all PDF page references (the PDF has 11 pages and several were off by one to three), the “three fundamental components” wording, the Table IV page, and the 4-eyes/runtime passages; replaced the unsupported claim that denominators are 5,000 per cell with an Inference noting the paper does not state denominators and that Fig. 6 suggests Table IV excludes non-compilable designs; replaced the DOI-form link with the arXiv link printed in the paper text; marked the trusted-base list as Inference. Did not check: the cited works, the dataset itself, the figures’ heatmap values (text extraction of Figs. 4 to 6 is unreadable), and the Verus forms, which are the study’s own inferences.

Last edited: 2026-10-17