VeraRAN: Pre-Actuation Certification and Event-Causal Synchronization Repair for Asynchronous Multi-Interface RAN Plans

VeraRAN: Pre-Actuation Certification and Event-Causal Synchronization Repair for Asynchronous Multi-Interface RAN Plans Yinghan Hou and Zongyou Yang

arXiv:2608.01047v1 [cs.NI] 2 Aug 2026

Imperial College London, United Kingdom {y.h24, zy2926}@ic.ac.uk Abstract—Agentic RAN controllers combine mobility, energy, and resource actions across independently implemented interfaces. Even when each command is valid and the target state is safe, asynchronous actuation can drive the network through unsafe intermediate states. In a frozen study of a 35B planner, 28.8% of locally valid plans remained asynchronously unsafe. We introduce VeraRAN, which checks plans before actuation by modeling request, delivery, acceptance, application, completion, and observation for each action while exploring plausible delays and event orders. When VeraRAN finds a counterexample, VeraSync inserts versioned event barriers and rechecks the repaired plan for safety and completion. MI-POR prunes independent interleavings using RAN lifecycle and resource footprints. In a post-freeze stratified confirmation within the declared repair domain, VeraSync re-certified every confirmation plan while leaving 87% of action pairs unordered. MI-POR matched exact search in a property-stratified audit and reduced explored states by 94.6–95.0% on 20–40-action plans. Native ns-O-RAN replay and an independent live E2 audit showed why distinguishing these events matters: acceptance may precede the authoritative state transition, so dependent actions must wait for direct APPLY evidence or a contract-backed completion event causally downstream of APPLY. Index Terms—O-RAN, agentic networking, model checking, partial-order reduction, runtime synchronization, RAN control.

I. I NTRODUCTION A RAN plan may combine mobility, energy, scheduling, load, and policy controls [1]–[3]. O-RAN exposes them through separately operated control and management paths [4]–[9]. Emerging intent-driven and agentic controllers motivate coordinated control across RAN functions and timescales [10], [11]. Yet local validity does not constrain the order in which such controls take effect. A source cell may sleep before the serving-cell transition applies; a donor quota may fall before its replacement becomes active, even though every command and the final state are valid. We model E2 control, A1 policy application, and O1 management as independently contracted actions whose delivery envelopes and authoritative events may differ. Local gates validate one command, fixed waits approximate actuation with elapsed time, and global serialization orders related and unrelated actions alike. These safeguards do not identify the authoritative event that discharges a cross-path dependency. VeraRAN supplies a pre-actuation certification pipeline (Fig. 1). A per-action event contract relates request, delivery,

acceptance, authoritative application, completion, and observation. The verifier explores admissible endpoints, delays, orders, versions, and evidence scopes. Counterexamples drive VeraSync to add event dependencies, after which the entire revised plan undergoes the same safety-and-completion check. A fail-closed executor releases each gated REQUEST, or opens a registered application hook, only when authoritative evidence matches the required action, scope, version, and epoch. Across a balanced six-stratum study, 51 of 177 locally valid 35B plans admitted an unsafe asynchronous execution. In an independent 144-plan confirmation within the declared repair domain, VeraSync re-certified every plan. Initial portable REQUEST-gate synthesis left 86.98% of action pairs unordered; registered application hooks enabled verified pruning to 89.33%. Live E2 measurements grounded the release events, while the multi-interface partial-order reduction (MI-POR) reduced explored states by 94.6–95.0% on decomposable 20– 40-action plans. The central contribution is an end-to-end refinement from a symbolic cross-path dependency to the runtime evidence allowed to discharge it. VeraSync instantiates registered failclosed gates and rechecks the full plan; MI-POR removes redundant interleavings through lifecycle, evidence, resource, repair, and necessary-enabling footprints without changing declared outcomes. II. U NSAFE P LAN T RAJECTORIES AND R ELEASE AUTHORITY A. Safe commands can form an unsafe trajectory For handover followed by source-cell sleep, the UE must move before its source cell turns off. The required dependency is APPLY(ServingCell(u) = ct , vh ) ≺ APPLY(CellSleep(cs ), vs ).

(1)

A quota migration transfers ∆ from donor slice d to recipient r. The decrease can be issued only after the increase applies: APPLY(qr ← qr + ∆, vq ) ≺ REQ(qd ← qd − ∆, vq ). The stronger APPLY-to-REQUEST form prevents an executor from delivering the decrease early to an endpoint that could apply it immediately.

VeraRAN pre-actuation certification typed plan · envelopes · properties

Locally valid plan Planner / controller

1 handover (UE,target)

Independent endpoints

Per-action event contract REQUEST

DELIVERY

2 sleep(source)

E2 mobility /

load

APPLY authoritative safe+

YES

complete?

ACCEPT: not authoritative no fixed APPLY precedence

unsafe order: APPLY(sleep) → APPLY(handover) SAFE source active

UNSAFE

SAFE

UE at source

UE at target

source asleep

Certified plan + event gates versioned certificate

COMPLETE / OBSERVE contract-backed

Versioned fail-closed executor

NO

released action

A1 policy O1

energy / config.

authoritative evidence match action · scope · version

Bounded trajectory verifier safety + bounded completion

required: APPLY(handover) ≺ APPLY(sleep)

MI-POR

Counterexample event core

VeraSync repair versioned event gates

repaired plan → full re-certification

Fig. 1. VeraRAN architecture and event-causal execution. The verifier certifies a candidate plan or sends its counterexample to VeraSync for repair with registered templates and full re-certification. The executor releases a gated REQUEST or opens a registered application hook only on authoritative evidence matching the certified action, scope, version, and epoch.

B. Release authority Only APPLY changes authoritative state. ACCEPT cannot release a dependency by label alone; COMPLETE or OBSERVE may release it only when the registered event contract places that event downstream of the matching APPLY transition. Accordingly, VeraRAN represents each dependency as a typed relation from an authoritative predecessor event to the successor’s REQUEST or APPLY gate. III. P LAN C ERTIFICATION WITH E VENT C ONTRACTS A. Typed plan A compiled plan is P = (A, ≺0 , Γ, D, Φ, H). A contains typed actions and ≺0 their declared order. Γ contains the event contracts and intrinsic lifecycle delays; D contains endpoint choices and root REQUEST-ready bounds. Φ = ΦS ∧ ΦL gives the safety and completion properties, and H is the horizon. Runtime evidence and versions belong to the verifier state, not to P. Let Vaall = {Ra , Da , Aa , Pa , Ca , Oa }, denote the universe of possible lifecycle events for action a, and let Va ⊆ Vaall be the subset present in its registered contract. The six symbols denote REQUEST, DELIVERY, ACCEPT, authoritative APPLY, mechanism COMPLETE, and independent OBSERVE. The per-action event contract is

can terminate at Pa or Oa . The compiler requires Ra ≺∗Γa z for every z ∈ Va \ {Ra }, and rejects an unreachable event or terminal. Only Ra ≺Γa Da ≺Γa Pa is mandatory. No order involving Aa , Ca , Oa is assumed without a declared edge. Define Auth(Γa ) = {Pa } ∪ {z ∈ Va ∩ {Ca , Oa } : Pa ⪯∗Γa z ∧ κa (z) ≡ κa (Pa )}. Here ≡ permits a different wire type but requires the same action, target scope, version, and epoch. ACCEPT is not authoritative by label; a direct-callback contract may omit Aa , Ca . The audited OCUDU contract is Ra ≺Γa Da ≺Γa Aa ≺Γa Pa ≺Γa Ca ,

Pa ≺Γa Oa ,

sets Ta = Ca , and assumes no unmeasured Ca /Oa order. Distinct events remain strictly ordered in the DAG even when their logical timestamps agree; for example, θa (Aa ) ≤ θa (Pa ) permits a legal equal-time Aa -then-Pa order.

B. State and transition relation The verifier state is s = (x, q, ℓ, θ, σ, e, ν, τ ),

Γa = (Va , Fa , δa , κa , Ta ), where Fa is a causal DAG, δa bounds edge delays, κa assigns evidence signatures, and Ta = Term(a) ∈ Va is the declared terminal event. Va includes Ra , Da , Pa ; a contract without Ca

where x, q are authoritative radio/resource state; ℓa (z) ∈ {pending, fired} and θa (z) record lifecycle status and firing time; σa (z) ∈ N0 ∪{⊥} is the scheduled firing time; e, ν store

runtime evidence and versions; and τ ∈ N0 is logical time. Let Preda (z) = {u : (u, z) ∈ Fa }. Readys (z) ⇐⇒ Preda (z) ⊆ Fired(s) ∧ Gplan ∧ Gid ∧ Grepair , Ls (z) = Us (z) =

max u∈Preda (z)

min u∈Preda (z)

C. Properties and event dependencies The two-action dependency in (1) generalizes to a handover group G: every declared member needs a matching target-cell APPLY before source sleep. ∀u ∈ G :

{θa (u) + d− uz },

APPLY(ServingCell(u) = ct , vh ) ≺ APPLY(CellSleep(cs ), vs ).

{θa (u) + d+ uz },

(4)

The service-floor property is X ϕfloor (s) ≡ qk (s) ≥ Qmin .

Enableds (z) ⇐⇒ ℓa (z) = pending ∧ Readys (z) ∧ σa (z) ̸= ⊥ ∧ σa (z) ≤ τ.

k∈S

Gplan enforces plan order and endpoint eligibility, Gid matches action, scope, version, epoch, and freshness, and Grepair enforces instantiated barriers. Initially σa (z) = ⊥ for non-root events. At initialization, the verifier nondeterministically assigns each root REQUEST an immutable scheduled time from its interval in D. When a transition first makes any other z ready by firing its last causal predecessor or discharging a guard, it assigns σa (z) ∈ [max{τ, Ls (z)}, Us (z)]; an empty interval makes z unrealizable. Firing z sets ℓa (z) = fired and θa (z) = τ , applies its registered update, and schedules newly ready successors. Let

The exact compiler instantiates this property for a bounded two-action quota migration.

Eτ (s) = {z : Enableds (z)}, Tick(s) ⇐⇒ τ < H ∧ ¬ΦL (s) ∧ Eτ (s) = ∅.

Proof. The sum is unchanged initially, rises by ∆ after the recipient APPLY, and returns to its initial value after the donor APPLY; identity matching prevents another migration from releasing the decrease. Lemma 1 covers only the declared two-action aggregate floor. Per-slice bounds, nonnegativity, total capacity, and all other obligations remain in ΦS and are checked by the whole-plan verifier.

A tick transition changes only logical time, setting τ ← τ + 1. Thus a due event cannot be postponed by TICK. The implementation coalesces consecutive ticks by jumping to the next scheduled time. At a nonempty Eτ (s), the verifier branches over every event and legal equal-time order; an unrealizable event or an empty transition set before completion is a completion failure. REQUEST/DELIVERY carry an endpoint. ACCEPT, COMPLETE, and OBSERVE record typed evidence and time, whereas APPLY alone changes authoritative state and version. Later evidence cannot rewrite its APPLY time. a) Exact six-event semantics: The reference retains every event read by a property, terminal predicate, timing rule, or gate, and enumerates the DAG, integer delays, and legal equaltime orders. Release requires matching kind, identity, scope, version, epoch, and freshness; deadlock cannot pass on safety alone. Exec(P) contains the maximal executions through H: a trace stops at completion, deadlock, or after exhausting event transitionsVat τ = H. Its monotone completion predicate is ΦL (s) ≡ a∈A [ℓa (Ta ) = fired]; a completed trace has time Tcomp (ρ) = maxa∈A θa (Ta ). A plan is certified iff ∀ρ ∈ Exec(P), ∀s ∈ ρ : ΦS (s),

(2)

∀ρ ∈ Exec(P), ∃s ∈ ρ : ΦL (s).

(3)

A reject-only deadlock may satisfy (2) but violates (3), so it is not a valid certificate.

Lemma 1 (Two-action service-floor barrier). Assume an initial P allocation with k qk ≥ Qmin , one recipient increase +∆, one donor decrease −∆, no other mutation of these quotas during the migration, and reliable execution of issued actions within the declared horizon. The barrier APPLY(qr ← qr + ∆, v) ≺ REQ(qd ← qd − ∆, v), preserves ϕfloor for every admitted delivery and application delay.

IV. V ERA S YNC : F ROM C OUNTEREXAMPLE TO E XECUTABLE C ERTIFICATE A. Counterexample core From an unsafe trace, VeraSync extracts the violated property, authoritative APPLY transitions, missing evidence, versions, and radio/resource footprints. VeraSync repairs over the original actions and endpoints by adding authoritative-event precedence relations. When no declared template expresses the required relation, the executor withholds the plan and reports UNSUPPORTED. Define B(b, a; z, G) to open gate G ∈ {REQ, APPLY} of action a only after z ∈ Auth(Γb ) fires with matching type, scope, and version. BT (P) denotes the finite set of barriers that the registered template library T can instantiate over the actions in P. Writing APPLY or OBS as the release event abbreviates z = Pb or z = Ob . The verifier reasons about that event, not the label of a transport ACK. We call B the symbolic barrier and its executor check the runtime gate. B. Template-guided repair Algorithm 1 preserves actions, endpoints, and plannerspecified request-ready times; barriers may delay issuance. Each iteration compiles one property-relevant core and

Algorithm 1 VeraSync template-guided certification Require: P = (A, ≺0 , Γ, D, Φ, H), s0 , T , Kmax Ensure: certified (P ⊕ B, χ), UNSUPPORTED, or ITERATION LIMIT 1: B ← ∅ 2: for k = 0, . . . , Kmax do 3: r ← Verify(P ⊕ B, s0 ) 4: if r = SAFE - AND - COMPLETE(χ) return (P ⊕ B, χ)

if r = INCOMPLETE(ρ) return UNSUPPORTED(r) if k = Kmax return ITERATION - LIMIT(r) η ← ExtractCore(r.counterexample) F ← Compile(η, P, s0 , T ) \ B if F = ∅ return UNSUPPORTED(η) B ←B∪F 11: end for 5: 6: 7: 8: 9: 10:

rechecks the full plan. Here P ⊕ B installs B in P and Kmax = 4. The verifier returns Verify(·) ∈ {UNSAFE(ρ, ϕ), INCOMPLETE(ρ), SAFE - AND - COMPLETE(χ)}. Here χ is a registry-bound execution manifest, χ = (vs , kr , vr , ϵ, ti , td , Ψ, h), Ψ = (s0 , P ⊕B, M ), Here vs is the schema version; (kr , vr ) is the registry key and revision; ϵ is the endpoint epoch; [ti , td ] is the validity interval; and M is the registry-supplied access map. h contains canonical component digests, including the initial-state projection. A validator checks them against an independently pinned registry before execution. Thus χ is a bound execution manifest, not a proof trace; the verifier remains responsible for the trajectory proof. The loop instantiates a registered template for each supported safety counterexample and rechecks the composition. It returns an INCOMPLETE result as UNSUPPORTED: the current templates add precedence gates but do not add actions, relax request-ready times, or claim a liveness repair. Because B grows within finite BT (P), an uncapped loop terminates within |BT (P)| iterations or returns UNSUPPORTED; soundness follows from the final whole-plan check. Of 728 confirmation components, 712 certify after one repair iteration and 16 after two; none consumes the additional guard depth Kmax = 4. The declared template library implements the sourceevacuation dependency in (4) and analogous scoped or versioned APPLY dependencies for capacity transfer and PRB/slice reprofiling. For the redundancy audit, B is 1-minimal iff it certifies and B \ {b} does not for every b ∈ B. Re-certified singleedge deletion reaches this fixed point; the component oracle evaluates a stronger lexicographic objective. For a plan P and barriers B, we report U (P, B) = 1 −

| TC(≺0 ∪ ≺B )| ,
|A| 2

where TC is the strict transitive closure over distinct action pairs. Thus U is the fraction left unordered. Summary values are macro-averages over plans, so every plan has equal weight. For the confirmation population, every pruned applicationhook repair lies in the direct APPLY-to-APPLY sublanguage. On access-map components of at most five actions, the oracle enumerates every acyclic subset of that sublanguage and minimizes direct barriers, ordered pairs, then worstcase completion time under the original requests. MI-POR screens candidates; exact search rechecks each winner and the composition. The oracle comparison is therefore stated for the confirmation’s application-gate language; Lemma 1 separately establishes the APPLY-to-REQUEST service-floor repair. C. Versioned execution and event-causal concretization Each verified dependency is released by an authoritative event and may guard the dependent action’s REQUEST or APPLY. Definition 1 (Admissible runtime concretization). For evidence record e, let βb : {Pb } → Auth(Γb ), Freshχ (e, s) ⇐⇒ ti ≤ t(e) ≤ tnow (s) ≤ td ∧ tnow (s) − t(e) ≤ TTL(type(e)) ∧ epoch(e) = ϵ, Matchχ (e, z, s) ⇐⇒ sig(e) = κb (z) ∧ Freshχ (e, s), Admχ (βb , e, s) ⇐⇒ βb (Pb ) = z ∈ Auth(Γb ) ∧ Matchχ (e, z, s) ∧ ℓb (z) = fired. A gate Ga for B(b, a; Pb , Ga ) opens only under Admχ (βb , e, s). The binding κb (z) ≡ κb (Pb ) fixes action, target scope, version, and epoch while allowing the wire type of z to differ from APPLY. The validator accepts only a Γb -conformant runtime trace. Theorem 1 (Contract-relative release-order refinement). Under Definition 1, every runtime release of Ga satisfies Pb ⪯ρ z ≺ρ Ga

and

t(Pb ) ≤ t(z) ≤ t(Ga ).

Hence the concrete gate trace refines the verified releaseorder dependency Pb ≺ Ga . Missing, stale, wrong-scope, wrong-version, or ACCEPT-only evidence cannot release Ga . Concretization may delay or block the plan, so bounded completion remains an independent verification obligation. Proof. Opening Ga identifies a fired z = βb (Pb ). Contract conformance gives Pb ⪯ρ z, and the gate gives z ≺ρ Ga ; failed validation and ACCEPT-only evidence remain closed. The executor binds each barrier to a versioned APPLY callback or authorized downstream evidence. Timeouts never count as APPLY; requests and evidence are idempotent, restarts advance the certificate epoch, and all lifecycle timestamps declared in Γa remain reconstructible. An APPLY gate also requires a registered application hook that can hold the successor before state mutation. Otherwise

the compiler lowers the dependency and verifies the stronger executable order: ( Pb ≺ Pa , AppGate(a), Pb ≺ Pa 7→ Pb ≺ Ra , otherwise. The lowered plan receives a new manifest only after full safety-and-completion verification; the executor never treats request release as an APPLY gate. V. S CALABLE C ERTIFICATION WITH MI-POR A. Exact reference and transparent projection The backend projects ACCEPT/COMPLETE only on a single-predecessor, single-successor chain with independent finite delays and no branch, mutation, semantic read, or gate; incident intervals combine by Minkowski sum. All other cases use the six-event reference. Lemma 2 (Transparent lifecycle projection). Contracting only transparent Aa , Ca nodes preserves bounded safety labels and the minimum and maximum occurrence time of every retained terminal event. Proof sketch. Trace contraction sums the two realized delays; every composed delay decomposes into an admitted pair. The chain and no-read premises preserve enabledness, labels, mutations, and terminal times both ways. B. RAN lifecycle and property footprints After Lemma 2, _event_access maps retained R, D, P, O events to conservative semantic read/write tokens; nontransparent Aa or Ca selects exact verification. The tokens cover lifecycle status and predecessors; endpoint options; radio, load, PRB, and slice state; evidence identity and freshness; terminal time, TTL, and horizon; rollback snapshots; and repair-order closure. Conflicts include read–write/write–write intersections, causality, barriers and their closure, same-action events, and global rollback APPLY. A concurrent APPLY also conflicts when a later rollback may read its pre-mutation snapshot. MI-POR runs in two stages. For Ω = (Φ, B, Γ, D, H), let Rloc (Ω) contain every safety property, repair gate, identity/freshness read, request-ready time, and per-action terminal read. For action components K, Supp(r) ⊆ A contains the actions read by obligation r. Define LocalityOK(K; Ω) ⇐⇒ ∀r ∈ Rloc (Ω), ∃Ki ∈ K : Supp(r) ⊆ Ki . The all-actions completion predicate and horizon are composed after component exploration. Let ki ∈ {U, I, S} be the verdict for ri ; when all are S, set Tmin = maxi Ti,min and Tmax = maxi Ti,max . Then  U, ∃i : ki = U,    I, ∃i : ki = I, C⊕ (r1:m ) =  I, (∀i : ki = S) ∧ Tmax > H,    S(Tmin , Tmax ), otherwise.

Stage 1 requires LocalityOK; a cross-component read disables it. Stage 2 selects the lexicographically rooted persistent component at each logical time. At state s, let τ = τ (s) and use the exact-semantics due set Eτ (s) = {e : Enableds (e)}. Zs,τ adds zero-delay lifecycle successors, while Ns,τ adds events made ready by a plan or repair guard before time advances. Both are conservative over endpoint and delay choices. Define the future closure and lifted conflict together:
Fs,τ (e) = µX. {e} ∪ Zs,τ (X) ∪ Ns,τ (X) , e ∼+ M,s v ⇐⇒ ∃u ∈ Fs,τ (e), w ∈ Fs,τ (v) : u ∼M w. Let e ⇝s,τ w mean that firing e can make pending event w ready before time advances. The registry admits Stage 2 only when EnableSound(P, B, M ) ⇐⇒ ∀s ∈ Reach≤H (P ⊕ B), ∀e ∈ Eτ (s) (s), ∀w : e ⇝∗s,τ (s) w ⇒ w ∈ Fs,τ (s) (e). This is a semantic proof obligation; the implementation checks a finite, conservative registry condition sufficient for it. Let Q0Γ = {(u, v) ∈ Fa : d− uv = 0}, Q0G = {(u, v) : u ⇒0G v}, where u ⇒0G v denotes discharge of a same-tick plan or repair guard, as derived from the registered DAGs, request-ready b Z and Q b N be the corresponding bounds, ≺0 , and B. Let Q edges enumerated by Z and N . Define bZ EnableCover(P, B, M ) ⇐⇒ Q0Γ ⊆ Q 0 bN . ∧ QG ⊆ Q

(5)

The compiler also requires every rule that can change readiness without advancing time to appear in Q0Γ ∪ Q0G . These rules comprise zero-delay DAG edges, plan and repair guards, and root request-ready equalities. Write StaticEnableOK(P, B, M ) for this registry check conjoined with Eq. (5). Lemma 3 (Syntactic enablement age). If StaticEnableOK(P, B, M ) holds, EnableSound(P, B, M ) holds.

coverthen

Proof sketch. The registry premise makes Q0Γ ∪ Q0G exhaustive. Equation (5) places each immediate successor in Z or N ; induction places every e ⇝∗s,τ w in Fs,τ (e). Failed projection or registry coverage selects exact verification. Options(s, e, τ (s)) enumerates endpoint and equal-time variants of firing e, together with schedule choices for successors that e newly makes ready. Events outside C ⋆ stay due and commute past the selected closure. The Stage 1 ablation branches over all enabled events with the same state, options, and checks. Plans of at most eight actions use exact search; larger plans use MI-POR only after the declared checks pass. Definition 2 (Access-map soundness). For transition t, let RWsem (t) = (Rsem (t), Wsem (t)) and RWM (t) =

Algorithm 2 Two-stage MI-POR verification Require: P = (A, ≺0 , Γ, D, Φ, H), s0 , B, M Ensure: k ∈ {U, I, S}; extrema if k = S 1: Ω ← (Φ, B, Γ, D, H) 2: Gconf ← static action-conflict graph from M, Γ, B, Φ 3: if not StaticEnableOK(P, B, M ) then 4: return Explore(P, s0 , B, N EXTexact ) 5: end if 6: K ← Components(Gconf ) 7: if |K| > 1 and LocalityOK(K; Ω) then 8: ri ← Explore(P[Ki ], s0 , B[Ki ], N EXTMI ) for each Ki ∈ K 9: return Compose(r1 , . . . , r|K| ) ▷ Stage 1 10: end if 11: return Explore(P, s0 , B, N EXT MI ) 12: function N EXTMI (s, Eτ ) 13: if Eτ = ∅ then 14: return {Tick} if Tick(s), else ∅ 15: end if 16: Fs,τ (e) ← SameTickClosure(s, e) for each e ∈ Eτ 17: Build G+ = (Eτ , ∼+ τ M ), including barriers and rollback-visible snapshots 18: a⋆ ← min{action(e) : e ∈ Eτ } ⋆ 19: C ⋆ ← component of G+ τ containing a ⋆ 20: return {(e, o) : e ∈ C , o ∈ Options(s, e, τ (s))} ▷ Stage 2 21: end function (RM (t), WM (t)), with componentwise containment; γ concretizes declared tokens. Then AccessSound(M ) ⇐⇒ ∀t : RWsem (t) ⊆ γ(RWM (t)). RWsem includes enabledness, property, evidence/freshness, state-key, and terminal-time accesses. An unassigned access disables decomposition. The typed plan supplies lifecycle, gate, identity, freshness, and timing tokens; a pinned registry supplies mechanismspecific resource accesses. Missing token classes are rejected and unmapped accesses select exact search. The theorem is registry-relative, and Section VII exercises that premise by access mutation and exact differential tests. Definition 3 (Implementation independence). For due transitions u, v, let Conf s collect causal, same-action, barrier, access-map, and rollback-snapshot conflicts. Write u(s) for the successor. The canonical key Ξ(s) contains logical time; lifecycle status, timestamps, and schedules; every radio/resource field read by a remaining transition or property; evidence identity, version, epoch, and freshness; terminal status; and rollback snapshots. Then Conf s = Caus ∪ Same ∪ Bar ∪ RWM ∪ Snaps , u Is v ⇐⇒ ¬Conf s (u, v) ∧ Enabledu(s) (v) ∧ Enabledv(s) (u) ∧ Ξ(v(u(s))) = Ξ(u(v(s))).

Lemma 4 (AccessSound bridge). If AccessSound(M ) holds and the implemented conflict detector establishes ¬Conf s (u, v) for due transitions u, v, then u Is v. Proof. Conservative access and rollback rules give mutual enabledness, commutativity, and identical future-relevant state. Lemma 5 (Equal-time diamond). If u Is v, then uv and vu reach the same future-relevant state and neither order changes whether a declared property is violated. Proof. This is immediate from Definition 3. Lemma 6 (Canonical representative). Every full equal-time execution is equivalent, by adjacent Is -swaps, to one whose next event belongs to the lexicographically rooted futureclosed component selected by MI-POR. Proof. The future closure pulls every exposed conflict into C ⋆ ; all outside events commute and can be moved by Lemma 5. Theorem 2 (Declared-footprint bounded verdict preservation). For declared event contracts and properties, if AccessSound(M ) and EnableSound(P, B, M ) hold, and Stage 1 is used only when LocalityOK(K; Ω) holds, MI-POR preserves the verifier verdict under the priority U ≻ I ≻ S. When the preserved verdict is S, it also preserves the minimum and maximum terminal completion times. Transparent projection requires Lemma 2. Proof sketch. Lemmas 4–6 retain one representative per equal-time class with identical enabledness, terminal status, state, and labels; TICK occurs only for an empty due set. Under LocalityOK, C⊕ returns U iff a component does; absent U, it returns I iff a component does or Tmax > H. Otherwise Tcomp (π) = maxi Tcomp,i (πi ) preserves the extrema. Lemma 2 handles transparent projection. VI. I MPLEMENTATION a) Trusted computing base and certificate integrity: The trusted computing base comprises the compiler and pinned registry, verifier, certificate validator, and fail-closed executor. Together they bind types, access maps, event contracts, properties, envelopes, identity fields, deadlines, and component digests. Authenticated evidence producers and their transport are part of this boundary. VeraSync only proposes barriers; the verifier and validator must accept each proposal. Runtime evidence releases a gate only when action, scope, version, and epoch match χ. Each of eight action types registers a bounded event DAG, evidence source, RAN footprints, and same-tick enabling dependencies. Missing coverage selects exact search. That engine retains nontransparent ACCEPT/COMPLETE nodes and failclosed gates; Lemma 2 permits the transparent R, D, P, O projection used by larger populations. Mechanism replay sends APER controls through an xApplike path to ns-O-RAN commit 5f547ae8 [12]. Handover APPLY is the serving-cell/RRC transition [13]; O1-bound cell

sleep APPLY is a versioned PHY commit [9]; quota APPLY is the versioned FdTbfqFfMacScheduler update. Packet sinks expose the resulting traffic effects, so APPLY is read from scheduler/PHY state rather than an adapter-side mirror. On OCUDU revision 9b0cfa6, an xApp reaches a gNB through SCTP/E2AP, O-RAN SC, and E2SM-RC Style 2/Action 6 [7], [14], [15]; instrumentation records ACCEPT, slothandler APPLY, executor COMPLETE, return ACK, and the scheduler effect. Table I maps each evaluation layer to the claim it supports. VII. E VALUATION A. Evidence strategy Before sampling, we fixed the generator, repair language, properties, delay envelopes, and analysis protocol. The 144plan confirmation spans six families, 4/8/16 cells, and 4–30 actions, with one plan as the statistical unit. The declared profile sets H = 64 and evidence TTL = 64. Joint sensitivity evaluates H ∈ {64, 96, 128} under both the declared TTL and a horizon-aligned policy TTL = max{64, H}; Figure 2(b) reports the aligned policy. DELIVERY spans 0–1/1–2/1–3 ticks on E2/A1/O1; APPLY spans 1–2 except handover prepare at 1–3; OBSERVE spans 0–1 on E2 and 1–2 on A1/O1. These are symbolic stress bounds. Figure 3 provides millisecondscale mechanism grounding. B. Residual risk after local validation The matched study assigns 192 base cases evenly to energy, mobility/load, and slice/resource plans under urgent or relaxed timing. Horizon/deadline pairs are 12/8 versus 24/20 ticks for energy and slice/resource, and 12/7 versus 20/17 for mobility. Both planners share state, goal, prompt, schema, compiler, verifier, properties, and request seed; all calls compile. A plan is local-pass when its schema, identifiers, action envelope, initial state, request-time preconditions, and individual effects are valid under the declared request order; this gate omits delay and interleaving exploration. The deterministic planners are Qwen3.6-35B-A3B (3B active) and Qwen3-4BInstruct-2507 [16], [17]. Among local-pass outputs, 51/177 35B plans are asynchronously unsafe (28.8%, Wilson 95% CI 22.6–35.9%) versus 119/148 for 4B. Every unsafe 35B plan starts and ends safely and is safe atomically; the 51 violations divide into 25 lifecycle-ordering and 26 cross-path resource cases. They occur in 50/81 urgent versus 1/96 relaxed local-pass plans. Thus 28.8% is the conditional risk in this six-stratum benchmark, with timing pressure providing the mechanism-level attribution. C. VeraSync closes plans with sparse ordering After fixing the generator and repair vocabulary, a prespecified hash selects eight of 16 eligible plans from each of 18 family-by-scale strata. Eligibility requires compilation, satisfaction of the fixed local-pass criteria, and an asynchronous counterexample before repair. Repair outcome and barrier count are not selection inputs. The 144 confirmation plans

have 4–30 actions; 96 combine mechanisms and 136 contain multiple unsafe cores. The portable path lowers each synthesized APPLY-toAPPLY dependency to an APPLY-to-REQUEST gate before pruning. Full verification certifies all 144 plans; none of its 1,400 barriers can be deleted, leaving 86.98% of action pairs unordered with median/P95 completion bounds of 17/17 ticks. When a successor exposes a registered application hook, the direct APPLY-gate path can retain the weaker symbolic order. Verified deletion then removes 140/1,400 barriers across 44 plans and raises the unordered fraction to 89.33%, with median/P95 bounds of 12/14 ticks; every retained set is 1minimal. Over 728 components of at most five actions, an oracle evaluates 42,888 acyclic barrier sets; the applicationgate repair matches all three lexicographic objectives on every plan within the declared APPLY-to-APPLY vocabulary. At H = 64, APPLY- and OBSERVE-gated whole-plan serialization certify 72/144 and 56/144 plans. With H = 128 and horizon-aligned TTL, they reach 144/144 and 104/144. Among plans certified at that setting, P95 completion bounds are 118 and 105 ticks, respectively (Fig. 2(b)). Boundary audits confirm fail-closed behavior: the API recertifies 100/100 expressible controls and returns UNSUP PORTED for 290/290 others; ingestion releases 30/30 clean manifests once, rejects 240/240 static mutations, and blocks dependent release for 90/90 runtime mismatches. D. Authoritative events realize the certificate Figure 3(b) uses 30 matched seeds per policy and mechanism. No-wait release is always unsafe; 60 ms protects 17/30 quota and 23/30 handover–sleep runs. ACCEPT protects 0/30 quota but 30/30 handover runs, where a fixed path delay places sleep APPLY 6.786 ms after the serving-cell transition. This incidental protection does not make ACCEPT authoritative. COMPLETE and direct APPLY protect every run, demonstrating that authority is contract-specific rather than inferred from an ACK label. In the 480-run delay-shift sweep, a 120-ms wait is safe in 30/30 nominal D0 runs but 23/30 stressed D1 runs; direct APPLY remains 30/30 and finishes 62 ms sooner than that wait at the D0 median (Fig. 3(a)). Across 30 OCUDU controls spanning 1/2/4 backlogged UEs and 0/50-ms pre-APPLY delay, the xApp-to-DU/MAC path preserves Ra ≺ρ Aa ≺ρ Pa ≺ρ Ca ≺ρ ACKa ,

θa (Aa ) ≤ θa (Pa ),

ACCEPT and APPLY may share a timestamp but remain distinct events. Every request has one matching APPLY, fresh version, and scheduler effect. Median ACCEPT-to-APPLY separation is 0.455/50.897 ms; COMPLETE-to-return-ACK is 0.615/0.720 ms, placing both completion signals downstream of APPLY on this contract. Intervals use the same host clock without overhead subtraction. E. MI-POR preserves outcomes and reduces search MI-POR matches exact verdicts, first violations, and completion extrema on all 130 property-stratified cases (78 unsafe,

TABLE I E VIDENCE COVERAGE . P LAN CERTIFICATION ESTABLISHES CROSS - ENDPOINT COVERAGE ; REPLAY AND THE LIVE E2 AUDIT GROUND EVENT BINDINGS . Validation layer

Scope

Lifecycle evidence

Establishes

Cross-endpoint certification

144 plans: A1+E2 (48), A1+E2+O1 (80), E2+O1 (16)

Per-action versioned APPLY/OBSERVE evidence under endpoint-specific contracts and delay envelopes

Mechanism-grounded replay

E2 handover and quota; O1-bound cell sleep

Independent live contract audit

OCUDU E2SM-RC Style 2/Action 6, 30 controls

Serving-cell transition, scheduler version update, PHY sleep commit, HandoverEndOk, and packet sinks DU/MAC APPLY, executor COMPLETE, return ACK, and scheduler effect

Plan-level safety and bounded completion; portable REQUEST-gate lowering and registered application-gate repair Certificate-to-mechanism event binding and release behavior

Local reject

a

Safe outcome

Unsafe / property violation

Live ACCEPT/APPLY/COMPLETE ordering on the audited OCUDU E2SM-RC path

Completion horizon

Residual trajectory risk across 384 matched planner outputs

Timeout

Conditional estimate · Wilson 95% CI

119/148 · 80.4%

Qwen3-4B

urgent 88.5 · relaxed 76.0

51/177 · 28.8%

Qwen3.6-35B

urgent 61.7 · relaxed 1.0

Energy urgent

b

Energy relaxed

Mobility / load urgent

Mobility / load relaxed

Slice / resource urgent

Slice / resource relaxed

0

50

Sparse causal repair preserves parallelism and deadline headroom

Aggregate counts 144

VeraSync APPLY → REQ

72

OBS → REQ

Unordered pairs (%)

100

Async-unsafe / local-pass (%)

72

56

88

Deadline headroom · aligned TTL · S+C at H/1.5H/2H

100

× exceeds 2H

80

60 S · 4–10 actions

M · 12–20 actions

L · 20–30 actions

VeraSync

144/144/144

APPLY → REQ

72/104/144

OBS → REQ

56/72/104

0

Plans sorted by profile, action count, family, and plan ID

H

1.5H

2H

Envelope-max completion T/H

3H

Fig. 2. Local validity leaves trajectory risk that sparse repair can close. (a) Matched planner outputs with Wilson 95% intervals. (b) Application-gate repair and release baselines on 144 confirmations; boxes show median/IQR, whiskers P5–P95, and crosses plans beyond 2H.

26 safe, 26 repaired) and 1,120 directed or seeded-random cases, including 387 multi-component plans. The six-event reference passes 56 nontransparent contracts and 256 valid projections; hidden-dependency and access-class mutations trigger the expected fallback or exact-versus-reduced witness. On 20/30/40-action workloads, the full pipeline cuts states from 17,741/24,925/35,481 to 890/1,335/1,780 (94.6–95.0%) and median time by 37.7–40.9×; P95 latency is 90/191/327 ms. Stage 1 supplies the full state reduction on these decomposable plans (Fig. 4(a)). On connected 60/80/100-action workloads, Stage 2 reduces states by 13.2%, peak RSS by 9.0–10.6%, and median runtime by 12.5–13.3% beyond decomposition. Median time falls from 12.0/20.9/32.2 s to 10.6/18.1/27.9 s; the decomposable control shows no added state pruning (Fig. 4(b)).

F. Deployment profiles VeraRAN certifies against registered event contracts, properties, and delay envelopes. Missing access or same-tick coverage selects exact search; missing or mismatched evidence closes the gate. A versioned mutation lease or endpoint precondition protects the resource footprint, and each release rechecks resource and registry versions, endpoint epoch, lease, and deadline. Any mismatch requires re-certification. The 20–40-action profiles model online plans; connected 60–100action profiles model policy/configuration workflows. New actions register event contracts plus access and enablement summaries. Bounded completion assumes registered endpoints and authenticated producers honor the registered request and lifecycle delay bounds in D and {δa }a∈A ; otherwise the gate stays closed until manifest expiry at td .

a Fixed waits become stale as APPLY shifts D0 · APPLY 20–120 ms

Plan completion (ms)

200

0

5

12

19

24

b Release authority depends on mechanism D1 · APPLY 40–180 ms

safe runs (/30) 29

30

30

0

0

5

8

safe runs (/30)

15

19

23

30

160

Property safe Property violation

Quota migration

120

0/30

17/30

0/30

30/30

30/30

0/30

23/30

30/30

30/30

30/30

No wait

60 ms

ACCEPT

COMPLETE

direct APPLY

80 Handover → sleep 40 0

20

40

60

80

100 120 direct APPLY

0

Fixed wait (ms) or direct APPLY

c

20

40

60

80

100 120 direct APPLY

Fixed wait (ms) or direct APPLY

Each mark is one matched run

Live E2 separates ACCEPT from APPLY

No injected delay

+50-ms pre-APPLY

ACCEPT → APPLY

COMPLETE → return ACK

0.2

1

5

20

50

Observed event separation (ms)

Fig. 3. Authoritative release adapts to actuation delay. (a) Fixed-wait/direct-APPLY sweep (480 runs). (b) Mechanism-grounded release replay; each mark is one matched run (300 runs). (c) Live E2 ACCEPT-to-APPLY separation (30 controls).

a MI-POR cuts end-to-end certification cost

Wall time (s, log)

10

b Future-closed Stage 2 cuts residual cost

Additional reduction over Stage 1 (%)

2

Plan actions

Exact live-state Full MI-POR 101

Runtime 37.7×

Connected mixed stress plans

40.1×

10−1

20 repetitions per method and size · bars: P5–P95

20 Explored states 94.6–95.0% fewer

30

Plan actions 17,741 → 890

24,925 → 1,335

80

100

13.2%

13.3%

12.0→10.6 s 11.1--13.0%

20.9→18.1 s 12.8--13.9%

32.2→27.9 s 12.6--14.0%

States

13.2%

13.2%

13.2%

Peak RSS

10.6%

9.0%

9.7%

40.9×

100

60 12.5%

40 35,481 → 1,780

Decomposable control: 0% additional state pruning · runtime overhead 0.3–1.7%

Fig. 4. MI-POR reduces certification cost at both stages. (a) Median wall time, P5–P95, and states (20 runs per size). (b) Residual Stage 2 savings; cells include absolute median seconds and P5–P95, with a decomposable control below.

VIII. R ELATED W ORK RAN control and conflict handling. O-RAN distributes control across E2, A1, and O1 [5], [7]–[9]. Existing systems characterize, mitigate, or block xApp conflicts [18]–[26]. VeraRAN certifies an already selected plan over bounded cross-endpoint trajectories. Consistent updates and synchronization repair. Consistent updates schedule SDN changes, while NICE and SDNRacer expose interleavings [27]–[31]. Synchronization synthesis inserts dependencies over program or network transitions [32], [33]. These methods do not generally bind a synthesized order to authoritative external lifecycle evidence. VeraSync adds version- and scope-checked REQUEST gates

or application hooks, then re-certifies safety and bounded completion. Formal verification and runtime evidence. Formal ORAN models verify energy and availability, while agentic model checking verifies generated programs [34], [35]. VeraRAN instead models action lifecycles, explores bounded trajectories before actuation, and records which versioned event may release each gate. Partial-order reduction. MI-POR builds on distributed event ordering [36], representative executions [37], and POR/DPOR/source sets [38]–[43]. It specializes independence with lifecycle, resource, evidence, completion, repair, and rollback footprints, including same-tick successors exposed by gates.

IX. C ONCLUSION VeraRAN certifies asynchronous RAN plans under peraction event contracts. VeraSync compiles supported counterexamples into version- and scope-bound gates and recertifies the plan. All 144 confirmations certify while leaving 86.98% of action pairs unordered with portable REQUEST gates and 89.33% with application hooks. Live E2 measurements ground release authority; MI-POR removes 94.6–95.0% of states. R EFERENCES [1] E. Oh, B. Krishnamachari, X. Liu, and Z. Niu, “Toward dynamic energyefficient operation of cellular network infrastructure,” IEEE Communications Magazine, vol. 49, no. 6, pp. 56–61, 2011. [2] G. Y. Li, Z. Xu, C. Xiong, C. Yang, S. Zhang et al., “Energy-efficient wireless communications: Tutorial, survey, and open issues,” IEEE Wireless Communications, vol. 18, no. 6, pp. 28–35, 2011. [3] P. Caballero, A. Banchs, G. de Veciana, and X. Costa-Pérez, “Multitenant radio access network slicing: Statistical multiplexing of spatial loads,” IEEE/ACM Transactions on Networking, vol. 25, no. 5, pp. 3044– 3058, 2017. [4] A. Garcia-Saavedra and X. Costa-Pérez, “O-RAN: Disrupting the virtualized RAN ecosystem,” IEEE Communications Standards Magazine, vol. 5, no. 4, pp. 96–103, 2021. [5] M. Polese, L. Bonati, S. D’Oro, S. Basagni, and T. Melodia, “Understanding O-RAN: Architecture, interfaces, algorithms, security, and research challenges,” IEEE Communications Surveys & Tutorials, vol. 25, no. 2, pp. 1376–1411, 2023. [6] M. Hoffmann, S. Janji, A. Samorzewski, L. Kulacz, C. Adamczyk et al., “Open RAN xApps design and evaluation: Lessons learnt and identified challenges,” IEEE Journal on Selected Areas in Communications, vol. 42, no. 2, pp. 473–486, 2024. [7] O-RAN Alliance, “E2 interface: Application protocol (E2AP),” O-RAN Alliance, Tech. Rep. O-RAN.WG3.E2AP-R003-v03.00, 2023. [8] ETSI, “A1 interface: General aspects and principles,” European Telecommunications Standards Institute, Tech. Rep. ETSI TS 103 983 V3.1.0, Jan. 2024, o-RAN.WG2.A1GAP-R003-v03.01. [9] ——, “O-RAN operations and maintenance interface specification,” European Telecommunications Standards Institute, Tech. Rep. ETSI TS 104 043 V11.0.0, Jun. 2024, o-RAN.WG10.O1-Interface-R003-v11.00. [10] L. Bonati, S. D’Oro, M. Polese, S. Basagni, and T. Melodia, “Intelligence and learning in O-RAN for data-driven NextG cellular networks,” IEEE Communications Magazine, vol. 59, no. 10, pp. 21–27, 2021. [11] M. Elkael, S. D’Oro, L. Bonati, M. Polese, Y. Lee et al., “AgentRAN: An agentic AI architecture for autonomous control of open 6G networks,” IEEE Communications Magazine, pp. 1–7, 2026, early access. [12] A. Lacava, M. Bordin, M. Polese, R. Sivaraj, T. Zugno et al., “ns-ORAN: Simulating O-RAN 5G systems in ns-3,” in Proc. Workshop on ns-3, 2023, pp. 35–44. [13] ETSI, “5G; NR; radio resource control (RRC); protocol specification,” European Telecommunications Standards Institute, Tech. Rep. ETSI TS 138 331 V18.6.0, Jul. 2025, 3GPP TS 38.331 Release 18. [14] O-RAN Alliance, “E2 service model (E2SM) RAN control,” O-RAN Alliance, Tech. Rep. O-RAN.WG3.E2SM-RC-R003-v03.00, 2023. [15] OCUDU Project, “OCUDU: Open-source 5G and beyond CU/DU,” https://gitlab.com/ocudu/ocudu, 2026, revision 9b0cfa600d9d693bf56277e4575dc8c4b8b729bb; accessed July 2026. [16] Qwen Team, “Qwen3.6-35B-A3B model card,” https://huggingface. co/Qwen/Qwen3.6-35B-A3B, 2026, experimental revision 1a5ae24e867f8d82388070d3f61590158a01d15c; accessed July 2026. [17] ——, “Qwen3-4B-Instruct-2507 model card,” https:// huggingface.co/Qwen/Qwen3-4B-Instruct-2507, 2025, revision cdbee75f17c01a7cc42f958dc650907174af0554; accessed July 2026. [18] P. B. del Prever, S. D’Oro, L. Bonati, M. Polese, M. Tsampazi et al., “PACIFISTA: Conflict evaluation and management in open RAN,” IEEE Transactions on Mobile Computing, vol. 24, no. 10, pp. 10 590–10 605, 2025. [19] A. E. Giannopoulos, S. T. Spantideas, G. Levis, A. S. Kalafatelis, and P. Trakadas, “COMIX: Generalized conflict management in O-RAN xApps—architecture, workflow, and a power control case,” IEEE Access, vol. 13, pp. 116 684–116 700, 2025.

[20] C. Adamczyk and A. Kliks, “Conflict mitigation framework and conflict detection in O-RAN Near-RT RIC,” IEEE Communications Magazine, vol. 61, no. 12, pp. 199–205, 2023. [21] A. Wadud, F. Golpayegani, and N. Afraz, “QACM: QoS-aware xApp conflict mitigation in open RAN,” IEEE Transactions on Green Communications and Networking, vol. 8, no. 3, pp. 978–993, 2024. [22] C. Adamczyk and A. Kliks, “ACCoRD: Actor-critic conflict resolution with deep learning for O-RAN xApps,” in Proc. IEEE INFOCOM Workshops, 2026, pp. 1–6. [23] D. C. Kwon and X. Zhang, “Open RAN conflict agents: Detecting and mitigating xApp conflicts with generative agents,” in Proc. IEEE INFOCOM, 2026, pp. 1–10. [24] A. Sultana, C. Adamczyk, M. Roy Chowdhury, A. Kliks, and A. Da Silva, “Experimental evaluation of xApp conflict mitigation framework in O-RAN: Insights from testbed deployment in OTIC,” in Proc. IEEE INFOCOM Workshops, 2025, pp. 1–6. [25] H. Gelban, R. Naim, and A. Badawy, “Detecting out-of-order control messages in O-RAN: Dataset, benchmarks, and early-warning models,” IEEE Open Journal of the Communications Society, vol. 7, pp. 1941– 1957, 2026. [26] M. A. Jawad, M. M. H. Munna, A. H. Kabir, N. H. Antu, and R. F. Tulona, “A runtime safety copilot for AI-native O-RAN: Predictive verification and fail-safe enforcement in Near-RT RIC control loops,” IEEE Access, vol. 14, pp. 63 106–63 120, 2026. [27] M. Reitblatt, N. Foster, J. Rexford, and D. Walker, “Consistent updates for software-defined networks: Change you can believe in!” in Proc. 10th ACM HotNets, 2011. [28] M. Reitblatt, N. Foster, J. Rexford, C. Schlesinger, and D. Walker, “Abstractions for network update,” in Proc. ACM SIGCOMM, 2012, pp. 323–334. [29] X. Jin, H. H. Liu, R. Gandhi, S. Kandula, R. Mahajan et al., “Dionysus: Dynamic scheduling of network updates,” in Proc. ACM SIGCOMM, 2014, pp. 539–550. [30] M. Canini, D. Venzano, P. Perešı́ni, D. Kostić, and J. Rexford, “A NICE way to test OpenFlow applications,” in Proc. 9th USENIX NSDI, 2012, pp. 127–140. [31] A. El-Hassany, J. Miserez, P. Bielik, L. Vanbever, and M. Vechev, “SDNRacer: Concurrency analysis for software-defined networks,” in Proc. 37th ACM SIGPLAN PLDI, 2016, pp. 402–415. [32] M. Vechev, E. Yahav, and G. Yorsh, “Abstraction-guided synthesis of synchronization,” in Proc. 37th ACM SIGPLAN-SIGACT POPL, 2010, pp. 327–338. [33] J. McClurg, H. Hojjat, and P. Černý, “Synchronization synthesis for network programs,” in Proc. CAV, vol. 10427, 2017, pp. 301–321. [34] R. Metere, K. Ye, Y. Gu, Z. Zhang, D. Alrajeh et al., “Towards achieving energy efficiency and service availability in 6G O-RAN via formal verification,” in Proc. 12th Int. Symp. From Data to Models and Back (DataMod 2024), ser. Lecture Notes in Computer Science, vol. 15556, 2025, pp. 137–157. [35] Y. Sun, J. Liu, D. Kroening, and J. Xue, “Agentic model checking,” 2026, arXiv:2605.21434. [36] L. Lamport, “Time, clocks, and the ordering of events in a distributed system,” Communications of the ACM, vol. 21, no. 7, pp. 558–565, 1978. [37] D. Peled, “All from one, one for all: On model checking using representatives,” in Proc. CAV, vol. 697, 1993, pp. 409–423. [38] E. M. Clarke, O. Grumberg, and D. A. Peled, Model Checking. MIT Press, 1999. [39] P. Godefroid, Partial-Order Methods for the Verification of Concurrent Systems. Springer, 1996. [40] M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. A. Nainar et al., “Finding and reproducing heisenbugs in concurrent programs,” in Proc. 8th USENIX OSDI, 2008, pp. 267–280. [41] C. Flanagan and P. Godefroid, “Dynamic partial-order reduction for model checking software,” in Proc. 32nd ACM SIGPLAN-SIGACT POPL, 2005, pp. 110–121. [42] P. A. Abdulla, S. Aronis, B. Jonsson, and K. Sagonas, “Optimal dynamic partial order reduction,” in Proc. 41st ACM SIGPLAN-SIGACT POPL, 2014, pp. 373–384. [43] ——, “Source sets: A foundation for optimal dynamic partial order reduction,” J. ACM, vol. 64, no. 4, pp. 25:1–25:49, 2017.

Related documents

• ViBE: Co-Optimizing Workload Skew and Hardware Variability for MoE Serving#246529
• InSPECtor: Improving SLEIGH Processor Specification Veracity via Proxy#615206
• InSPECtor: Improving SLEIGH Processor Specification Veracity via Proxy#614239
• InSPECtor: Improving SLEIGH Processor Specification Veracity via Proxy#451229
• Algorithms for synchronizing network clocks#213377