arXiv CSopen access

AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification

arXiv:2605.10712v1 [cs.SE] 11 May 2026

AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification Paschal Amusuo

Ricardo Calvo

Dharun Anandayuvaraj

Purdue University USA [email protected]

Purdue University USA [email protected]

Purdue University USA [email protected]

Taylor Le Lievre

Kevin Kolyakov

Elijah Jorgensen

Columbia University USA [email protected]

University of Waterloo Canada [email protected]

Purdue University USA [email protected]

Aravind Machiry

James C. Davis

Purdue University USA [email protected]

Purdue University USA [email protected]

Abstract

Keywords

Memory-safety errors remain a persistent source of zero-day vulnerabilities in low-level software. The problem is especially acute in embedded systems, where hardware protections are often limited and dynamic analysis is difficult to apply effectively. Memory-safety verification can provide stronger assurance by proving the absence of such errors or exposing violations when they exist. However, current verification workflows remain largely manual and require substantial specialized expertise, limiting their adoption in practice. We present AutoSOUP, a system for automating component-level memory-safety verification through Safety-Oriented Unit Proofs. We formalize these unit proofs as artifacts that encode verification choices (scope, loop bounds, and environment models) for verifying safety properties, and introduce three techniques for deriving them automatically. To overcome the limitations of existing automation approaches, we further introduce LLM-As-Function-Call, a hybrid architecture that combines deterministic program synthesis with LLMs to automate these techniques and produce justifiable unit proofs. We evaluate AutoSOUP by assessing its ability to automate memory-safety verification and expose vulnerabilities in verified components, and we characterize the assumptions and guarantees of the resulting proofs.

Memory-safety verification, Bounded Model Checking, Unit Proofs

CCS Concepts • Software and its engineering → Formal software verification; • Security and privacy → Software security engineering.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]. XXX ’26, United States © 2018 Copyright held by the owner/author(s). Publication rights licensed to ACM. ACM ISBN 978-1-4503-XXXX-X/2018/06 https://doi.org/XXXXXXX.XXXXXXX

ACM Reference Format: Paschal Amusuo, Ricardo Calvo, Dharun Anandayuvaraj, Taylor Le Lievre, Kevin Kolyakov, Elijah Jorgensen, Aravind Machiry, and James C. Davis. 2018. AutoSOUP: Safety-Oriented Unit Proof Generation for Componentlevel Memory-Safety Verification. In Proceedings of ACM Conference on XXX (XXX ’26). ACM, New York, NY, USA, 24 pages. https://doi.org/XXXXXXX. XXXXXXX

1

Introduction

Memory-safety errors remain a persistent source of zero-day exploits in low-level software [11, 56]. These errors enable denial-ofservice, data-theft, and remote-code-execution attacks [63]. Their risk is especially acute in embedded systems, which often lack standard hardware protections [9] and are difficult to analyze effectively with techniques such as fuzzing [57, 61]. After decades of recurring exploits and failures [27, 55, 56, 63], government agencies and industry organizations increasingly advocate or mandate methods that provide stronger memory-safety guarantees [7, 10, 19, 47]. Formal memory-safety verification can provide such guarantees, but existing techniques remain difficult to apply at scale. Deductive verification [34] can prove memory safety [45, 50], but it often requires specialized verification expertise, domain knowledge, and manual proof guidance [36, 39]. Bounded model checking (BMC) [5, 25] offers a more automated alternative, but whole-program BMC does not scale to large software systems. Recent industry case studies [24, 68, 70] favor a decomposition approach, wherein engineers verify components in isolation using “unit proofs” [15] that specify a component’s verification scope, loop bounds, and environment models. However, constructing these unit proofs remains challenging and error-prone: engineers must choose scopes, bounds, and models that are strong enough to expose genuine memory-safety errors, but constrained enough to keep verification tractable. AWS’s report [24] suggests a substantial engineering cost, with a verification rate of 1500 lines of code in one person-month. No existing

XXX ’26, 2026, United States

Amusuo et al.

1 2 3 4 5 6 7 8 9 10

size_t get_record_count() { // Complex logic returning ↩→ [0,10] return count; } int handle_record(size_t i) { ... } void process_record(uint8_t ↩→ *dst) {

Figure 1: AutoSOUP automatically identifies the functions to include in the verification scope, loop bounds, and environment model for which the resulting component-level memory-safety verification completes and provides useful guarantees of memory safety.

work automates these choices in a way that supports practical component-level memory-safety verification for real C software. To address this gap, this paper introduces AutoSOUP (Figure 1), a hybrid system for constructing unit proofs that enable useful memory-safety verification for embedded software. The key idea is the notion of memory-safety-oriented unit proofs: reusable verification artifacts that prioritize the scope, bounds, and environment models needed to preserve safety-relevant memory behavior, rather than faithfully model all execution behavior. AutoSOUP derives these choices using three techniques: resource-aware scope widening, property-guided loop-bound selection, and context-aware environment refinement. To make this automation reliable and generalizable, AutoSOUP uses a hybrid LLM-as-function-call architecture [42, 51]. Rather than asking an LLM to synthesize an entire proof artifact, AutoSOUP uses deterministic program-analysis workflows to drive the construction process and invokes LLMs for controlled tasks with explicit validation criteria. As a result, each verification choice incorporated into the unit proof is tied to a specific algorithmic objective and validated before use. We evaluate AutoSOUP on four embedded real-time operating systems. AutoSOUP successfully produces valid unit proofs and verifies 93% of candidate targets, exposing 66.7% of evaluated vulnerabilities—38.7% and 28.5% more than the next bestperforming baselines. Each of our techniques contributes to the final verification results by improving the derived bounds and environment models. Moreover, AutoSOUP’s unit proofs use simpler and more general environment assumptions than fidelity-oriented expert-written counterparts while achieving comparable verification outcomes. In summary, this paper makes the following contribution: • We propose safety-oriented unit proofs, a formulation of component-level memory-safety verification artifacts; and techniques for scope, bounds, and environment models. • We operationalize the LLM-as-function-call architecture for automating auditable and justifiable unit-proof construction. • We design and implement AutoSOUP to automatically construct safety-oriented unit proofs for C-language software. • We evaluate AutoSOUP on 177 components from four widely used embedded operating systems and report its utility, effectiveness, and cost for memory-safety verification.

size_t n = get_record_count(); // Bug!! should be i < n for (size_t i = 0; i <= n; ↩→ ++i) { dst[i] = handle_record(i); assert(isValidObject(dst)); assert(ObjectSize(dst) > i); }

11 12 13 14 15 16 17 18 19 20 21 22 23

1

Scope = {process_record, handle_record}. Loop bound: {process_record.0: ↩→ 11}

↩→ 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17

}

18

void caller() { int dst[10]; process_record(dst); }

19 20 21

size_t get_record_count_m1() { uint8_t ret = nondet_int(); assume(ret < 10); return ret; } size_t get_record_count_m2() { uint8_t ret = nondet_int(); assume(ret <= 10); return ret; } void harness(void) { uint8_t dst_size = ↩→ nondet_int(); uint8_t *dst = ↩→ malloc(dst_size); assume(dst != NULL); process_record(dst); }

Listing 1: Left: Program instrumented with memory-safety properties and its calling context. Right: Unit proof with verification choices for the process_record component.

Significance: AutoSOUP is the first system to automate memorysafety verification through the construction of unit proofs that enable component-level bounded model checking. Our results show that AutoSOUP applies to substantial real-world codebases, provides useful memory-safety assurance, and exposes real security vulnerabilities. Automated memory-safety verification can be practical enough to integrate into software-development workflows and help prevent memory-safety vulnerabilities before deployment.

2 Background 2.1 Memory-Safety and Verification Memory safety means that all memory accesses performed by a program are valid under the semantics of the language [63]. Accesses must refer to memory that has been properly allocated, remain within the bounds of the target object, and occur during that object’s lifetime [16, 38, 58]. A memory safety error violates these conditions [58, 67], either spatially or temporally [63]. Violations of these conditions cause memory corruption and remain a major source of software failures, security vulnerabilities, and exploits [6, 8, 56, 69]. Memory-safety verification uses formal methods to establish that a program cannot perform invalid memory accesses, subject to explicit modeling assumptions. Compared with testing and bugfinding techniques, its goal is not only to expose errors, but also to provide assurance that specified classes of memory violations are absent within the verified program. Two approaches have been especially important for memorysafety verification. Deductive verification proves memory safety by reasoning over program behavior using specifications of program state, memory, and invariants [21, 45]. It can provide strong guarantees over all executions, but it requires substantial expertise and manual proof effort. In contrast, Bounded Model Checking (BMC) [41] checks memory-safety properties automatically by exploring executions within explicit bounds.

AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification

2.2

Bounded Model Checking and Unit Proofing

Tools for Bounded Model Checking (BMC) [43, 46] specify program properties as Boolean assertions over variable states, automatically check these assertions using constraint-solving tools, and report counterexample traces [53]. For memory-safety verification, BMC instruments the program with memory-safety assertions, unrolls loops and recursion, translates the resulting bounded program into a satisfiability formula, and applies constraint solvers. If no violating trace exists, BMC proves that the instrumented properties hold. If a violation exists, BMC returns a counterexample. Listing 1 illustrates how BMC can be used to verify a component’s memory safety. An engineer verifies a connected subset of a program to keep verification tractable (verification scope); for example, they may verify process_record and handle_record while excluding the get_record_count callee. The engineer must also choose the maximum number of times to unroll loops (loop bounds), because BMC operates only on loop-free programs, and provide assumptions about the behavior of callers and callees outside the chosen scope (environment model). These choices—verification scope, loop bounds, and environment model—are encoded in a unit proof, shown on the right of Listing 1. For example, Program Lines 15–16 assert that dst points to a valid allocated object and that the object is large enough for the indexed write; the unit proof then determines the scope, bounds, and assumptions under which BMC checks those assertions.

2.3

Verification Choice Fidelity

The guarantees afforded by BMC depend on the choices encoded in a unit proof. For example, on Line 13 of Listing 1, setting the bound for the program loop to 1 may suffice to check that dst is valid, but not that all indexed accesses are valid. Similarly, the overlyconstrained model get_record_count_m1 (Unit Proof Lines 4–8) masks the violation, whereas get_record_count_m2 exposes it. We define verification choice fidelity (VCF) as the degree to which these choices reflect the behavior of the real system. Formally, we characterize fidelity as 𝑉𝐶𝐹 = ⟨𝑆𝑐 𝑓 , 𝐵 𝑓 , 𝐸 𝑓 ⟩, where 𝑆𝑐 𝑓 denotes verification-scope fidelity, 𝐵 𝑓 denotes loop-bound fidelity, and 𝐸 𝑓 denotes environment-model fidelity. This notion is related to model fidelity in systems modeling [54] and execution fidelity in firmware rehosting [33, 61] but focuses on choices that affect bounded model checking. Higher-fidelity choices preserve implementation behavior and can support stronger guarantees. Lower-fidelity choices simplify semantics, reducing development cost. Many existing approaches to component-level BMC are fidelityoriented. They rely on experts to encode detailed knowledge of the system [24], infer artifacts from specifications [70] or unit tests [68], or refine artifacts manually using verification results [12]. Such proofs can provide strong guarantees, but require deep knowledge of the component and its role in the surrounding program. It is therefore hard to create them automatically. Other approaches rely on automatable choices, such as fixed function-level scopes [23, 40], uniform loop bounds [64], or environment models inferred by program analysis [21, 40]. However, these methods focus on restricted property sets, limiting their use for memory-safety verification; or require expert guidance to apply

XXX ’26, 2026, United States

them in real software. This gap motivates methods that derive verification choices automatically while preserving the safety-relevant behavior needed for useful memory-safety verification guarantees.

3

Problem Statement

Our goal is to automate component-level memory-safety verification through the creation of unit proofs. This requires identifying verification choices that provide meaningful memory-safety guarantees while keeping verification tractable. We formalize the problem as follows. Given a software system 𝑆, a component entry point 𝐶𝑒 , a set of memory-safety properties 𝑄, and a resource budget 𝑅, automatically construct a unit proof 𝑈 (𝑉 ) that encodes the verification choices 𝑉 = (𝑆𝑐 , 𝐵, 𝐸), where 𝑆𝑐 ⊆ 𝑆 is a connected set of functions rooted in 𝐶𝑒 , 𝐵 maps each loop reachable in 𝑆𝑐 to a maximum unrolling bound, and 𝐸 is an environment model that defines assumptions for functions outside 𝑆𝑐 . The resulting proof should allow BMC to verify 𝑄 conclusively within 𝑅, while ensuring the result reflects the memory safety of the verified functions 𝑆𝑐 in the original system 𝑆. In Listing 1, this means constructing the unit proof on the right so that BMC exposes the memory-safety error on the left. No existing work solves this problem automatically. Prior work on memory-safety verification either requires experts to define these choices [24, 68, 70], or uses fixed scope, loop bounds and program-analysis-inferred environment models [21, 23, 40] that require expert adaptation to real software. In this work, we automatically derive verification choices and construct executable unit proofs for real C software.

3.1

Success Criteria

A unit proof should support useful memory-safety guarantees. Building on [12], we distinguish five requirements: (1) Structural validity: It should compile and verify the intended component identified by the entry point 𝐶𝑒 . For example, the unit proof in Listing 1 must verify process_record. (2) Conclusiveness [12]: It should produce a verification result within the resource budget 𝑅. The result may be either a proof that the target memory-safety properties 𝑄 hold, or a counterexample showing the states and execution trace that violate them. (3) Verification coverage [12]: It should verify as much reachable code in its verification scope as possible. We define verification coverage as the proportion of included lines that are exercised and checked by the unit proof. This metric is analogous to line coverage in unit testing and fuzzing. (4) Result validity: It should make verification choices that neither encode spurious violations nor mask feasible memory-safety violations within the checked scope, bounds, and assumptions. Reported violations should correspond to real memory-safety errors. (5) Maintainability: Unit proofs are reusable and auditable artifacts. As a result, their format should be familiar to software engineers so that the verification choices can be inspected and refined and the unit proofs maintained as the code evolves.

XXX ’26, 2026, United States

Automatically generating unit proofs that satisfy these requirements is non-trivial because the requirements can conflict. For example, a system may improve conclusiveness with shallow bounds or simple models, but reduce verification coverage or result validity. Conversely, techniques optimized for result validity may compromise coverage and tractability, or yield unit proofs too complex for engineering teams. Prior work [12] introduced conclusiveness and verification coverage to assess unit proof completeness. We add structural validity, result validity, and maintainability to capture risks introduced by automation: a generated unit proof may verify the wrong entry point, encode choices that produce invalid results, or become too complex for maintainers to inspect and refine.

3.2

System and Threat Model

System model: We consider software systems 𝑆 written in the C language, which is often used for embedded software development. We focus on components that process untrusted inputs from external interfaces, e.g., network channels, since these interfaces form primary attack surfaces. We exclude programs in which memory references can be shared across processes (threads or tasks) and that are prone to race conditions, because they violate the linear execution assumptions of standard bounded model checking tools. Threat model: We consider attackers who can supply inputs through external interfaces and thereby trigger violations of the target memory-safety properties 𝑄. Such inputs may flow directly to memory-safety sinks or indirectly influence control/data flow so that the component reaches an unsafe memory state.

4

AutoSOUP Design and Implementation

We designed AutoSOUP to automate component-level memorysafety verification through the creation of unit proofs (Figure 2).

4.1

Key Ideas

AutoSOUP explores two ideas: safety-oriented derivation of verification choices (§4.1.1) and LLM-as-function-call automation (§4.1.2). 4.1.1 Memory-Safety-Oriented Unit Proofs. We introduce memorysafety-oriented unit proofs: unit proofs whose verification choices 𝑉 = (𝑆𝑐 , 𝐵, 𝐸) are tailored to the instrumented memory-safety properties 𝑄. Unlike fidelity-oriented unit proofs, which choose 𝑉 to approximate the program’s behavior, memory-safety-oriented unit proofs choose 𝑉 to preserve the behavior needed to prove or refute 𝑄 within the resource budget 𝑅. This gives a safety-oriented interpretation of each choice: 𝑆𝑐 should include code that contributes checkable memory-safety behavior; 𝐵 should be large enough to cover or expose property-relevant loop behavior; and 𝐸 should expose possible violations while excluding infeasible ones. AutoSOUP realizes this interpretation through three techniques. 1. Resource-aware scope widening: Prior fidelity-oriented approaches rely on experts to select verification scopes [24, 64]. Automating this selection is difficult because it requires reasoning about both interfunction semantics and verification cost. However, prior work [12] suggests that memory-safety verification often does not require preserving all inter-function behavior. We therefore treat scope selection as a resource-aware coverage problem rather than a full semantic-modeling problem. AutoSOUP

Amusuo et al.

widens 𝑆𝑐 incrementally, using simple models for functions that remain outside the current scope. This lets the verifier check memorysafety properties in the included code without requiring precise models for every external callee. A widened scope is useful only if it increases the code and properties checked while remaining within the resource budget 𝑅. This reframing avoids the need to predict the globally best scope in advance: AutoSOUP starts with a small, tractable scope and expands only as needed. 2. Property-guided loop-bound refinement: Prior fidelity-oriented approaches rely on experts to define loop bounds [24] or loop invariants [37]. Other approaches use uniform bounds for all loops [64], which can be expensive and still miss memory-safety-relevant behavior. We instead treat loop-bound selection as a property-guided refinement problem. The intuition is that many memory-safety properties depend on local program states and are affected most directly by nearby loops. Thus, AutoSOUP refines 𝐵 only for loops whose iterations affect the reachability or violation of instrumented memory-safety properties (e.g., the loop on Line 13 of Listing 1). 3. Context-aware environment refinement: Environment models create a different tension: permissive models expose possible memorysafety violations, but can also produce infeasible counterexamples; overly constrained models avoid spurious reports, but can mask real violations. We therefore extend counterexample-guided environment refinement [40] with context validation. AutoSOUP starts with permissive models that expose possible violations, infers preconditions that suppress infeasible violations, and then validates those preconditions against calling contexts in the original program. Preconditions satisfied by the surrounding program become explicit assumptions in 𝐸; violated preconditions identify feasible memorysafety errors. In Listing 1, this process distinguishes assumptions needed for process_record to be memory safe from assumptions violated by the actual implementation of get_record_count(). Together, these techniques derive 𝑆𝑐 , 𝐵, and 𝐸 in a propertydirected way. The resulting unit proofs 𝑈 (𝑉 ) are safety-oriented because they preserve behavior relevant to the target safety properties rather than all program behavior. Although we focus on memory safety, the same formulation applies to safety properties expressible as Boolean predicates over program states.

4.1.2 Automating Safety-Oriented Unit Proofs. Automating safetyoriented unit proofs requires both project-specific reasoning and auditable verification choices. Program analysis can enforce syntactic and semantic constraints, but struggles with build configuration, local code idioms, and scalable semantic inference. LLMs can handle such project-specific reasoning, but unconstrained generation is unsuitable because invalid scopes, bounds, or environment assumptions can invalidate the resulting verification guarantees. AutoSOUP balances reliability and generalizability with an LLMas-function-call architecture. Deterministic algorithms control the proof-construction workflow and define the objective of each step. When a step requires semantic code understanding or projectspecific adaptation, AutoSOUP delegates a bounded task to a toolequipped LLM agent. Program-analysis modules then validate the returned artifact before it is incorporated into the unit proof.

AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification

XXX ’26, 2026, United States

Figure 2: AutoSOUP system diagram. AutoSOUP connects safety-oriented unit-proof construction with LLM-as-function-call automation. Across all stages, deterministic workflows derive the verification choices 𝑉 = (𝑆𝑐 , 𝐵, 𝐸), delegate bounded semantic tasks to LLM agents, and validate returned artifacts before incorporating them into the unit proof.

4.2

Resource-Aware Scope Widening

Resource-aware scope widening derives 𝑆𝑐 by incrementally adding semantically related code that may contain checkable memorysafety properties, retaining expansions only while verification remains within the resource budget 𝑅. We use source files as the unit of expansion because related functions are often colocated, making file-level widening a coarse but useful approximation of semantic locality. The algorithm proceeds in three steps (cf. §C.1). Step 1: Initialize the scope, bounds, and input model: AutoSOUP initializes 𝑆𝑐 with the file containing 𝐶𝑒 , sets all loop bounds to 1, and constructs a type-directed input model for 𝐶𝑒 : primitive arguments receive unconstrained symbolic values, while pointer arguments receive valid allocated objects containing unconstrained values. An LLM agent synthesizes this input model and recovers the build configuration needed to compile the entry point’s parent file, including headers, include paths, macros, and mandatory project configurations. AutoSOUP accepts the result only if deterministic checks confirm that the proof compiles, calls 𝐶𝑒 , and introduces no preconditions beyond the intended type-directed initialization. Step 2: Model external calls: AutoSOUP identifies call edges that cross the current scope boundary and replaces their targets with simple type-based models. Primitive returns are modeled as unconstrained symbolic values, while pointer returns are modeled as valid allocated objects to avoid irrelevant invalid-pointer states that inflate the solver state space. An LLM agent synthesizes and integrates these models from the recovered call graph and return types; deterministic checks confirm that the resulting unit proof remains structurally valid. Step 3: Widen the scope: AutoSOUP checks the provisional unit proof against the configured time, memory, and file-depth budgets. If verification remains within 𝑅, it widens 𝑆𝑐 by adding files that define previously modeled callees, selecting among ambiguous definitions

by longest common path prefix to the in-scope caller. An LLM agent recovers build configuration for newly added files, and AutoSOUP repeats external-call modeling and scope widening until verification exceeds 𝑅 or no additional files can be added. Algorithm 1: Property-guided loop-bound and model refinement. Given a verification instance with initial loop bounds, refine the bounds, build configuration, and environment models to cover property-relevant code and expose loop-dependent memory-safety violations. Input: Verification scope 𝑆𝑐 , properties 𝑄, loop bounds 𝐵, environment model 𝐸, resource budget 𝑅 Output: Refined loop-bound map 𝐵, refined environment model 𝐸 1 Function PropertyGuidedRefinement(𝑆𝑐 , 𝑄, 𝐵, 𝐸, 𝑅) // Step 1: Cover property-relevant code 2 𝐺 ← UncoveredPropertyBlocks(𝑆𝑐 , 𝑄, 𝐵, 𝐸 ) 3 foreach 𝑔 ∈ 𝐺 do 4 𝜌 ← ClassifyCoverageGap(𝑔, 𝑆𝑐 , 𝐵, 𝐸 ) 5 (𝐵 ′ , 𝐸 ′ ) ← RepairCoverageGap(𝑔, 𝜌, 𝐵, 𝐸 ) 6 if ValidCoverageRefinement(𝑆𝑐 , 𝑄, 𝐵 ′ , 𝐸 ′ , 𝑅) then 7 (𝐵, 𝐸 ) ← (𝐵 ′ , 𝐸 ′ )

15

// Step 2: Expose loop-dependent property violations 𝐿 ← LoopsWithIncompleteUnwinding(𝑆𝑐 , 𝐵, 𝐸 ) foreach ℓ ∈ 𝐿 do 𝑃ℓ ← LoopDependentProperties(ℓ, 𝑄 ) if 𝑃ℓ ≠ ∅ then 𝑛 ← MinBoundToViolate(ℓ, 𝑃ℓ ) 𝐵 ′ ← 𝐵; 𝐵 ′ [ℓ ] ← max(𝐵 [ℓ ], 𝑛) if ValidBoundRefinement(𝑆𝑐 , 𝑄, 𝐵 ′ , 𝐸, 𝑅) then 𝐵 ← 𝐵′

16

return (𝐵, 𝐸 )

8 9 10 11 12 13 14

XXX ’26, 2026, United States

4.3

Property-Guided Loop & Model Refinement

Property-guided refinement derives the bounds 𝐵 and model refinements 𝐸 to exercise memory-safety-relevant behavior in 𝑆𝑐 . It uses the instrumented properties 𝑄 as the oracle for deciding which refinements matter. It honors the resource budget 𝑅 by increasing bounds or refining models only to cover property-relevant code or expose violations. Our technique has two steps (Algorithm 1). Step 1: Cover property-relevant code: A violation of 𝑞 ∈ 𝑄 can be exposed only if the line containing 𝑞 is reached and checked. Coverage can be blocked by three factors: insufficient loop bounds, missing compile-time configuration, or external-call side effects not captured by return-value-only models. AutoSOUP runs BMC in coverage mode, identifies uncovered property blocks, and uses an LLM agent to classify the blocking factor. It then applies the corresponding local repair: increase the relevant loop bound, adjust the configuration, or refine the external model to write unconstrained symbolic values through affected pointer arguments. The taxonomy and repair rules constrain the agent so that refinements remain local and aligned with the technique. A refinement is accepted only if the unit proof remains semantically valid, the target block becomes covered, and overall verification coverage does not decrease. Step 2: Expose loop-dependent property violations: Covering a property does not imply that the current loop bounds can expose its violation. AutoSOUP inspects loops from the coverage report whose current bounds were insufficient for complete unwinding. For each such loop, it uses an LLM agent to determine whether the loop can affect violation of a nearby memory-safety property and, if so, to estimate the minimum bound likely to expose a violation. The prompt constrains this estimation using local program semantics, such as memory-region size, access stride, allocation constraints, and loop guards. A proposed bound is accepted only if it modifies the intended loop bound and preserves structural validity, conclusiveness, and verification coverage. If the bound causes verification to exceed 𝑅, AutoSOUP reports the bound but does not apply it.

4.4

Context-Aware Env. Model Refinement

Property-guided refinement in §4.3 maximizes exposure of violations of 𝑄 using permissive models 𝐸. However, violations found under permissive models may be infeasible in the broader system 𝑆. For example, the assertion on Program Line 15 in Listing 1 is violated if the input model provides a null pointer, even if the actual caller provides a statically allocated array. Our context-aware environment refinement separates infeasible violations (caused by overly permissive environment assumptions) from genuine memory-safety errors. This technique operates in two steps (Algorithm 2). Step 1: Infer approximate weakest preconditions: Following counterexample-guided environment refinement, AutoSOUP infers preconditions that suppress reported violations of memory-safety properties. These preconditions need not be logically weakest, since weakest-precondition inference is often computationally expensive [23]. Instead, they should be weak enough to preserve safe states while strong enough to suppress the target violation. AutoSOUP parses the verification report to extract each violated property 𝑞 ∈ 𝑄, its location loc(𝑞), and its counterexample witness

Amusuo et al.

Algorithm 2: Context-aware environment model refinement. The algorithm infers approximate preconditions for violated memory-safety properties, validates them against calling contexts, and reports caller-feasible violations as memory-safety errors. Input: Software system 𝑆, component entry point 𝐶𝑒 , Environment model 𝐸, Property violations 𝑄 𝑣 Output: Refined environment model 𝐸, memory-safety error set M 1 Function ContextAwareEnvRefinement(𝑆, 𝐶𝑒 , 𝐸, 𝑄 𝑣 ) 2 M←∅ 3 W ← ParseViolationReport(𝑄 𝑣 ) // W contains tuples (𝑞, 𝑤 (𝑞) ) 4 foreach (𝑞, 𝑤 (𝑞) ) ∈ W do 5 𝜙 ← InferApproxPrecondition(𝐸, 𝑞, 𝑤 (𝑞) ) 6 (𝜙 ′ , B ) ← ValidatePrecondition(𝑆, 𝐶𝑒 , 𝑞, 𝜙 ) 7 𝐸 ← 𝐸 ∪ {𝜙 ′ } 8 M←M∪B 9

return (𝐸, M )

Function ValidatePrecondition(𝑆, 𝐶𝑒 , 𝑞, 𝜙 ) B ← ∅; 𝜙 ′ ← 𝜙 12 C ← CallsitesOf(𝐶𝑒 , 𝑆 ) 13 foreach 𝑐 ∈ C do 14 𝜓𝑐 ← PathConstraints(𝑐, 𝑆 ) 15 if 𝜓𝑐 ̸ |= 𝜙 ′ then 16 𝜙ˆ ← WeakenPrecondition(𝜙 ′ ,𝜓𝑐 ) ˆ 𝑞) then 17 if SatisfiesProperty(𝜙, 18 𝜙 ′ ← 𝜙ˆ

10

11

19 20

21

else B ← B ∪ { (𝑞,𝜓𝑐 , 𝜙 ′ ) } return (𝜙 ′ , B )

𝑤 (𝑞). For each tuple (𝑞, loc(𝑞), 𝑤 (𝑞)), an LLM agent infers a precondition that keeps loc(𝑞) covered but suppresses the violation of 𝑞. The prompt guides the agent to identify the violated condition, propagate it backward through local dataflow and path constraints, and stop at the external model or input responsible for the value. The agent can inspect witnesses, navigate code, and test candidate preconditions. A candidate is accepted only if it suppresses the target violation without reducing structural validity, conclusiveness, coverage, or the number of checked properties. Step 2: Validate and refine against calling contexts: An inferred precondition may exclude feasible caller states that would not violate 𝑞, or it may reveal that the surrounding program can trigger the violation. AutoSOUP therefore validates each accepted precondition against calling contexts in 𝑆. Using a pre-indexed call graph, it identifies callsites of 𝐶𝑒 and implementations of modeled functions. For each context, an LLM agent identifies path constraints reaching the callsite or implementation and checks whether those constraints imply the inferred precondition. Validation has three outcomes. If a calling path violates the precondition but still satisfies 𝑞, the agent weakens and revalidates the precondition. If the precondition holds across the checked contexts, it becomes an explicit assumption in 𝐸. And of course, if a calling path violates the precondition and triggers 𝑞, AutoSOUP reports

AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification

the path as a feasible memory-safety error in 𝑆. These assumptions make the generated unit proof auditable: the component is verified only under the preconditions recorded in its environment model.

4.5

Guarantees and Limitations

We discuss the guarantees and limitations of AutoSOUP. 4.5.1 Guarantees. Unit proofs generated by AutoSOUP provide bounded formal guarantees of memory safety, backed by BMC. They establish that no execution from the component entry point violates a verified memory-safety property, provided the execution stays within the scope, loop bounds, and assumptions encoded in the unit proof. This is the same form of guarantee provided by expertwritten unit proofs [24]; its strength depends on the correctness and completeness of the encoded verification choices. AutoSOUP strengthens these choices by expanding safety-relevant scope, increasing bounds needed to expose property-relevant behavior, and making environment assumptions explicit. 4.5.2 Limitations. Three limitations constrain these guarantees. First, AutoSOUP uses LLMs for project-specific reasoning. To reduce unreliable outputs, deterministic workflows issue bounded tasks and validate outputs before incorporating them into the unit proof. As program analyses improve, these modules can be replaced with deterministic techniques. Second, AutoSOUP relies on static analysis to recover call graphs for scope widening and precondition validation. Imprecision, especially around indirect calls, may cause AutoSOUP to miss relevant call edges; engineers can reduce this risk by providing accurate application call graphs. Third, AutoSOUP widens scope at file granularity. Large files may exceed 𝑅 and prevent wider scopes from being explored.

4.6

Implementation

We implement AutoSOUP in 15463 lines of Python and 1230 lines of prompts. Resource-aware scope widening uses 1227 lines of Python and 292 prompt lines; property-guided loop-bound refinement uses 775 lines of Python and 316 prompt lines; and context-aware environment refinement uses 1091 lines of Python and 479 prompt lines. Bounded model checking: AutoSOUP uses the ANSI-C Bounded Model Checker (CBMC) [46] as its verification backend. AutoSOUP can be used with most bounded model checkers with memorysafety instrumentation, as elaborated in §E. Program-analysis modules: AutoSOUP integrates components for deterministic program analysis. We use CBMC’s goto-instrument to extract call-graph and symbol information from the compiled verification scope, which lets AutoSOUP check that the unit proof invokes the target entry point and identify undefined external callees during scope widening. We use libclang to locate function-pointer calls in the verification scope, allowing AutoSOUP to constrain them to selected models or concrete targets. We use cscope to index the software system 𝑆, recover project-level call relations, locate candidate function definitions, and identify calling contexts for validating inferred preconditions.

XXX ’26, 2026, United States

LLM-driven modules: AutoSOUP implements its LLM-driven modules using the OpenAI Python SDK [2] and LiteLLM [1]. The OpenAI SDK provides access to the GPT-family models used in our evaluation, while LiteLLM supports additional providers, including open-source and self-hosted models. We expose three tools to the agents: (i) a containerized terminal tool lets agents inspect source files, build logs, and verification reports; (ii) a cscope-based navigation tool supports code search, definition lookup, and call-graph queries; and (iii) a unit-proof validation tool analyzes the compiled unit and verification report after each proposed change to confirm the proof compiles, calls the target entry point, satisfies the requested refinement task, and does not reduce line coverage or the number of covered or verified properties.

5

Evaluation

We structure our evaluation with four research questions: • RQ1: Can AutoSOUP generate useful unit proofs for memorysafety verification? • RQ2: Are memory-safety-oriented unit proofs effective at exposing memory-safety vulnerabilities? • RQ3: How do AutoSOUP’s safety-oriented techniques contribute to its performance and cost? • RQ4: Do AutoSOUP-generated unit proofs differ from those of experts?

5.1

Evaluation Setup

Subjects: Following prior works on validating embedded software [12], we evaluate AutoSOUP using four widely-used open-source embedded operating systems: Zephyr RTOS, RIOT OS, Contiki-NG and FreeRTOS. These operating systems are substantial (Table 7), including task management, IPC, networking, and storage subsystems. We considered including downstream embedded applications but their source code is often not publicly available [61]. Vulnerability selection: To assess AutoSOUP’s effectiveness to expose security vulnerabilities, we identify and recreate 60 known CVEs in selected subjects. To ensure reliable recreation, we extract CVEs affecting each software from the National Vulnerability Database and identify the first 20 CVEs where the vulnerable function still exists and the security advisory provided details of the vulnerability sink and the fixing commit. The FreeRTOS CVEs in our dataset did not provide the fixing commits and were excluded. We re-expose each CVE by applying a patch to reverse the changes in the identified fixing commit. For each CVE, we also record the vulnerability type, affected function, and sink location, to enable exposure detection. Verification targets: Component-level verification require entry points through which the components would be verified. We identify these entry points in three steps. First, we include the 57 functions affected by the 60 selected CVEs 1 . Second, to assess generalizability beyond known vulnerable functions, we randomly select an additional 100 functions across the four embedded OSes. First, we identify five modules in each operating system that handle untrusted data, such 1 3 functions contained 2 CVEs each

XXX ’26, 2026, United States

as bluetooth, network and USB modules. For each module, we perform an attack surface analysis to identify sources of untrusted data and the functions that process them. We select 5 functions per module, yielding an additional 25 functions per OS. Finally, we select 20 FreeRTOS functions with expert-written harnesses to enable head-to-head comparison in RQ4. Our component entry point set thus has a total of 177 entry points. Table 7 shows the parent modules containing the selected entry points. Baselines.: We compare AutoSOUP against two categories of baselines. First, we compare against alternative methods for producing unit proofs, including expert-written FreeRTOS proofs and proofs generated by vanilla coding agents (GPT Codex). This comparison evaluates differences in verification choices and resulting outcomes. Second, we compare against memory-safety verification techniques, using Seeker [64], a recent open-source verifier for memory safety of open programs. Seeker is the closest prior system to our setting. We defer conceptual comparisons with other verification methods to §6.2. Hardware and AI models: We run experiments on dedicated servers (32 virtual CPUs, 188GB of RAM). We use gpt-5.3-codex through their API for our evaluation, as it ranked among the best AI models for coding [4] at time of study. We configure with the default temperature (1.0) and reasoning effort (high). To assess generalizability to open-source models, we compare against Minimax M2.5 and GLM-5, two leading open-source models for coding [4]. AutoSOUP configuration: We evaluate two AutoSOUP configurations that differ in the maximum scope level used by resource-aware scope widening (§4.2). Scope-1 (S1) widens only to scope level of one (parent file containing entry point). Scope-2 (S2) uses depth two (parent file and all adjacent files). For each verification run, we use a 30-minute timeout, a practical budget under which most component-level verification tasks complete. We use the default configurations for the baseline techniques.

5.2

RQ1: Are AutoSOUP’s Results Useful?

§3.1 identifies five properties that unit proofs must satisfy to support useful verification guarantees: structural validity, conclusiveness, verification coverage, result validity and maintainability. RQ1 evaluates the first three and last properties. We defer result validity to RQ2. 5.2.1 Method. We evaluate RQ1 on the full set of selected component entry points and use both AutoSOUP configurations. We run AutoSOUP-S1 on all verification targets and AutoSOUP-S2 only on targets with recreated CVEs because its wider scope increases generation and verification cost. We terminate generation runs that exceed 24 hours. For each generated unit proof, we measure whether generation completes, whether the proof compiles, whether it is semantically valid, and how long verification takes. We then measure the verification outcome: the total lines of code in functions statically reachable from the unit proof, the proportion of those lines covered under the proof bounds and assumptions, the total number of instrumented memory-safety properties, and the proportion of those properties verified.

Amusuo et al.

We also measure the cost and size of each unit proof. For cost, we record total generation time and API cost. For size, we record proof size in lines of code, including both harness function and all function models. Following prior work on unit testing [28, 62], we use unit proof size as a proxy for maintainability. For comparison, we run Codex and Seeker on the verification targets with recreated vulnerabilities and report the corresponding measurements when available. For Codex, we use a prompt that states the goal of unit proof creation and the success criteria in §3.1, but gives no specific guidance on how to derive verification choices. This baseline tests whether a general-purpose AI coding agent can independently produce unit proofs that support useful memory-safety guarantees. For Seeker, we extract the compilation configurations from AutoSOUP-generated unit proofs and the scripts provided in the Seeker artifact to compile and verify the target file. To validate our setup, we sampled benchmarks from the Seeker codebase and confirmed that our instrumented programs matched the artifact versions and produced identical verification results. 5.2.2 Result. Unit proof validity: Table 1 compares the validity, verification outcomes, and generation cost of unit proofs produced by AutoSOUP and CodexUP. AutoSOUP produced substantially more valid unit proofs than Codex: 93%, 89.5% and 91.7% for scope levels 1 and 2 and the randomly selected targets, respectively, compared with 31.6% for CodexUP. In Seeker, of the 57 targets, 12 (21.1%) returned an error while 23 (40.4%) timed out. Most Codex proofs were structurally invalid because Codex often failed to compile or verify the target, due to missing compilation, incomplete environment models or initially large loop bounds, and instead created simpler copies to verify. Seeker more often returned errors when it could not process the source file and timed out more often because it assigned a uniform bound of 20 to all loops and did not create valid environment models that reduce the state space. This shows that AutoSOUP’s structured refinement and validation are necessary to produce unit proofs that compile, reach the target, and complete verification. The lower success rate of AutoSOUP-S2 relative to AutoSOUP-S1 is expected. Increasing the scope level adds more adjacent code to the verification target, which increases program size, state space, and verification time. Verification outcomes and assurance: Among valid unit proofs, AutoSOUP, at scope levels 1 and 2, covered and verified 88.2% and 155% more lines of code compared to Codex’ 57.8 lines of code. Data from Seeker is excluded as it does not provide coverage report. Table 1 also provides the number of total and verified properties as reported by the tool. However, because it counts the properties in non-covered code as verified because no violation was produced, Codex substantially lower coverage led to a higher number of reported verified properties. These results show that AutoSOUP also outperforms frontier coding agents in generating unit proofs that achieves better verification coverage and provides stronger memory-safety assurances. The remaining uncovered code was primarily caused by statements that were not statically reachable from the generated unit proof, even when their enclosing functions were reachable. This effect becomes more pronounced as scope level increases and the

S1

S2

Codex

Random

Num Targets Struct. valid (%) Verification completes (%) Generation succeeds (%)

57 93% 96.5% 93.0%

57 89.5% 91.2% 78.9%

57 31.6% 70.2% 98.2%

84 2 91.7% 76.2% 75%

Verification time (s) Avg compon. size (loc) Avg covered size (loc)

137.9 126.1 108.8

249.1 418.9 147.4

37.4 132.5 57.8

17.7 107.7 88.8

Avg num. properties (#) Avg prop. verified (#) Avg reported errors (#)

382.4 369.5 4.7

1187.2 1185.3 3.2

468.3 465.1 1.6

243.2 242.7 1.2

Avg gen. time (min) Avg API cost ($)

129.8 3.0

363.7 5.9

10.1 0.8

45.0 1.8

Avg proof size (loc)

34.1

40.1

50.7

27.3

proof includes functions from adjacent files. AutoSOUP nevertheless achieved higher coverage than CodexUP because its generated proofs are designed to admit all valid reachable states. By contrast, CodexUP often introduced restrictive assumptions in its unit proofs that excluded feasible states, reducing both code coverage and the corresponding number of properties checked. Unit proof generation cost: Generating AutoSOUP unit proofs required 2.16 and 6.06 hours on average for scope levels 1 and 2, respectively, and cost $3 and $5.9 in API usage. These costs are higher than CodexUP, but they produce substantially more valid and useful proofs. They are also modest relative to prior humandriven unit proofing effort, where verifying 1,500 lines of code required about one person-month of work [24]. Figure 3 shows that the cost of AutoSOUP was distributed across the unit proofs. Overall, increasing the scope level from 1 to 2 increased the size of verified code, together with the development costs. Our data also showed these costs correlated closely with component size: larger component sizes took longer to verify, which increased the iterative-refinement-based development time.

5.3

RQ2: Does AutoSOUP Find Vulnerabilities?

§3.1 requires unit proofs to produce valid memory-safety results: their verification outcomes should reflect genuine memory-safety vulnerabilities in the verified component. RQ2 evaluates whether unit proofs generated by AutoSOUP expose known memory-safety vulnerabilities during verification. 5.3.1 Method. We evaluate RQ2 on verification targets with recreated vulnerabilities. We compare AutoSOUP against the baselines using the proportion of vulnerabilities exposed and the root causes of any missed vulnerabilities.

XXX ’26, 2026, United States

Verification Time (s)

500 400 300 200 100 0

S1

S2

Codex

3500 3000 2500 2000 1500 1000 500 0

2500

30

2000

25

API Cost ($)

Metric

Generation Time (min)

Table 1: Comparison of unit proofs produced by AutoSOUP at scope level 1 and 2 and by CodexUP. Random represents targets selected to assess generalizability. We report results from Seeker baseline in the prose. Below the double-line, we consider only the unit proofs from successful runs for each method.

Component Coverage (loc)

AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification

1500 1000 500 0

S1

S2

Codex

S1

S2

Codex

20 15 10 5

S1

S2

Codex

0

Figure 3: Distribution of program reachable LOC, verification time, development time, and API cost for the RQ1 unit proofs.

Counting a vulnerability as exposed is non-trivial. During contextaware environment refinement (§4.4), AutoSOUP infers underapproximate preconditions that suppress reported property violations. A precondition inferred for one violation may also suppress other violations that share the same root cause. As a result, the violation location recorded by AutoSOUP may differ from the CVE sink location defined in §5.1, even when both correspond to the same vulnerability. We therefore count a vulnerability as exposed if any of the following holds: (i) AutoSOUP reports a memory-safety error at the recorded CVE sink, and the inferred precondition can be violated at the component callsite; (ii) AutoSOUP reports a memory-safety error at a different sink, the inferred precondition can be violated at the callsite, and violating it would also trigger a property violation at the recorded CVE sink; or (iii) AutoSOUP reports a memory-safety error at the recorded CVE sink without inferring a precondition that suppresses the error. We identify the first and third cases automatically by comparing recorded CVE sink locations with the memory-safety errors reported by AutoSOUP. We identify the second case manually by checking whether removing the inferred precondition produces a property violation at the recorded CVE sink. Finally, we compare the proportion of CVEs exposed by AutoSOUP, Codex, and Seeker, and manually categorize missed vulnerabilities to understand limitations of our techniques and those of the underlying bounded model checker. 5.3.2 Result. Exposure of known CVEs: Table 2 reports the proportion of recreated CVEs exposed by each method and summarizes the reasons for non-exposure. AutoSOUP-S1 and AutoSOUP-S2 exposed 66.7% and 65% of CVEs, respectively. In contrast, Codex and Seeker exposed only 28.3% and 41.7% 3 . These results show that AutoSOUP exposes substantially more known vulnerabilities than both a general-purpose coding agent and the prior verification baseline. 3 For Seeker, due to limited information it provides, we counted any violation corre-

sponding to the CVE sink line as exposure

XXX ’26, 2026, United States

Amusuo et al.

Table 2: Exposure rate of known vulnerabilities. S1 and S2 represents AutoSOUP configured at scope levels one and two respectively. Metric

S1

S2

Codex

Seeker

Number of CVEs Number exposed Unexploitable

60 40 6

60 39 5

60 17 1

60 25 -

Compilation error Structural invalidity Resource exhaustion

3 0 1

4 0 2

6 2 17

-

Limited scope Limited loop unwinding Inaccurate env. model

3 1 2

0 3 0

2 0 14

-

Unsupported sink BMC field granularity

2 2

2 4

1 0

-

Root causes of non-exposure: We classify non-exposure into three categories. First, some unit proofs were invalid or inconclusive, preventing verification from producing a useful result. Second, some proofs used insufficient verification choices, such as scopes that excluded vulnerability-relevant paths, loop bounds that were too small, or environment assumptions that ruled out vulnerable states. Third, some cases were limited by the underlying bounded model checker, even when the relevant code and triggering conditions were present. For AutoSOUP-S1, missed CVEs were primarily caused by limited scope, CBMC limitations, or vulnerabilities that were not triggerable from the project context. The scope-related misses were resolved by AutoSOUP-S2, showing that scope widening is important for exposing vulnerabilities whose triggers cross file boundaries. The CBMC limitations appeared in two forms. First, CBMC reports a spatial memory-safety violation only when an access leaves the allocated object. However, for structs, AutoSOUP’s propertyguided loop-bound analysis computes the bound needed to overflow the destination field, not necessarily the containing object. Thus, when a write overflows a struct field but remains within the same allocated struct object, CBMC does not report a violation. Second, 2 vulnerabilities was missed because they required semantics that CBMC did not model. One was a memory-leak, missed because the corresponding custom deallocator is not supported. The second required timer semantics for exposure. In cases we tagged unexploitable, AutoSOUP reached the CVE sink and inferred the relevant precondition, but the precondition was valid in the component’s calling context, either due to upstream constraints or default program configurations. Codex missed CVEs mainly because its unit proofs were invalid, inconclusive, or over-constrained. Its ad hoc proof generation often produced scopes that did not support conclusive verification or assumptions that excluded vulnerable states. We could not investigate Seeker misses because no coverage report or unit proofs were produced. Exposure of new vulnerabilities: During unit proof generation, AutoSOUP scope levels 1 and 2 reported 63 and 99 potential

Table 3: New vulnerabilities discovered using AutoSOUP. Each count is reported as Total (Contiki-NG, Zephyr, RIOT). Vulnerability Type

Count

Out-of-bound write Out-of-bound read Undefined shift behavior Null pointer dereference

9 (5, 1, 2) 7 (2, 3, 2) 2 (1, 1, 0) 1 (1, 0, 2)

Total

20 (9, 5, 6)

memory-safety violations where inferred preconditions were violated. After reviewing a subset of these reports, we confirmed 20 new externally triggerable vulnerabilities (Table 3). Nine of these are out-of-bound write vulnerabilities, with potentials to cause denial of service or arbitrary code execution. Another 7 are out-ofbound reads, which can potentially lead to information disclosure attacks. Details of one vulnerability is in §F. We reported all confirmed vulnerabilities to the corresponding maintainers. One has been fixed and assigned a CVE. Another 4 were fixed without CVE assignment because maintainers considered exploitation to require prior compromise of the downstream embedded application, which was outside their threat model. The remaining reports are still under investigation. Sample out-of-bound write vulnerability in RIOT-OS: Listing 4 illustrates a vulnerability in RIOT-OS nanocoap.c discovered by AutoSOUP. AutoSOUP first generated a harness for the root function coap_opt_put_uri_pathquery, initializing buf and string as nondeterministic pointers with unconstrained sizes. Stage 2 refined the proof bounds and models until verification reached the vulnerable memcpy on Line 33, where a memcpy write violation was exposed. Finally, Stage 3 inferred a precondition on the input-buffer length that would eliminate the violation, but the validator traced the constrained string back to the nanocoap_sock_post public API and found no corresponding length check. AutoSOUP therefore classified the precondition as violable in the real environment and reported the memcpy out-of-bounds write vulnerability.

5.4

RQ3: Ablation of AutoSOUP’s Techniques?

We ablate the techniques used to derive our safety-oriented unit proofs: verification scope, loop bounds, and environment models. 5.4.1 Method. During the RQ1 runs, we save a unit proof snapshot after each technique completes. For each snapshot, we also record the technique’s execution time and API cost. We use these snapshots to measure how each technique changes the unit proof. Specifically, we measure changes in verification scope, loop bounds, and environment models. We then execute each snapshot and measure the resulting verification coverage, the number of reachable memory-safety properties, and the proportion of those properties verified. This allows us to isolate how each verification choice affects verification outcomes and to estimate the marginal cost of each technique. Finally, we compare generalizability to open-source models. We execute the 37 targets in RIOT and Contiki-NG using AutoSOUP

AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification

Table 4: Stage-wise contribution of AutoSOUP’s scope, loopbound, and environment-modeling stages to harness structure, verification behavior, development time, and API cost. Metric

Stage 1

Stage 2

Stage 3

Harness Size (LOC) Proof Size (LOC)

6.613 18.74

7.795 25.76

21.64 44.81

# Functions In Scope # Custom Loop Bounds # Variable Models # Function Models Avg Function Model Size (LOC)

17.78 0.004 0.044 1.351 2.954

18.84 0.909 0.068 1.938 3.602

17.34 0.842 3.424 2.119 5.402

Component Size (LOC) Verification Coverage (LOC) Total Properties Verified Properties

209.8 94.06 542.8 412.3

220.8 139.6 580.0 412.8

196.3 115.8 539.0 531.6

Generation Time (min) API Cost ($)

6.054 0.296

39.99 0.743

141.5 2.602

configured at scope level 1 and equipped with the selected opensource models, Minimax M2.5 and GLM-5. Similar to RQ1, we measure the validity of produced unit proofs, their verification outcomes and the generation cost. 5.4.2 Result. Contribution and cost of each technique: Table 4 summarizes how each AutoSOUP stage changes the unit proof, affects verification outcomes, and contributes to generation cost. Overall, the results show that the three techniques are complementary: each stage introduces a distinct class of verification choices and improves a different aspect of the final proof. Stage 1 (resource-aware scope widening) determines the reachable functions included in the proof and introduces models for undefined functions. These choices remain largely unchanged in later stages. This stage is also the cheapest because it is implemented primarily using deterministic program analysis. Stage 2 (property-guided loop refinement) increases the number of per-loop bounds. This expands the explored behavior of the component, which increases both verification coverage and the number of reachable memory-safety properties. At this stage, up to 71.04% of reachable properties on average are violated under the unconstrained environment, showing that loop unwinding exposes safety-relevant behaviors that must later be checked or constrained. This stage takes 39.99 minutes and costs $0.743 on average. Stage 3 (context-aware environment refinement) primarily refines the variable and function models to eliminate infeasible executions while preserving safety-relevant behavior. This allows 98.63% of reachable properties to be verified and produces the environment assumptions under which the verification holds. It is also the most expensive because AutoSOUP infers and validate preconditions for reported property violations one by one. Together, these results explain AutoSOUP’s performance. Scope widening determines what code is analyzed, loop unwinding exposes safety-relevant behaviors within that code, and environment

XXX ’26, 2026, United States

refinement separates feasible violations from behaviors ruled out by the component context. Generalizability to open-source models: Table 6 in §G evaluates AutoSOUP with open-source models. Across 37 test cases, unit proof generation succeeded for 78.4% with GLM-5 and 48.6% with Minimax M2.5, compared to 93% with GPT-5.3-Codex. Their average costs were $4.9 and $0.7, respectively, compared to $3 for GPT-5.3-Codex. These results show that AutoSOUP can generalize to open-source models, but its performance depends on model capability. As open-source models improve, we expect corresponding gains in AutoSOUP’s performance with them.

5.5

RQ4: AutoSOUP vs. Expert-Written Proofs?

RQ4 compares unit proofs generated by AutoSOUP with existing FreeRTOS proofs. We restrict this analysis to FreeRTOS because it is the only evaluation subject with unit proofs developed by project maintainers. 5.5.1 Method. We first compare verification choices and outcomes quantitatively. For verification choices, we measure proof size, verification-scope size, distinct loop bounds, and the number of variable and function models. For outcomes, we measure verification time, component size, verification coverage, the number of verified properties, and the number of violated properties. We then qualitatively analyze the environment models using the taxonomy from prior work [12]. Variable models fall into four categories: null-pointer preconditions (p != NULL), pointer-offset preconditions (p2 = p1 + offset), variable-constant preconditions (var >= CONSTANT), and variable-variable preconditions (var1 >= var2). Function models fall into three categories: Type 1 models with no preconditions, Type 2 models with preconditions only on return values, and Type 3 models with preconditions on inputs or global variables. We classify each model and compare the assumptions encoded by AutoSOUP-generated and expert-written proofs. Finally, we conduct a case study of three randomly selected functions with varying proof sizes. We inspect their loop bounds and environment models to explain observed differences and their implications for verification. 5.5.2 Result. Quantitative comparisons: Figure 4 compares the verification choices and outcomes. Overall, AutoSOUP-generated unit proofs are smaller, use smaller verification scopes, include more variable models and fewer function models, and achieve comparable verification coverage. This difference stems from two design choices. First, AutoSOUP uses preconditions to constrain environment variables, whereas FreeRTOS proofs often call project functions to initialize or constrain state, such as the proof for vDHCPProcess using prvCreateDHCPSocket to initialize DHCP sockets. Second, FreeRTOS proofs often replace same-file callees with function models and reuse shared function models across proofs. In contrast, AutoSOUP keeps same-file callees in scope and creates models only for functions outside the entry point’s parent file, resulting in fewer function models.

XXX ’26, 2026, United States

Amusuo et al.

Figure 4: Comparing AutoSOUP’s unit proofs with expertwritten ones. Top measures verification choices. Bottom measures verification outcomes. Table 5: Categorization of environment models from unit proofs. Data is aggregated from 20 unit proofs each. Top section represent variable model categories, while bottom section is for function models. Model category

Expert-written

AutoSOUP

pointer-not-null pointer-offset variable-constant variable-variable

65 2 38 3

62 1 70 8

Type 1 models Type 2 models Type 3 models

58 18 0

23 19 2

Qualitative comparisons: Table 5 shows the distribution of model categories. Although AutoSOUP introduces 90% more preconditions than the expert-written proofs, most are simple: nonnull pointer constraints or fixed upper and lower bounds on environment variables needed for memory safety. Thus, AutoSOUPgenerated environment models are comparable to expert-written models, making them auditable and maintainable. Case studies comparing specific unit proofs are in §D. Sample AutoSOUP-generation unit proof is in Listing 2.

6

Discussion and Related Work

We discuss implications for practitioners and researchers and compare our work to related lines of research.

6.1

Discussion

Guarantees, cost, and practicality.: AutoSOUP occupies a practical middle ground in the software-verification landscape. Deductive verification [34] can prove rich functional and memory-safety properties, but requires substantial specifications, annotations, and proof effort. Expert-written unit proofs for bounded model checking [24, 70] can provide useful memory-safety guarantees, but require experts to define scopes, loop bounds, inputs, and environment models. Automated analyzers such as Infer [20] operate

at lower cost, but target narrower classes of properties than the bounded memory-safety guarantees studied in this paper. In contrast, AutoSOUP automates these choices and makes them explicit, while providing bounded memory-safety guarantees. RQ2 (§5.3) shows that this tradeoff is useful in practice: AutoSOUP exposes 66.7% of recreated CVEs and reports the assumptions under which each verified component is memory safe. It is also substantially cheaper than prior industry experience where expert-written proofs take one engineer-month to cover 1500 lines of code. Although AutoSOUP does not replace stronger verification methods for safetycritical certification, it lowers the cost of memory-safety verification for broader software teams. Integration in developer workflow.: AutoSOUP makes componentlevel verification more practical for low-level software projects. RQ1 (§5.2) shows that it can generate unit proofs and verify components in realistic embedded software. This supports a practical shift-security-left workflow [60]: developers can obtain formal evidence about component memory safety during development, when defects are cheaper to diagnose and fix [3]. Our aeronautics industry partners noted that this capability is especially valuable in long development cycles, where products may take up to seven years to complete. In addition, by making environment assumptions explicit in the unit proof, AutoSOUP also exposes the interface contracts under which a component is memory safe. This will help developers identify and validate the caller-side obligations whose violation often leads to component-interface vulnerabilities [49]. Implications and future directions.: AutoSOUP also illustrates a path for trustworthy AI-assisted software engineering. As developers increasingly use AI agents to generate and modify code, tools like AutoSOUP can provide machine-checkable evidence that generated components are memory safe under explicit assumptions. Its LLMas-function-call architecture also allows model improvements to strengthen LLM-driven subtasks without weakening the deterministic orchestration and validation framework. This matters because formal guarantees depend on the assumptions encoded in the verification task [36], and automatically judging the correctness of these assumptions remains an open problem [15]. Looking forward, extending AutoSOUP from component-level memory-safety verification to broader project-level assurance requires three advances. First, loop unwinding should be combined or replaced with loop invariant generation [59] to expose vulnerabilities whose required bounds exceed the resource budget. Second, whole-project verification requires techniques that select effective component entry points, reduce bound or environment refinement cost with program analysis, and compose component-level results into project-level guarantees [17, 23]. Third, generalizing beyond memory safety requires techniques that automatically infer system and security properties that can be verified using bounded model checking. Novel AI-driven techniques can help infer them from existing specifications, comments, and unit tests [48], then encode them as safety properties for verification.

6.2

Related Work

We situate our work within three lines of research.

AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification

(1) Automating component-level BMC: Prior work has explored automating bounded model checking through compositional verification [23, 40]. These techniques decompose programs along call-graph or control-flow edges, infer preconditions under which each fragment is safe, and discharge the resulting obligations using assume-guarantee reasoning [26]. However, it remains unclear whether these techniques scale to real-world systems with large components, diverse coding patterns, and complex inter-component relationships. Other work targets open programs, where components have undefined dependencies, and refines their environments using expert-provided precondition templates [29, 64]. Our evaluation shows that such templates can be imprecise and incomplete, compromising the resulting verification guarantees. In contrast, AutoSOUP automates industry-adopted component-level verification workflow and derives the scope, loop bounds, and environment models needed for practical memory-safety verification. The derived choices can also support compositional and open-program verification methods. (2) LLMs and the verification-oracle problem: Large language models are increasingly used to automate software-verification tasks, including tactic generation for deductive verification [35, 44, 72], precondition and loop-invariant inference for bounded model checking [59], and repair of verification failures [65]. In these settings, the LLM usually acts as the main driver and the task has a clear success oracle: the generated artifact is accepted if verification succeeds. AutoSOUP addresses a harder oracle problem because successful verification is not sufficient when unjustified choices of scope, bounds, or environment assumptions can make verification succeed without providing appropriate guarantees. Thus, AutoSOUP uses LLMs as assistants inside program-analysis-driven workflows: deterministic orchestrators issue small tasks aligned with specific algorithms and validate each result before incorporating it into the unit proof. This architecture may also apply to other security and software-engineering tasks, such as fuzzing, where AI-generated harnesses can compile and achieve coverage yet still produce false crashes or invalid results [13, 71, 74]. (3) Security vulnerability detection: AutoSOUP complements static analysis [22, 31] and dynamic analysis [14, 73, 75] for vulnerability detection. Unlike these techniques, AutoSOUP produces auditable unit proofs that specify the scope, bounds, and assumptions under which a component is memory safe. These proofs can be rechecked to obtain bounded formal evidence of memory safety. Because AutoSOUP operates statically on source code, it is also well suited to embedded software, where dynamic analysis is often limited by emulation, rehosting, and peripheral-modeling challenges [18, 32, 33, 52, 76].

7

Conclusion

AutoSOUP makes component-level bounded model checking more practical by automatically constructing unit proofs that verify a component’s memory safety, while documenting the bounds and environment assumptions for the guarantees. It combines LLMs with a deterministic, incremental workflow to balance utility with reliability. Our evaluation on four substantial embedded RTOSes suggest automated harness generation as an incremental path toward security guarantees for real-world embedded software.

XXX ’26, 2026, United States

Acknowledgments Davis and Machiry acknowledge funding from Rolls Royce. Amusuo and Anandayuvaraj acknowledge funding from the Qualcomm Innovation Fellowship. All authors acknowledge API credits from OpenAI.

AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification

References [1] LiteLLM - getting started | liteLLM. URL: https://docs.litellm.ai/docs/. [2] openai/openai-python. original-date: 2020-10-25T23:23:54Z. URL: https://github. com/openai/openai-python. [3] Software defect reduction top 10 list. URL: https://www.computer.org/csdl/ magazine/co/2001/01/r1135/13rRUwgyOg9. [4] SWE-bench leaderboards. URL: https://www.swebench.com/index.html. [5] IEC 61508-3: Functional safety of electrical/electronic/programmable electronic safety-related systems – part 3: Software requirements, 2010. Second edition. [6] Channel File 291 Incident RCA is Available | CrowdStrike, 2025. URL: https: //www.crowdstrike.com/en-us/blog/channel-file-291-rca-available/. [7] DARPA Guide for Formal Methods to Deliver Resilient Systems for Proposals, 2025. URL: https://defencescienceinstitute.com/wp-content/uploads/2025/01/ Resilient_Systems_Best_Practices_Guide_-_1-9-2025.pdf. [8] Project Zero: 0day "In the Wild", 2025. URL: https://googleprojectzero.blogspot. com/p/0day.html. [9] Ali Abbasi, Jos Wetzels, Thorsten Holz, and Sandro Etalle. Challenges in designing exploit mitigations for deeply embedded systems. In 2019 IEEE European Symposium on Security and Privacy (EuroS&P), pages 31–46, 2025. URL: https://ieeexplore.ieee.org/abstract/document/8806725, doi:10.1109/EuroSP. 2019.00013. [10] Alex Rebert, Ben Laurie, Murali Vijayaraghavan, and Alex Richardson. Securing tomorrow’s software: the need for memory safety standards, 2025. URL: https:// security.googleblog.com/2025/02/securing-tomorrows-software-need-for.html. [11] Alex Rebert, Chandler Carruth, Jen Engel, and Andy Qin. Safer with Google: Advancing Memory Safety, 2024. URL: https://security.googleblog.com/2024/10/ safer-with-google-advancing-memory.html. [12] Paschal C. Amusuo, Owen Cochell, Taylor Le Lievre, Parth V. Patil, Aravind Machiry, and James C. Davis. Do unit proofs work? an empirical study of compositional bounded model checking for memory safety verification. In 2026 IEEE/ACM 48th International Conference on Software Engineering. URL: http://arxiv.org/abs/ 2503.13762, arXiv:2503.13762[cs], doi:10.48550/arXiv.2503.13762. [13] Paschal C. Amusuo, Dongge Liu, Ricardo Andres Calvo Mendez, Jonathan Metzman, Oliver Chang, and James C. Davis. FalseCrashReducer: Mitigating false positive crashes in OSS-fuzz-gen using agentic AI. URL: http://arxiv.org/abs/ 2510.02185, arXiv:2510.02185[cs], doi:10.48550/arXiv.2510.02185. [14] Paschal C. Amusuo, Ricardo Andrés Calvo Méndez, Zhongwei Xu, Aravind Machiry, and James C. Davis. Systematically detecting packet validation vulnerabilities in embedded network stacks. In 2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 926–938, 2023. ISSN: 2643-1572. URL: https://ieeexplore.ieee.org/abstract/document/10298483, doi:10.1109/ASE56229.2023.00095. [15] Paschal C. Amusuo, Parth V. Patil, Owen Cochell, Taylor Le Lievre, and James C. Davis. A unit proofing framework for code-level verification: A research agenda. In 2025 IEEE/ACM 47th International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER), pages 36–40. URL: https://ieeexplore.ieee.org/ abstract/document/11023946, doi:10.1109/ICSE-NIER66352.2025.00013. [16] Arthur Azevedo de Amorim, Cătălin Hriţcu, and Benjamin C. Pierce. The meaning of memory safety. In Lujo Bauer and Ralf Küsters, editors, Principles of Security and Trust, pages 79–105. Springer International Publishing. doi:10.1007/9783-319-89722-6_4. [17] S. Bensalem, M. Bozga, T.-H. Nguyen, and J. Sifakis. Compositional verification for component-based systems and application. IET Software, 4(3):181–193, 2010. Publisher: IET Digital Library. URL: https://digital-library.theiet.org/content/ journals/10.1049/iet-sen.2009.0011, doi:10.1049/iet-sen.2009.0011. [18] Moritz Bley, Tobias Scharnowski, Simon Wörner, Moritz Schloegel, and Thorsten Holz. Protocol-aware firmware rehosting for effective fuzzing of embedded network stacks. In Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security, CCS ’25, pages 4484–4498. Association for Computing Machinery. URL: https://dl.acm.org/doi/10.1145/3719027.3765125, doi:10.1145/3719027.3765125. [19] Bob Lord. The Urgent Need for Memory Safety in Software Products | CISA, September 2025. URL: https://www.cisa.gov/news-events/news/urgent-needmemory-safety-software-products. [20] Cristiano Calcagno and Dino Distefano. Infer: An automatic program verifier for memory safety of c programs. In Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi, editors, NASA Formal Methods, pages 459–465. Springer. doi:10.1007/978-3-642-20398-5_33. [21] Cristiano Calcagno, Dino Distefano, Peter O’Hearn, and Hongseok Yang. Compositional shape analysis by means of bi-abduction. In Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL ’09, pages 289–300. Association for Computing Machinery, 2025. URL: https: //dl.acm.org/doi/10.1145/1480881.1480917, doi:10.1145/1480881.1480917. [22] Qi Alfred Chen, Zhiyun Qian, Yunhan Jack Jia, Yuru Shao, and Zhuoqing Morley Mao. Static detection of packet injection vulnerabilities: A case for identifying attacker-controlled implicit information leaks. In Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, CCS ’15, pages

XXX ’26, 2026, United States

388–400. Association for Computing Machinery, 2015. URL: https://dl.acm.org/ doi/10.1145/2810103.2813643, doi:10.1145/2810103.2813643. [23] Chia Yuan Cho, Vijay D’Silva, and Dawn Song. BLITZ: Compositional bounded model checking for real-world programs. In 2013 28th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 136–146, 2013. URL: https://ieeexplore.ieee.org/abstract/document/6693074, doi:10.1109/ASE.2013. 6693074. [24] Nathan Chong, Byron Cook, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, and Mark R. Tuttle. Code-level model checking in the software development workflow. In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Software Engineering in Practice, ICSE-SEIP ’20, pages 11–20. Association for Computing Machinery, 2020. URL: https://dl.acm.org/doi/10.1145/ 3377813.3381347, doi:10.1145/3377813.3381347. [25] Edmund Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 19(1):7–34, 2001. doi:10.1023/A:1011276507260. [26] Jamieson M. Cobleigh, Dimitra Giannakopoulou, and Corina S. PĂsĂreanu. Learning assumptions for compositional verification. In Hubert Garavel and John Hatcliff, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 331–346. Springer, 2003. doi:10.1007/3-540-36577-X_24. [27] CrowdStrike, Inc. External technical root cause analysis — channel file 291. Technical report, CrowdStrike, August 2024. Accessed January 2026. URL: https://www.crowdstrike.com/wp-content/uploads/2024/08/Channel-File291-Incident-Root-Cause-Analysis-08.06.2024.pdf. [28] Ermira Daka, José Campos, Gordon Fraser, Jonathan Dorn, and Westley Weimer. Modeling readability to improve unit tests. In Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2015, pages 107–118. Association for Computing Machinery. URL: https://dl.acm.org/doi/10.1145/ 2786805.2786838, doi:10.1145/2786805.2786838. [29] Ankush Das, Shuvendu K. Lahiri, Akash Lal, and Yi Li. Angelic verification: Precise verification modulo unknowns. In Daniel Kroening and Corina S. Păsăreanu, editors, Computer Aided Verification, pages 324–342. Springer International Publishing, 2015. doi:10.1007/978-3-319-21690-4_19. [30] James C Davis, Sophie Chen, Huiyun Peng, Paschal C Amusuo, and Kelechi G Kalu. A guide to stakeholder analysis for cybersecurity researchers. arXiv preprint arXiv:2508.14796, 2025. [31] Dino Distefano, Manuel Fähndrich, Francesco Logozzo, and Peter W. O’Hearn. Scaling static analyses at facebook. Communications of the ACM, 62(8):62–70, 2019. URL: https://dl.acm.org/doi/10.1145/3338112, doi:10.1145/3338112. [32] Andrew Fasano, Tiemoko Ballo, Marius Muench, Tim Leek, Alexander Bulekov, Brendan Dolan-Gavitt, Manuel Egele, Aurélien Francillon, Long Lu, Nick Gregory, Davide Balzarotti, and William Robertson. SoK: Enabling security analyses of embedded systems via rehosting. In Proceedings of the 2021 ACM Asia Conference on Computer and Communications Security, ASIA CCS ’21, pages 687–701. Association for Computing Machinery. URL: https://dl.acm.org/doi/10.1145/3433210. 3453093, doi:10.1145/3433210.3453093. [33] Bo Feng, Alejandro Mera, and Long Lu. {P2IM}: Scalable and hardwareindependent firmware testing via automatic peripheral interface modeling. In 29th USENIX Security Symposium (USENIX Security 20), pages 1237–1254, 2020. URL: https://www.usenix.org/conference/usenixsecurity20/presentation/feng. [34] Jean-Christophe Filliâtre. Deductive software verification. 13(5):397–403. doi: 10.1007/s10009-011-0211-0. [35] Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. Baldur: Wholeproof generation and repair with large language models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2023, pages 1229–1241. Association for Computing Machinery, 2023. URL: https://dl.acm.org/doi/10. 1145/3611643.3616243, doi:10.1145/3611643.3616243. [36] Pedro Fonseca, Kaiyuan Zhang, Xi Wang, and Arvind Krishnamurthy. An empirical study on the correctness of formally verified distributed systems. In Proceedings of the Twelfth European Conference on Computer Systems, EuroSys ’17, pages 328–343. Association for Computing Machinery, 2017. URL: https: //dl.acm.org/doi/10.1145/3064176.3064183, doi:10.1145/3064176.3064183. [37] Mikhail Y. R. Gadelha, Hussama I. Ismail, and Lucas C. Cordeiro. Handling loops in bounded model checking of c programs via k-induction. 19(1):97–114. doi:10.1007/s10009-015-0407-9. [38] Michael Hicks. What is memory safety? - the PL enthusiast. URL: http://www.plenthusiast.net/2014/07/21/memory-safety/. [39] Li Huang, Sophie Ebersold, Alexander Kogtenkov, Bertrand Meyer, and Yinling Liu. Lessons from Formally Verified Deployed Software. CoRR, March 2023. URL: http://arxiv.org/abs/2301.02206, doi:10.48550/arXiv.2301.02206. [40] Franjo Ivančić, Gogul Balakrishnan, Aarti Gupta, Sriram Sankaranarayanan, Naoto Maeda, Hiroki Tokuoka, Takashi Imoto, and Yoshiaki Miyazaki. DC2: A framework for scalable, scope-bounded software verification. In 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), pages 133–142. ISSN: 1938-4300. URL: https://ieeexplore.ieee.org/abstract/ document/6100046, doi:10.1109/ASE.2011.6100046.

XXX ’26, 2026, United States

[41] Franjo Ivančić, Zijiang Yang, Malay K. Ganai, Aarti Gupta, and Pranav Ashar. Efficient SAT-based bounded model checking for software verification. 404(3):256– 274. URL: https://www.sciencedirect.com/science/article/pii/S0304397508002223, doi:10.1016/j.tcs.2008.03.013. [42] Yuchen Ji, Ting Dai, Zhichao Zhou, Yutian Tang, and Jingzhu He. Artemis: Toward accurate detection of server-side request forgeries through LLM-assisted inter-procedural path-sensitive taint analysis. 9:128:1349–128:1377. URL: https: //dl.acm.org/doi/10.1145/3720488, doi:10.1145/3720488. [43] kani. Getting started - the kani rust verifier, 2024. URL: https://model-checking. github.io/kani/. [44] Saketh Ram Kasibatla, Arpan Agarwal, Yuriy Brun, Sorin Lerner, Talia Ringer, and Emily First. Cobblestone: A divide-and-conquer approach for automating formal verification. URL: https://arxiv.org/abs/2410.19940v4, doi:10.1145/3744916. 3773178. [45] Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, SOSP ’09, pages 207–220. Association for Computing Machinery, 2009. URL: https://dl.acm.org/doi/10.1145/1629575.1629596, doi: 10.1145/1629575.1629596. [46] Daniel Kroening and Michael Tautschnig. CBMC – c bounded model checker. In Erika Ábrahám and Klaus Havelund, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 389–391. Springer, 2014. doi:10. 1007/978-3-642-54862-8_26. [47] Latham & Watkins LLP. New EU product liability directive comes into force. Client alert / legal briefing, December 2024. Accessed January 2026. URL: https://www.lw.com/admin/upload/SiteAttachments/New-EUProduct-Liability-Directive-Comes-Into-Force.pdf. [48] Thanh Le-Cong, Bach Le, and Toby Murray. Can LLMs reason about program semantics? a comprehensive evaluation of LLMs on formal specification inference. In Wanxiang Che, Joyce Nabende, Ekaterina Shutova, and Mohammad Taher Pilehvar, editors, Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 21991–22014. Association for Computational Linguistics. URL: https://aclanthology.org/2025.acl-long.1068/, doi:10.18653/v1/2025.acl-long.1068. [49] Hugo Lefeuvre, Vlad-Andrei Bădoiu, Yi Chen, Felipe Huici, Nathan Dautenhahn, and Pierre Olivier. Assessing the impact of interface vulnerabilities in compartmentalized software. In Proceedings 2023 Network and Distributed System Security Symposium. Internet Society. doi:10.14722/ndss.2023.24117. [50] Shaofeng Li, Lei Qiao, and Mengfei Yang. Memory state verification based on inductive and deductive reasoning. 70(3):1026–1039. URL: https://ieeexplore.ieee. org/abstract/document/9435092, doi:10.1109/TR.2021.3074709. [51] Ziyang Li, Saikat Dutta, and Mayur Naik. IRIS: LLM-assisted static analysis for detecting security vulnerabilities. In Y. Yue, A. Garg, N. Peng, F. Sha, and R. Yu, editors, International Conference on Learning Representations, volume 2025, pages 35735–35758. URL: https://proceedings.iclr.cc/paper_files/paper/2025/file/ 582d4e27fa24168f3af1f4582655034b-Paper-Conference.pdf. [52] Dominik Maier, Lukas Seidel, and Shinjo Park. BaseSAFE: baseband sanitized fuzzing through emulation. In Proceedings of the 13th ACM Conference on Security and Privacy in Wireless and Mobile Networks, WiSec ’20, pages 122–132. Association for Computing Machinery. URL: https://dl.acm.org/doi/10.1145/3395351. 3399360, doi:10.1145/3395351.3399360. [53] Martin Brain. CBMC: goto-cc, 2024. URL: https://diffblue.github.io/cbmc/group_ _goto-cc.html. [54] Atif Mashkoor, Michael Leuschel, and Alexander Egyed. Validation obligations: A novel approach to check compliance between requirements and their formal specification. In 2021 IEEE/ACM 43rd International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER), pages 1– 5. URL: https://ieeexplore.ieee.org/abstract/document/9402243, doi:10.1109/ ICSE-NIER52604.2021.00009. [55] Barton P. Miller, Lars Fredriksen, and Bryan So. An empirical study of the reliability of UNIX utilities. 33(12):32–44. URL: https://dl.acm.org/doi/10.1145/ 96267.96279, doi:10.1145/96267.96279. [56] MSRC Team. A proactive approach to more secure code | MSRC Blog | Microsoft Security Response Center, 2019. URL: https://msrc.microsoft.com/blog/2019/07/aproactive-approach-to-more-secure-code/. [57] Marius Muench, Jan Stijohann, Frank Kargl, Aurelien Francillon, and Davide Balzarotti. What you corrupt is not what you crash: Challenges in fuzzing embedded devices. In Network and Distributed System Security Symposium. Internet Society, 2025. URL: https://www.ndss-symposium.org/wp-content/uploads/2018/ 02/ndss2018_01A-4_Muench_paper.pdf, doi:10.14722/ndss.2018.23166. [58] Santosh Nagarakatte. Full spatial and temporal memory safety for c. 22(4):30– 39. URL: https://ieeexplore.ieee.org/abstract/document/10439147, doi:10.1109/ MSEC.2024.3363142. [59] Muhammad A. A. Pirzada, Giles Reger, Ahmed Bhayat, and Lucas C. Cordeiro. LLM-generated invariants for bounded model checking without loop unrolling. In

Amusuo et al.

Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, ASE ’24, pages 1395–1407. Association for Computing Machinery. URL: https://dl.acm.org/doi/10.1145/3691620.3695512, doi:10.1145/3691620. 3695512. [60] Mark Pitchford. The ‘shift left’ principle. New Electronics, 54(14):18–21, 2021. Publisher: Mark Allen Group. URL: https://www.magonlinelibrary.com/doi/full/ 10.12968/S0047-9624%2822%2960234-7, doi:10.12968/S0047-9624(22)602347. [61] Sai Ritvik Tanksalkar, Siddharth Muralee, Srihari Danduri, Paschal Amusuo, Antonio Bianchi, James C Davis, and Aravind Kumar Machiry. Lemix: Enabling testing of embedded applications as linux applications. In [USENIX Security’25] USENIX Security Symposium, 2025, pages arXiv–2503, 2025. [62] Brian Robinson, Michael D. Ernst, Jeff H. Perkins, Vinay Augustine, and Nuo Li. Scaling up automated test generation: Automatically generating maintainable regression unit tests for programs. In 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), pages 23–32. ISSN: 1938-4300. URL: https://ieeexplore.ieee.org/abstract/document/6100059, doi:10.1109/ASE. 2011.6100059. [63] László Szekeres, Mathias Payer, Tao Wei, and Dawn Song. SoK: Eternal war in memory. In 2013 IEEE Symposium on Security and Privacy, pages 48–62, 2025. ISSN: 1081-6011. URL: https://ieeexplore.ieee.org/abstract/document/6547101, doi:10.1109/SP.2013.13. [64] Gourav Takhar, Baldip Bijlani, Prantik Chatterjee, Akash Lal, and Subhajit Roy. Memory-safety verification of open programs with angelic assumptions. 9:312:1119–312:1147. URL: https://dl.acm.org/doi/10.1145/3763090, doi: 10.1145/3763090. [65] Norbert Tihanyi, Yiannis Charalambous, Ridhi Jain, Mohamed Amine Ferrag, and Lucas C. Cordeiro. A new era in software security: Towards self-healing software via large language models and formal verification. In 2025 IEEE/ACM International Conference on Automation of Software Test (AST), pages 136–147. IEEE Press. URL: https://dl.acm.org/doi/10.1109/AST66626.2025.00020, doi:10. 1109/AST66626.2025.00020. [66] John Toman and Dan Grossman. Taming the static analysis beast. In Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi, editors, 2nd Summit on Advances in Programming Languages (SNAPL 2017), volume 71 of Leibniz International Proceedings in Informatics (LIPIcs), pages 18:1–18:14. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/ entities/document/10.4230/LIPIcs.SNAPL.2017.18, doi:10.4230/LIPIcs.SNAPL. 2017.18. [67] Paul C. van Oorschot. Memory errors and memory safety: C as a case study. 21(2):70–76. URL: https://ieeexplore.ieee.org/abstract/document/10102611, doi: 10.1109/MSEC.2023.3236542. [68] Minghua Wang, Jingling Xue, Lin Huang, Yuan Zi, and Tao Wei. UnsafeCop: Towards memory safety for real-world unsafe rust code with practical bounded model checking. In Andre Platzer, Kristin Yvonne Rozier, Matteo Pradella, and Matteo Rossi, editors, Formal Methods, pages 307–324. Springer Nature Switzerland, 2025. doi:10.1007/978-3-031-71177-0_19. [69] Lian Kit Wee. Here comes the wave of insurance claims for the CrowdStrike outage, 2025. URL: https://www.businessinsider.com/businesses-claiming-lossescrowdstrike-outage-insurance-billions-losses-cyber-policies-2024-7. [70] Tong Wu, Shale Xiong, Edoardo Manino, Gareth Stockwell, and Lucas C. Cordeiro. Verifying components of arm(r) confidential computing architecture with ESBMC, 2024. URL: https://arxiv.org/abs/2406.04375v1. [71] Hanxiang Xu, Wei Ma, Ting Zhou, Yanjie Zhao, Kai Chen, Qiang Hu, Yang Liu, and Haoyu Wang. CKGFuzzer: LLM-based fuzz driver generation enhanced by code knowledge graph. In 2025 IEEE/ACM 47th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion), pages 243–254. URL: https://ieeexplore.ieee.org/abstract/document/11024256, doi: 10.1109/ICSE-Companion66252.2025.00079. [72] Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R. Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, and Shan Lu. AutoVerus: Automated proof generation for rust code, 2024. URL: https://arxiv.org/abs/2409.13082v1. [73] Joobeom Yun, Fayozbek Rustamov, Juhwan Kim, and Youngjoo Shin. Fuzzing of embedded systems: A survey. ACM Computing Surveys, 55(7):1–33, 2025. URL: https://dl.acm.org/doi/10.1145/3538644, doi:10.1145/3538644. [74] Cen Zhang, Yaowen Zheng, Mingqiang Bai, Yeting Li, Wei Ma, Xiaofei Xie, Yuekang Li, Limin Sun, and Yang Liu. How effective are they? exploring large language model based fuzz driver generation. In Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2024, pages 1223–1235. Association for Computing Machinery, 2024. URL: https: //dl.acm.org/doi/10.1145/3650212.3680355, doi:10.1145/3650212.3680355. [75] Chi Zhang, Yu Wang, and Linzhang Wang. Firmware fuzzing: The state of the art. In 12th Asia-Pacific Symposium on Internetware, Internetware’20, pages 110–115. Association for Computing Machinery, 2020. doi:10.1145/3457913.3457934. [76] Yaowen Zheng, Yuekang Li, Cen Zhang, Hongsong Zhu, Yang Liu, and Limin Sun. Efficient greybox fuzzing of applications in linux-based IoT devices via enhanced

AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification

user-mode emulation. In Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2022, pages 417–428. Association for Computing Machinery. URL: https://dl.acm.org/doi/10.1145/3533767.3534414, doi:10.1145/3533767.3534414.

XXX ’26, 2026, United States

XXX ’26, 2026, United States

Amusuo et al.

Outline of Appendices

methods. Our work is intended to shift their cost/benefit calculus.

The appendix contains the following material: • §A Ethics analysis • §B Open science information • §C Extended version of AutoSOUP algorithms • §D Unit Proof Case Studies • §E Instrumented memory safety properties • §F: Sample vulnerability disclosed as a result of this work. • §G: Additional experimental results.

A

Potential Harms and Mitigating Factors • Exploitation risk. AutoSOUP could be used by adversaries to more efficiently identify exploitable vulnerabilities, including zero-day vulnerabilities, before patches are developed or deployed. • False positives. When used by engineers, false positives in AutoSOUP may waste their time. Our evaluation characterized the false positives resulting from AutoSOUP to let them make an informed adoption decision. • Operational and economic impact. Findings may require costly remediation, downtime, or architectural changes for system operators and organizations. • False confidence or misuse. Over-reliance on AutoSOUP ’s outputs may lead developers to overlook other vulnerability classes or to misinterpret partial guarantees as comprehensive security. To reduce the risk of overgeneralization by engineers, our work characterizes the class of vulnerabilities exposed by AutoSOUP, and the extent of false negatives. • Risk to researchers. The research team may face legal or reputational consequences if AutoSOUP is misused, misconfigured, or perceived as facilitating harm.

Ethical Considerations

This section describes the ethical considerations of our work. AutoSOUP’s primary ethical consideration is that it can be used to identify defects in a software system, resulting in a standard “dual use” scenario posing both harms and benefits. We followed the guidance of Davis et al. in conducting our stakeholder-based ethics analysis [30].

Stakeholders Direct stakeholders: • Software maintainers and developers. Engineers who use AutoSOUP to analyze their own codebases for vulnerabilities and correctness issues. They directly interact with the tool and may act on its findings. • System operators and organizations. Teams responsible for deploying and operating software systems evaluated using AutoSOUP, including embedded, infrastructure, or safety-critical systems. • The research and development team. Authors and maintainers of AutoSOUP, who may face legal, professional, or reputational risks related to vulnerability discovery, disclosure practices, or downstream misuse. • Adversaries. Malicious actors who could use AutoSOUP, or techniques disclosed in the paper, to systematically discover vulnerabilities in target software.

Potential Benefits • Improved software security. AutoSOUP enables engineers to detect and remediate vulnerabilities earlier and more systematically, reducing the likelihood of exploitation. • Support for higher-assurance engineering. By producing structured analysis artifacts (e.g., unit-level evidence or proofs), AutoSOUP can assist organizations in meeting regulatory, safety, or compliance requirements. • Knowledge transfer and standardization. The tool and associated research disseminate best practices for systematic vulnerability analysis and verification. They may change the standard cost/benefit analysis for the use of bounded model checking. • Research advancement. AutoSOUP contributes to the scientific understanding of systematic vulnerability detection and verification, enabling further defensive research.

Indirect stakeholders: • End users of affected software. Individuals or organizations who rely on software analyzed using AutoSOUP and may be impacted by vulnerabilities or by mitigations applied as a result of AutoSOUP ’s use. • Downstream software ecosystem. Maintainers and users of libraries, dependencies, or products that incorporate code analyzed or modified using AutoSOUP. • Vulnerable populations. Groups disproportionately harmed by software exploitation, such as users of safety-critical, medical, industrial, or civic infrastructure. • Broader public. Society at large, insofar as widespread exploitation or mitigation of vulnerabilities affects trust in software systems and digital infrastructure. • Research and security community. Other researchers and practitioners who may reuse, extend, or operationalize AutoSOUP ’s techniques. • Policymakers and standards bodies. Government and industry policymakers have asked for greater use of formal

Judgment In our judgment, the potential benefit to software cybersecurity outweighs the risks posed by our work. We understood the ethical framing of our work at the outset of our study. We did not observe any new concerns during the research conduct. We therefore proceeded with submission to USENIX.

B

Open Science

An anonymized artifact for our submission is available at: https://anonymous.4open.science/r/AutoSOUP. This artifact consists of:

AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification

(1) The implementation of AutoSOUP, consisting of both the conventional software and the prompts for the LLM components. We used an agentic framework that facilitates the use of open-source LLMs rather than commercial ones. (2) The organized benchmark of real-world CVE patches in opensource embedded operating systems, derived from the work of Amusuo et al. [12]. (3) The evaluation automation that permit the replication of our results. (4) The data associated with the evaluation automation that is used to create the tables and figures in this manuscript. (5) Links to the CVEs and defect repairs resulting from this research, as they emerge. In short, we provide everything we used to create our work and collect data. We acknowledge that our use of OpenAI’s frontier models complicates the replicability of this work. We spent several thousand dollars to perform our experiments, and an independent replication would require a similar outlay of funds — and the results will change because of the evolving nature of frontier models. For more information, we refer the reviewers to the README of that artifact.

C

Detailed AutoSOUP Algorithms

Here we provide detailed versions of the core AutoSOUP algorithms.

C.1

Resource-Aware Scope Widening

Resource-aware scope widening derives the verification scope 𝑆𝑐 by incrementally adding code that may contain checkable memorysafety properties and are semantically related while keeping verification within the resource budget 𝑅. Its goal is to increase the component behavior checked against 𝑄 without making verification intractable or the resulting unit proof difficult to audit. Following prior work [64], we use source files as the unit of scope expansion. This choice reflects the convention that related functions are often colocated in the same file. File-level widening therefore preserves useful semantic context while keeping each expansion step coarse enough to manage. The technique proceeds in three steps (Algorithm 3). Step 1: Initialize the scope, bounds, and input model: We first add the file containing the component entry point 𝐶𝑒 to 𝑆𝑐 , initialize all loop bounds in the current scope to 1, and construct an input model for 𝐶𝑒 . The input model follows the entry-point type signature. Primitive arguments receive unconstrained symbolic values over their full type range, while pointer arguments are initialized to valid allocated objects containing unconstrained values. The resulting unit proof 𝑈 (𝑉 ) contains this input model and a call to 𝐶𝑒 . We use an LLM agent to synthesize this input model and recover the configurations to compile the entry point’s parent file. Although the input model follows a fixed template, compiling it with the target file requires project-specific headers, include paths, macros and mandatory program configurations. These requirements are difficult to recover reliably with fixed rules across diverse C projects [66]. Following the LLM-as-Function-Call architecture, we mechanically validate the result: the proof must compile, call 𝐶𝑒 , and introduce no preconditions beyond the intended type-based initialization.

XXX ’26, 2026, United States

Algorithm 3: Resource-aware scope widening. The algorithm incrementally expands the verification scope at the file level and returns the largest scope whose provisional verification instance remains within the resource budget. Input: Software system 𝑆, component entry point 𝐶𝑒 , maximum scope level 𝑑 max , resource budget 𝑅 Output: Verification scope 𝑆𝑐 , loop bounds 𝐵, env. model 𝐸 1 Function ResourceAwareScopeWidening(𝑆, 𝐶𝑒 , 𝑑 max , 𝑅) 2 𝑆𝑐 ← AllFunctionsIn(FileOf(𝐶𝑒 ) ) 3 𝐵 ← InitBounds(𝑆𝑐 , 1) 4 𝐸 ← InputModel(𝐶𝑒 ) ∪ ModelExternalCallees(𝑆𝑐 ) 5 if ¬WithinBudget(𝑆𝑐 , 𝐵, 𝐸, 𝑅) then 6 return ( ∅, ∅, ∅ ) 7 8 9 10 11 12 13 14

for 𝑑 ← 1 to 𝑑 max do 𝑆𝑐′ ← WidenByOneFileLevel(𝑆𝑐 ) 𝐵 ′ ← InitBounds(𝑆𝑐′ , 1) 𝐸 ′ ← InputModel(𝐶𝑒 ) ∪ ModelExternalCallees(𝑆𝑐′ ) if ¬WithinBudget(𝑆𝑐′ , 𝐵 ′ , 𝐸 ′ , 𝑅) then return (𝑆𝑐 , 𝐵, 𝐸 ) (𝑆𝑐 , 𝐵, 𝐸 ) ← (𝑆𝑐′ , 𝐵 ′ , 𝐸 ′ ) return (𝑆𝑐 , 𝐵, 𝐸 )

Function WidenByOneFileLevel(𝑆𝑐 ) 𝐹 ← FilesOf(𝑆𝑐 ) 17 𝐹 adj ← FilesContainingCalleesFrom(𝑆𝑐 ) 18 return AllFunctionsIn(𝐹 ∪ 𝐹 adj )

15

16

Step 2: Model external calls: We next identify call edges that cross the current scope boundary and replace their targets with simple type-based models. From the compiled unit, we recover the call graph and identify edges to undefined callees and their return types. We use an LLM agent to synthesize models for these undefined callees following strict guidelines, integrate them to the unit proof and ensure the resulting unit proof remains structurally valid. Primitive returns are also modeled as unconstrained symbolic values, while pointer returns are modeled as valid allocated objects containing unconstrained values. These unconstrained models preserve all possible states that may be returned by the excluded functions, including values that may violate 𝑄. Validly-allocated pointer returns avoid irrelevant invalid-pointer states that cause state-space explosion and increase verification cost. As in Step 1, an LLM agent generates and integrates the models, while deterministic checks ensure that the unit proof remains semantically valid. Step 3: Widen the scope: After constructing the provisional instance 𝑉 = (𝑆𝑐 , 𝐵, 𝐸), we check it against the configured resource budgets. If verification remains within 𝑅, we widen 𝑆𝑐 by adding all reachable functions from files that contain definitions of previously excluded and modeled callees. We use a pre-indexed database of 𝑆 to locate candidate files. When multiple files define functions with the same name and signature, we select the file closest to the in-scope caller by longest common path prefix. The LLM agent is finally used to recover the compilation configuration for newly added files. We repeat external-call modeling and scope widening until verification exceeds 𝑅 or no additional files can be added. We use

XXX ’26, 2026, United States

three budgets: verification time, memory resources, and file depth. The file depth budget bounds the number of files whose functions can be added to the verification scope so as to keep the unit proof generation cost reasonable.

C.2

Property-Guided Loop Bound and Model Refinement

A detailed description is in the main body of the manuscript. We do not expand on it here.

C.3

Context-Aware Environmental Model Refinement

Property-guided refinement in §4.3 maximizes exposure of violations of 𝑄 using unconstrained models 𝐸. However, violations found under unconstrained models may be infeasible in the broader system 𝑆. For example, the assertion on Program Line 15 in Listing 1 will be violated by an input model that provides a null pointer, even though the actual caller only provides statically-defined arrays. Context-aware environment refinement separates these infeasible property violations caused by overly permissive environment assumptions from genuine memory-safety errors. This technique operates in two steps, illustrated in Algorithm 2.

Algorithm 4: Context-aware environment model refinement. The algorithm infers underapproximate preconditions for violated memory-safety properties, validates them against calling contexts of the component entry point, and reports caller-feasible violations as memory-safety errors. Input: Software system 𝑆, component entry point 𝐶𝑒 , Environment model 𝐸, Property violations 𝑄 𝑣 Output: Refined environment model 𝐸, memory-safety error set M 1 Function ContextAwareEnvRefinement(𝑆, 𝐶𝑒 , 𝐸, 𝑄 𝑣 ) 2 M←∅ 3 W ← ParseViolationReport(𝑄 𝑣 ) // W contains tuples (𝑞, 𝑤 (𝑞) ) 4 foreach (𝑞, 𝑤 (𝑞) ) ∈ W do 5 𝜙 ← InferApproxPrecondition(𝐸, 𝑞, 𝑤 (𝑞) ) 6 (𝜙 ′ , B ) ← ValidatePrecondition(𝑆, 𝐶𝑒 , 𝑞, 𝜙 ) 7 𝐸 ← 𝐸 ∪ {𝜙 ′ } 8 M←M∪B 9

return (𝐸, M )

Function ValidatePrecondition(𝑆, 𝐶𝑒 , 𝑞, 𝜙 ) B ← ∅; 𝜙 ′ ← 𝜙 12 C ← CallsitesOf(𝐶𝑒 , 𝑆 ) 13 foreach 𝑐 ∈ C do 14 𝜓𝑐 ← PathConstraints(𝑐, 𝑆 ) 15 if 𝜓𝑐 ̸ |= 𝜙 ′ then 16 𝜙ˆ ← WeakenPrecondition(𝜙 ′ ,𝜓𝑐 ) ˆ 𝑞) then 17 if SatisfiesProperty(𝜙, 18 𝜙 ′ ← 𝜙ˆ

10

11

19 20

21

else B ← B ∪ { (𝑞,𝜓𝑐 , 𝜙 ′ ) } return (𝜙 ′ , B )

Amusuo et al.

Step 1: Infer underapproximate weakest preconditions: Following prior counter-example-guided environment refinement approaches, we infer preconditions from counterexamples that suppress violations of memory-safety properties. These preconditions need not be logically weakest, since weakest-precondition inference is often computationally expensive [23]. Instead, they must be weak enough to preserve the target property while avoiding unnecessary restrictions on safe states. For example, in Listing 1, the property on line 16 requires the loop index to remain within the size of dst. The inferred precondition 𝑟𝑒𝑡 ≤ 10 constrains the value returned by get_record_count_m2() and therefore the number of loop iterations. Further weakening this precondition by allowing larger values of 𝑟𝑒𝑡 violates the property. We first parse the verification report to extract each violated property 𝑞 ∈ 𝑄, its location loc(𝑞), and its counterexample witnesses 𝑤 (𝑞). For each tuple (𝑞, loc(𝑞), 𝑤 (𝑞)), we prompt an LLM agent to infer a precondition that, when added to 𝐸, keeps loc(𝑞) covered but suppresses the violation of 𝑞. The prompt guides the agent to identify the violated condition, propagate it backward through dataflow and path constraints, and stop at the external model or input responsible for the value. In Listing 1, the agent first identifies the violated condition 𝑖 < 𝑂𝑏 𝑗𝑒𝑐𝑡𝑆𝑖𝑧𝑒 (𝑑𝑠𝑡), which simplifies to 𝑖 < 10. It then propagates this condition through the loop condition on program line 13 to derive 𝑛 ≤ 10. Finally, it propagates the constraint to the get_record_count_m2() model and derives 𝑟𝑒𝑡 ≤ 10. The agent can inspect witnesses, navigate code, and test candidate preconditions. We accept a candidate only if it suppresses the target violation without reducing structural validity, conclusiveness, coverage, or the number of checked properties. Step 2: Validate and refine against calling contexts: The resulting precondition may overgeneralize and exclude valid caller states that would not violate 𝑞. As a result, we validate each accepted precondition against the calling contexts of 𝐶𝑒 in 𝑆. Using a pre-indexed call graph, we identify callsites of 𝐶𝑒 or the actual implementations of modeled functions. For each callsite or implementation, we use an LLM agent to identify the constraints along execution paths that reach the callsite and check whether those constraints can violate the inferred precondition. This validation produces three outcomes. If a calling path violates the precondition but still satisfies 𝑞, the agent weakens and revalidates the precondition. If a calling path violates the precondition and triggers 𝑞, we report the path as a feasible memory-safety error in 𝑆. If the precondition holds, we report the property as verified. All preconditions are added to the unit proof’s environment model 𝐸. They become explicit, auditable assumptions under which the verified component is memory safe.

D D.1

Unit Proof Case Studies Case study 1: prvCheckOptions.

prvCheckOptions processes TCP packet options using a socket pointer and a network-buffer pointer. Listing 2 shows a unit proof, comprising its input and function model, created by AutoSOUP. Scope.: At scope level 1, AutoSOUP verified the entry point and two reachable same-file callees, covering 107 lines of code. The

AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification

1 2 3 4 5 6 7 8 9

size_t uxIPHeaderSizePacket( const NetworkBufferDescriptor_t ↩→ * nbuf ) { const EthernetHeader_t * pxEth = ( const EthernetHeader_t ↩→ * ) nbuf->pucEthernetBuffer; if( pxEth->usFrameType == ( uint16_t ) ipIPv6_FRAME_TYPE ) { return ipSIZE_OF_IPv6_HEADER; } return ipSIZE_OF_IPv4_HEADER; }

10 11 12 13 14 15 16

void harness() { size_t sock_len; __CPROVER_assume(sock_len >= sizeof(FreeRTOS_Socket_t)); FreeRTOS_Socket_t *sock = malloc(sock_len); __CPROVER_assume(sock != NULL);

17

size_t nbuf_len; __CPROVER_assume(nbuf_len >= ↩→ sizeof(NetworkBufferDescriptor_t)); NetworkBufferDescriptor_t *nbuf = malloc(nbuf_len); __CPROVER_assume(nbuf != NULL);

18 19 20 21 22

size_t ethbuf_len; __CPROVER_assume(ethbuf_len >= ipSIZE_OF_ETH_HEADER); nbuf->pucEthernetBuffer = malloc(ethbuf_len); __CPROVER_assume(nbuf->pucEthernetBuffer != NULL);

23 24 25 26 27

__CPROVER_assume(nbuf->xDataLength <= ethbuf_len);

28 29

const EthernetHeader_t *eth = (const EthernetHeader_t *) nbuf->pucEthernetBuffer;

30 31

XXX ’26, 2026, United States

the callees, creating separate unit proofs to verify them. Thus, AutoSOUP maximized the number of properties verified with one unit proof, while FreeRTOS abstracted part of that behavior. Loop bounds.: prvCheckOptions contains one loop that iterates over TCP packet options. AutoSOUP kept this loop at its initial bound of 2 because all memory-safety properties were covered and no in-scope memory access depended on further unwinding. FreeRTOS used a bound of 41. It is not clear why they used such large loop bound even though the helper logic was already abstracted and no memory-safety access occur in or after that loop. This shows how property-guided refinement can avoid unnecessary unwinding. Models.: Both proofs used similar input models: valid struct pointers for input arguments (Lines 13–28) and preconditions that specify a lower bound on the size of received TCP packet (Lines 33–41). AutoSOUP also inferred the same packet-length precondition used by FreeRTOS, namely that the packet must contain the Ethernet, IP, and TCP headers. For environment modeling, both proofs modeled uxIPHeaderSizePacket by returning the IP header size implied by the packet’s IP version. The main difference is that FreeRTOS also modeled the same-file helper prvSingleStepTCPHeaderOptions, while AutoSOUP included that helper directly in scope. Overall, this case shows that AutoSOUP can replicate expert-like input and environment assumptions while checking more same-file behavior with a smaller loop bound.

32

__CPROVER_assume( ((eth->usFrameType == (uint16_t) ipIPv6_FRAME_TYPE) && (nbuf->xDataLength >= (ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + ipSIZE_OF_TCP_HEADER))) ((eth->usFrameType != (uint16_t) ipIPv6_FRAME_TYPE) && (nbuf->xDataLength >= (ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv4_HEADER + ipSIZE_OF_TCP_HEADER))));

33 34 35 36 37 38 39 40 41 42

__CPROVER_assume( ipconfigIS_VALID_PROG_ADDRESS(sock->u.xTCP.pxHandleSent) ↩→ == pdFALSE);

43 44 45

prvCheckOptions(sock, nbuf);

46 47

}

Listing 2: AutoSOUP-generated unit proof for prvCheckOptions. The harness specifies the input model. It initializes the input socket and network buffer arguments. It also identifies conditions for memory safety: the ethernet frame ethbuf_len is greater than the size of ethernet header (Line 24), the specified length value (Line 28) and the combined size of the ethernet, IP and TCP headers (Line 33 – 41). The uxIPHeaderSizePacket function model specifies the memory-safety-relevant behavior of the function: that it returns the size of IP header corresponding to the IP version in the ethernet frame. These environment models were inferred through the context-aware environment refinement technique.

FreeRTOS proof verified only the 33-line entry point and excluded

D.2

Case Study 2: vDHCPProcess

vDHCPProcess function processes received DHCP packets and manages the DHCP state machine. Scope.: AutoSOUP includes vDHCPProcess and all reachable functions in its parent file, covering 17 functions and 507 lines of code. The FreeRTOS proof includes only the 41-line entry function and excludes the reachable helper functions. This difference reflects the goal of AutoSOUP: rather than minimizing the proof to the entry point, it expands the scope to include code that may contain checkable memory-safety properties or may affect the entry point’s memory-safety behavior. Loop bounds.: AutoSOUP reaches eight loops but does not increase all bounds uniformly. It keeps six loops at the default bound of 2, bounds memcmp’s internal loop at 7 because it compares six-byte MAC addresses, and increases the bound for vProcessHandleOption.1 only after coverage feedback shows that the loop exit is needed to reach additional code. Listing 3 shows this localized refinement. In contrast, the FreeRTOS proof reaches only two loops and assigns both a uniform bound of 4. This demonstrates the property-guided approach AutoSOUP follows to derive appropriate loop bounds. Models.: AutoSOUP initializes the primitive argument as an unconstrained symbolic value and models the endpoint pointer as a valid allocated endpoint list. It also infers, from verification feedback, that the global pxNetworkEndPoints must reference the input endpoint. It also correctly infers, from a failed assertion in the program, that its xSocketValid model should return True after socket creation. The FreeRTOS proof uses a similar endpoint model by passing the initialized global endpoint object directly to vDHCPProcess, but it additionally calls prvCreateDHCPSocket and prvCloseDHCPSocket around the target call, possibly to ensure a valid socket is available.

XXX ’26, 2026, United States

1

{

2

"analysis": "The uncovered block starts at line 1095, ↩→ immediately after the `while` loop at line 1088: `while(uxTargetIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT)`.

Amusuo et al.

• pointer relation: dead object in 𝑝: ¬dead(𝑝) • pointer relation: pointer outside object bounds in 𝑝 + 𝑘: 3 offset(𝑝) + 𝑘 ≤ object_size(𝑝) 4 • pointer relation: invalid integer address in 𝑝+𝑘: object(𝑝) ≠ 5 Root cause: `ipconfigENDPOINT_DNS_ADDRESS_COUNT` is 5 in this object(NULL) ∨ 𝑝 + 𝑘 = NULL ↩→ proof configuration ↩→ (`test/unit-test/ConfigFiles/FreeRTOSIPConfig.h`), so the (4) Pointer primitives ↩→ loop may require up to 5 iterations before exit...", • pointer invalid in 𝑃 (𝑝, 𝑛): 𝑝 = NULL ∨ valid(𝑝) 6 7 "proposed_modifications": "Minimal change in Makefile only: add • deallocated dynamic object in 𝑃 (𝑝, 𝑛): 𝑝 = NULL∨¬deallocated(𝑝) ↩→ a loop-specific unwind bound for `vProcessHandleOption.1`. • dead object in 𝑃 (𝑝, 𝑛): 𝑝 = NULL ∨ ¬dead(𝑝) 8 • pointer outside object bounds in 𝑃 (𝑝, 𝑛): 𝑝 = NULL ∨ 9 Set: 10 `--unwindset vProcessHandleOption.1:6` offset(𝑝) + 𝑛 ≤ object_size(𝑝) 11 (5 needed iterations + 1 to allow falsifying the loop condition (5) Array bounds ↩→ and exiting).", • array lower bound in 𝑎[𝑖]: 𝑖 ≥ 0 12 13 "updated_harness": ... • array upper bound in 𝑎[𝑖]: 𝑖 < |𝑎| 14 } • array dynamic object upper bound in 𝑝 [𝑖]: offset(𝑝) + 𝑖 · sizeof (𝑇 ) < object_size(𝑝) Listing 3: Loop-unwinding refinement proposed for a loop • string constant lower bound in 𝑠 [𝑖]: 𝑖 ≥ 0 in vProcessHandleOption, reachable from vDHCPProcess, by • string constant upper bound in 𝑠 [𝑖]: 𝑖 < |𝑠 | the property-guided loop bound refinement technique. The (6) Overflow technique identified a block of code which was not being • arithmetic overflow on signed + in 𝑥 + 𝑦: MIN ≤ 𝑥 + 𝑦 ≤ verified, determined it resulted from insuffient loop bounds, MAX and derived the minimal loop bound required for the loop • arithmetic overflow on signed − in 𝑥 − 𝑦: MIN ≤ 𝑥 − 𝑦 ≤ exit condition to hold and the block of code to be verified. MAX • arithmetic overflow on signed ∗ in 𝑥 ·𝑦: MIN ≤ 𝑥 ·𝑦 ≤ MAX • arithmetic overflow on signed shl in 𝑥 ≪ 𝑘: MIN ≤ 𝑥 ·2𝑘 ≤ These differences identify the distinguishing feature of fidelityMAX oriented and safety-oriented unit proofs: fidelity-oriented proofs • arithmetic overflow on signed unary minus in −𝑥: 𝑥 ≠ may use functions within the project to proactively set up valid MIN calling context, while safety-oriented proofs recover these semantic • arithmetic overflow on signed division in 𝑥/𝑦: ¬(𝑥 = knowledge as necessary and encode them as explicit assumptions MIN ∧ 𝑦 = −1) in the unit proof. • result of signed mod is not representable in 𝑥 mod 𝑦: ¬(𝑥 = MIN ∧ 𝑦 = −1) E Instrumented Memory Safety Properties (7) Undefined-shift This appendix summarizes the memory-safety properties verified in • shift distance is negative in 𝑥 ≪ 𝑘: 𝑘 ≥ 0 this work as part of the experimental evaluation. These properties • shift distance too large in 𝑥 ≪ 𝑘: 𝑘 < 𝑤 are instrumented by CBMC and genuine violations can represent • shift operand is negative in 𝑥 ≪ 𝑘: 𝑥 ≥ 0 high-impact security vulnerabilities. (8) Division-by-zero (1) Assertion • division by zero in 𝑥/𝑦 or 𝑥 mod 𝑦: 𝑦 ≠ 0 • max allocation size exceeded: malloc_size ≤ MAX_SIZE (9) Pointer • max allocation may fail: ¬should_malloc_fail • same object violation in pointer comparison: object(𝑝) = (2) Pointer dereference object(𝑞) • dereference failure: pointer NULL in 𝑝: 𝑝 ≠ NULL (10) Precondition instance • dereference failure: pointer invalid in 𝑝: valid(𝑝) • memcpy src/dst overlap: object(𝑠𝑟𝑐) ≠ object(𝑑𝑠𝑡) ∨ 𝑠𝑟𝑐 + • dereference failure: deallocated dynamic object in 𝑝: ¬deallocated(𝑝) 𝑛 ≤ 𝑑𝑠𝑡 ∨ 𝑑𝑠𝑡 + 𝑛 ≤ 𝑠𝑟𝑐 • dereference failure: dead object in 𝑝: ¬dead(𝑝) • memcpy source region readable: R_OK(𝑠𝑟𝑐, 𝑛) • dereference failure: pointer outside object bounds in 𝑝: • memcpy destination region writeable: W_OK(𝑑𝑠𝑡, 𝑛) offset(𝑝) + sizeof (∗𝑝) ≤ object_size(𝑝) • memset destination region writeable: W_OK(𝑑𝑠𝑡, 𝑛) • dereference failure: invalid integer address in 𝑝: object(𝑝) ≠ • memmove source region readable: R_OK(𝑠𝑟𝑐, 𝑛) object(NULL) ∨ 𝑝 = NULL • memmove destination region writeable: W_OK(𝑑𝑠𝑡, 𝑛) • no candidates for dereferenced function pointer: false • strcpy/strncpy src/dst overlap: object(𝑠𝑟𝑐) ≠ object(𝑑𝑠𝑡)∨ • dereferenced function pointer must be 𝑓 : fp = 𝑓 𝑠𝑟𝑐 + 𝑛 ≤ 𝑑𝑠𝑡 ∨ 𝑑𝑠𝑡 + 𝑛 ≤ 𝑠𝑟𝑐 • dereferenced function pointer must be one of {𝑓1, . . . , 𝑓𝑛 }: • free argument must be NULL or valid pointer: 𝑝 = NULL∨ fp ∈ {𝑓1, . . . , 𝑓𝑛 } R_OK(𝑝, 0) (3) Pointer arithmetic • free argument must be dynamic object: 𝑝 = NULL ∨ • pointer relation: pointer NULL in 𝑝: 𝑝 ≠ NULL dynamic(𝑝) • pointer relation: pointer invalid in 𝑝: valid(𝑝) • free argument has offset zero: 𝑝 = NULL ∨ offset(𝑝) = 0 • pointer relation: deallocated dynamic object in 𝑝: ¬deallocated(𝑝)

AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification

1 2 3

// Public API. path is user-controlled. ssize_t nanocoap_sock_post(nanocoap_sock_t *sock, const char ↩→ *path, ...) { return _sock_put_post(sock, path, ...);}

4 5

8 9

GLM-5

MiniMax M2.5

37.0

37.0

size_t coap_opt_put_uri_pathquery(uint8_t *buf, uint16_t ↩→ *lastonum, const char *uri) { coap_opt_put_string_with_len(buf, ..., string, ...); }

Compiles (%) Structural validity (%) Verification completes (%) Generation succeeds (%)

97.3% 81.1% 86.5% 78.4%

75.7% 62.2% 73.0% 48.6%

// buf is a fixed size buffer from sock->hdr_buf // const char *string contains user-provided string size_t coap_opt_put_string_with_len(uint8_t *buf, ..., const char *string, ...) { uint8_t *bufpos = buf; char *uripos = (char *)string;

Verification time (s) Avg component size (loc) Avg covered size (loc) Avg coverage (%)

98.6 99.9 90.9 96.1

56.9 54.6 42.7 81.5

Avg num. properties (#) Avg num. verified properties (#) Avg num. vulnerabilities (#)

262.1 253.0 2.1

174.6 170.3 1.2

Avg generation time (min) Avg API cost ($)

739.4 4.9

83.4 0.7

Avg proof size (loc)

48.4

29.6

10 11 12 13 14 15 16 17 18

while (len) { uint8_t *part_start = (uint8_t *)uripos; bufpos += coap_put_option(bufpos, ..., part_start, ...); }

19 20 21 22 23

}

24 25 26 27 28

Table 6: Comparison AutoSOUP’s performance when using open-source models

Num Targets

// nanocoap_sock_post -> _sock_put_post -> ↩→ coap_opt_put_uri_pathquery -> coap_opt_put_string_with_len -> ↩→ coap_put_option

6 7

// odata is user-provided string. olen is its length. size_t coap_put_option(uint8_t *buf, ..., const void *odata, ↩→ size_t olen) { assert(lastonum <= onum);

Metric

Table 7: Summary statistics for the evaluation subjects.

29

n = _put_delta_optlen(buf, n, 0, olen); if (olen) { // Copy of olen bytes into fixed length buffer without ↩→ validation. memcpy(buf + n, odata, olen); n += olen; } return (size_t)n;

30 31 32 33 34 35 36 37

}

Listing 4: Sample of out-of-bound write vulnerability on line 33 discovered by AutoSOUP in RIOT-OS.

Details of Reported Vulnerabilities

Listing 4 illustrates a vulnerability in RIOT-OS (nanocoap.c) discovered by AutoSOUP. The bug is reached along the following execution flow. • Initial harness. AutoSOUP first generates a harness for coap_opt_put_uri_pathquery, a root function in nanocoap.c. The harness initializes the buf and string arguments as nondeterministic buffers with unconstrained sizes. • Coverage refinement and bug exposure. Stage 2 then resolves coverage gaps until all edges along the call path

Software

Size

Stars

Parent modules

Zephyr-RTOS RIOT-OS Contiki-NG FreeRTOS

2253971 417135 186095 836205

15115 5718 1486 7280

BT, FS, USB, Shell, 6LoWPAN BT, FS, USB, Shell, 6LoWPAN BT, FS, USB, Shell, 6LoWPAN Shell, FS, OTA, MQTT, JSON

in line 5 of Listing 4 are covered. At this point, verification exposes an out-of-bounds write at line 33. Although the code contains a loop at line 19, the bug manifests without increasing its unwinding limit. • Precondition generation. In Stage 3, AutoSOUP analyzes the counterexample trace and infers a precondition that constrains the input (buffer) length to eliminate the reported error. • Precondition validation. The validator performs backward dataflow analysis to trace the constrained argument to its source. It determines that the relevant string originates from a parameter of the public API nanocoap_sock_post. Along this path, it finds no explicit constraint on the string length. It therefore flags the inferred precondition as violable in the real environment and reports the corresponding memcpy out-of-bounds write as a true vulnerability.

• double free: 𝑝 = NULL ∨ ¬deallocated(𝑝) • free called for new[] object: 𝑝 = NULL ∨ ¬new_array(𝑝) • free called for stack-allocated object: 𝑝 = NULL∨¬stack(𝑝) (11) Precondition • memcmp region readable: R_OK(𝑠, 𝑛) • memcpy region readable: R_OK(𝑠, 𝑛) • buffer nonnull: 𝑏𝑢 𝑓 ≠ NULL • size greater than zero: 𝑠𝑖𝑧𝑒 > 0 • buffer writable: W_OK(𝑏𝑢 𝑓 , 𝑠𝑖𝑧𝑒) • object overlap: object(𝑝) ≠ object(𝑞)

F

XXX ’26, 2026, United States

We reported this issue to the RIOT-OS maintainers, who acknowledged receipt and began an internal investigation.

G

Additional Evaluation Data and Results

Table 7 summarizes the evaluation subjects. These are embedded operating systems developed and maintained by Google (ZephyrRTOS), Amazon Web Services (FreeRTOS), and the international engineering community (RIOT-OS, Contiki-NG).

XXX ’26, 2026, United States

Table 6 compares AutoSOUP’s performance when using two open-source models, GLM-5 and MiniMax M2.5, across 37 targets. Received 20 February 2007; revised 12 March 2009; accepted 5 June 2009

Amusuo et al.