arXiv CSopen access

Certified Closed-Loop Control for Packet Networks: A Compositional Certification Framework

Certified Closed-Loop Control for Packet Networks: A Compositional Certification Framework Muhammad Bilal∗1 , Jon Crowcroft2 , Xiaolong Xu3 , and Huaming Wu4 1

arXiv:2606.02368v1 [cs.NI] 1 Jun 2026

2

School of Computing and Communications, Lancaster University, United Kingdom Department of Computer Science and Technology, University of Cambridge, Cambridge, United Kingdom, [email protected] 3 School of Computer Science, School of Software, Nanjing University of Information Science and Technology, China, [email protected] 4 Center for Applied Mathematics, Tianjin University, China, [email protected]

Abstract Packet networks are controlled dynamical systems with discontinuities, delayed observations, and partial state information. Adaptive or learning-driven proposers can improve performance, but an unsafe proposal may still cause starvation, tail-delay spikes, or unstable queue behaviour. This paper treats packet-network control as an executed-action certification problem. A certified operator sits between any proposer and the dataplane. At each control tick, the proposer emits an arbitrary candidate action ũ(t). The operator either projects it to an executable action u(t) that satisfies a configuration-compiled certificate, or reports INFEASIBLE and executes an always-defined fallback with quantified slack. The certificate also exports an auditable envelope z̄(t) for downstream composition. The guarantees are conditional and explicit. They apply on ticks where the operator reports CERTIFIED, the declared arrival envelope and backlog bound are valid, and the platform realises the assumed service lower bound. Under these conditions, one mechanism covers backlog caps, service floors, mitigation caps, Foster–Lyapunov drift constraints, and compositional envelope contracts. We prove operator-level safety, feed-forward compositional safety and stability using exported envelopes, and a cyclic closure result under a small-gain condition. We also define breach and infeasibility semantics, discuss calibration of the service-tracking factor that links certified targets to realised scheduler behaviour, and evaluate the design under delayed telemetry, delayed actuation, weak proposers, envelope mismatch, overload, and millisecond-scale certification. The present evaluation validates the certified execution boundary in a byte-level closed-loop backend; deployment-level scheduler tracking is left to future Linux or hardware experiments.

Highlights • Frames packet-network control as certification of the action actually executed at the dataplane. • Separates arbitrary proposers from the certified operator, status flag, slack report, and exported envelope contract. • Provides per-tick constraints for backlog caps, service floors, mitigation caps, and drift-based queue stability. ∗

Corresponding author: Muhammad Bilal. Email: [email protected]

1

• Gives compositional safety and stability results for feed-forward networks, plus cyclic closure diagnostics under a small-gain condition. • Makes the limits of certification explicit through valid-envelope, valid-state-bound, servicetracking, breach, and infeasibility semantics. Keywords Certified closed-loop network control; Packet networks; Safety filtering; Runtime assurance; Compositional certification; Queue stability

1

Introduction

Packet networks are controlled dynamical systems in which scheduling and queueing decide who is served and when, queue management decides what is marked or dropped, routing determines where work flows, and mitigation actions shape or isolate traffic. These mechanisms connect continuous objectives, such as tail delay, fairness, and delivered rate, to discontinuous packet-level dynamics, including integer service, idling, and reflection at zero backlog. Classical mechanisms already show that small control choices can have large effects on delay and stability, including fair queueing, deficit round robin, active queue management, and service abstractions for per-flow guarantees [12, 14, 18, 19, 22]. Queue-drift analysis has long been used to reason about packet-network stability [24, 17]. In this view, the relevant object is the service action executed by the system, rather than the controller’s intended action. That distinction matters in modern packet systems. Data-centre and edge networks often operate at high utilisation, with tail-latency targets and feedback drawn from sampled counters, aggregate telemetry, or in-band summaries rather than direct queue state [1, 20, 16, 4, 23, 29]. Programmable monitoring improves visibility, but it still leaves the controller making some decisions before the full state is known. Network control is also becoming more adaptive. Recent work includes synthesis-style control, learning from expert behaviour, and controllers trained across varied network conditions [26, 13, 28, 27, 7]. The risk is not only poor average performance. Model error, traffic shift, or timed adversarial behaviour can produce starvation, delay spikes, or unstable control actions. Delayed telemetry and delayed actuation make this worse because the controller may recognise the failure only after queues have already grown. Even under simple admissibility rules, worst-case arrivals can increase delay and backlog in ways that average-case reasoning does not predict [8]. This paper asks a deployment-facing question: how can adaptive proposing be combined with strict, online-checkable guarantees for packet queues, in a form that composes across a network? We separate proposal from correctness by placing a certified operator between the proposer and the dataplane. At each control tick, the proposer emits a candidate action ũ(t) from delayed telemetry. In agentic NetOps settings, it may also be a software agent or LLM-based assistant [5]. The operator then enforces constraints compiled from configuration and returns the executed action u(t), an exported envelope z̄(t) for downstream composition, and a status flag indicating whether certification succeeded. The guarantees attach to the executed action u(t), not to the internal logic of the proposer. This “execute through a filter” pattern is close to safety filtering in control, where an arbitrary controller is wrapped by an online feasibility check and a correction step [3, 25]. For composition, we use an envelope-contract view. Modules exchange certified bounds, rather than internal policies. This is adjacent to deterministic envelope reasoning in network calculus, with the difference that the bounds here are enforced at runtime through the operator interface [10, 11]. The paper makes four contributions. First, it formalises a delayed closed-loop model for packet queues and defines a certified-operator interface that compiles a unified, configurationdriven certificate into per-tick constraints. Second, it supports backlog-cap and floor/cap safety constraints, drift-based stability guarantees with explicit constants, and compositional contracts

2

through exported envelopes. Third, it proves operator-level safety, compositional safety, and stability for feed-forward DAG networks using only exported envelopes. It also gives a cyclicnetwork closure result based on an envelope fixed point under a small-gain condition. Fourth, it specifies contract-breach semantics and an always-defined emergency fallback for infeasible constraints. The evaluation covers timing-shaped stress, envelope mismatch, overload, delayed telemetry and actuation, and pinned control-tick runtime microbenchmarks [6]. The envelope layer is designed to work with classical network calculus, not to replace it. Declared arrival envelopes Ā(t) and exported envelopes z̄(t) may be instantiated from arrival-curve and service-curve assumptions, with token-bucket contracts as a standard case [9, 10]. Classical network calculus uses such assumptions to derive deterministic backlog and delay bounds for queueing elements and their composition. Here the emphasis is different: envelopes are used inside an online certified operator that filters arbitrary proposed actions at each control tick. The paper proves operator-level and compositional properties for the abstract queueing model and for the compiled per-tick constraints. It does not claim mechanised verification of the certificate compiler, solver, runtime, or dataplane backend. Strengthening that trusted computing base through translation validation or machine-checked implementation proofs is a natural next step, but outside the scope of this paper [21, 15]. Positioning and scope. Queueing stability and drift-based control provide the mathematical backbone for many packet-network controllers. Max-weight style arguments and Foster–Lyapunov drift give conditions under which queues remain stable under admissible loads [24, 17]. The present paper uses the same discipline, but moves the proof obligation to the action that is executed after online certification. The proposer is not trusted to preserve drift by itself. Network calculus and service-curve methods give deterministic backlog and delay bounds from arrival and service envelopes [10, 11, 9]. Our envelope contracts are deliberately compatible with that tradition. The difference is operational: the envelope is not only an offline assumption used to derive a static bound. It is also an input to a per-tick certification interface that accepts, corrects, or rejects a proposed dataplane action. Safety filters, shielding, and control-barrier-function methods similarly wrap an arbitrary controller with online feasibility checks [3, 2, 25]. Packet queues make this setting less tidy than smooth continuous-state systems. Service is packetised, queues reflect at zero, actuation may be delayed, and the scheduler may realise only a lower-bounded fraction of the requested service target. The certified operator therefore exposes these assumptions as part of its status and diagnostic interface. Verified systems and dataplane-correctness work address a different layer of trust. Translation validation and machine-checked implementations can reduce the trusted computing base of the compiler or runtime [21, 15]. This paper does not claim such mechanised verification. It uses these traditions to define a runtime certification boundary for executed packet-network actions. The certificate compiler, solver implementation, and dataplane backend remain trusted components unless separately verified. Core distinction. Existing adaptive control work often analyses a policy, controller, or intended action. This paper analyses only the action actually executed after certification. The proposer may be heuristic, learned, adversarial, or agentic. Correctness attaches to the certified output u(t), the status flag σ(t), the diagnostic report r(t), and the exported envelope contract z̄(t).

2

Model and platform realisation

Queues and actions. Time is slotted t = 0, 1, 2, . . . with step ∆. For a module (node or link scheduler) M , let qiM (t) ∈ R≥0 denote backlog of class-queue i ∈ {1, . . . , NM } at time t.

3

Table 1: Guarantee semantics exposed by the certified operator. Status or flag

Action taken

Guarantee available

Logged dence

CERTIFIED

Projected action u(t)

Envelope, action, status

INFEASIBLE

Slack-minimising fallback

MISSING_ENVELOPE

Hold-safe or fallback

Safety and drift guarantees, provided the declared envelope, backlog bound, and service-tracking lower bound are valid No hard guarantee; quantified violation under the compiled constraints No compositional guarantee for that tick No state-based safety guarantee for that tick Downstream composition is not valid for that tick

MISSING_STATEBOUND Hold-safe or fallback Breach flag b(t) = 1

Action may still run

evi-

Slack vector Missing contract Missing state bound Breach flag

M Arrivals to module M consist of exogenous arrivals aM i (t) and routed inflow ini (t). The M M module executes service µi (t) ≥ 0 and shedding δi (t) ≥ 0 (drop, admission denial, or policing). Define total removal M M sM (1) i (t) ≜ µi (t) + δi (t). The queue update is   M M qiM (t + 1) = qiM (t) + aM (2) i (t) + ini (t) − si (t) + . Resource constraints define an admissible set. For a bottleneck resource at module M with capacity CM (t), NM X µM µM δiM (t) ≥ 0. (3) i (t) ≤ CM (t), i (t) ≥ 0, i=1

Additional constraints (WFQ weight bounds, class caps, service floors) are modelled as linear inequalities in µM (t). Delayed telemetry and delayed actuation. The proposer observes telemetry y M (t) rather than q M (t). A delayed, noisy measurement model is y M (t) = HM q M (t − τyM ) + ν M (t), (4) M M where HM aggregates counters, τy ≥ 0 is telemetry delay, and ν (t) is measurement noise. Section 5 describes robust handling. Arrival envelopes and adversaries. We assume declared envelopes on arrivals: M ¯M 0 ≤ aM 0 ≤ inM (5) i (t) ≤ āi (t), i (t) ≤ ini (t). Define the total envelope M ¯M ĀM (6) i (t) ≜ āi (t) + ini (t). Adversarial timing shaping is captured by allowing arrivals to be any sequence respecting (5). Correctness is with respect to the declared envelope. This envelope-conditioned viewpoint matches a long line of drift-based queueing control, and it makes the distinction between executed actions and proposed actions explicit in the object that is analysed [17, 24]. The use of envelope-bounded but otherwise unconstrained timing also aligns with worst-case perspectives studied in adversarial queueing [8].

2.1

Service targets and realised removals on commodity schedulers

The model in (2) uses µi (t) as the realised service removal on tick t. On real platforms, the controller often sets weights or rates (WFQ, DRR, HTB), and realised per-tick removals can 4

Table 2: Operational interpretation of the service-tracking factor. The categories are qualitative design guidance only; the present experiments do not estimate deployment-level κmin . Scheduler regime

Tracking reliability

Main source of loss from target

Ideal fluid or long-tick scheduler Packetised WFQ/DRR with active classes HTB or paced queues under cross-traffic Congested software path with NIC batching

high high to moderate

negligible packetisation error quantum, packet size, and class backlogging effects rate policing, burst shaping, batching, and link variability batching delay and short-window service jitter

moderate low to moderate

differ from targets because of packetisation, quantum effects, non-backlogged classes, variable link rate, and cross-traffic. To make this explicit, we interpret the operator output as a service target µtar i (t) and allow a bounded tracking model for realised service: µi (t) ≥ κi (t) µtar κi (t) ∈ [κmin , 1], (7) i (t), where κmin is a conservative platform constant (or an online lower bound) that accounts for scheduler noise and rate variability over one control tick. The operator can stay robust by finding its lower limit on the target variable through κmin . Concretely, if certification requires si (t) = µi (t) + δi (t) ≥ ℓi (t), it is sufficient to enforce κmin µtar (8) i (t) + δi (t) ≥ ℓi (t). While this approach is cautious, it reflects how deployments actually operate. We authenticate based on the functionality that the platform can guarantee, rather than on an idealized clock-level scheduler. In the experiments we log the realised tracking ratio µi (t)/µtar i (t) to show when this conservatism matters. Estimating κmin in deployment. The service-tracking factor should be treated as a calibrated platform parameter, not as a free modelling convenience. During a calibration window of Wκ ticks, the controller logs the target service µtar i (t) and the realised removal µi (t) for each backlogged class. It then computes   µi (t) κ bi = Qpκ : t ∈ Wκ , qi (t) > 0 , (9) max{µtar i (t), ηµ } where Qpκ is a low empirical quantile, for example pκ = 0.01, and ηµ > 0 avoids division by zero. A conservative deployment uses κmin = max{κfloor , min κ bi − mκ }, (10) i

with margin mκ and a configured lower floor κfloor . The estimate may be refreshed only when the platform is in a stable regime and the observed breach rate is low. Otherwise it is frozen. This prevents a transient overload period from silently weakening the certificate.

3

Unified certificate mechanism and configuration

M (t) over actions. We express At each time t, certification induces a certified feasible set Ucert certificates in a form that can be compiled from configuration and checked online.

Type B: barrier certificates for safety Fix backlog caps QM,max > 0 and define the safe set i M,max NM M M M S = {q ∈ R≥0 : qi ≤ Qi ∀i}. (11) A sufficient one-step barrier condition for forward invariance under (2) and (5) is M,max M qiM (t) + ĀM ∀i, (12) i (t) − si (t) ≤ Qi

5

equivalently, M,max M M sM ∀i. (13) i (t) ≥ qi (t) + Āi (t) − Qi Safety often includes linear constraints such as service floors for protected classes P M , M µM ∀i ∈ P M , (14) i (t) ≥ ϕi CM (t), M and mitigation caps for flagged classes F (t), M µM ∀i ∈ F M (t). (15) i (t) ≤ ρi CM (t), Figure 8 illustrates why explicit floors/caps are needed: without them, a proposer can induce a priority inversion in which the latency class tail delay degrades sharply while the bulk class appears artificially good.

Type A: drift certificates for stability Fix high thresholds QM,hi ∈ (0, QM,max ) and margins i i εM > 0. The drift trigger is i M M qiM (t) ≥ QM,hi ⇒ sM (16) i (t) ≥ Āi (t) + εi . i This is enforced online and yields an explicit Foster–Lyapunov drift bound (Section 6). Type C: contract certificates for composition For each directed interconnection U → V , define the realised outflow signal zU →V (t) that enters downstream as inflow. A contract certificate exports an envelope 0 ≤ zU →V (t) ≤ z̄U →V (t), (17) and downstream assumes X ¯ V (t) ≥ in z̄U →V (t). (18) U ∈Pred(V )

Modules exchange bounds, not internal policies. Contract mechanics. This section gives only the interface. Section 7 defines how realised inter-module flow z and exported envelopes z̄ are computed from executed removals, including the physical cap that prevents a module from exporting more work than backlog plus envelope arrivals.

3.1

Certificates as configuration and feasibility diagnostics

For each class i at module M , the configuration specifies queue limits, tolerance margin, optional caps, and the action form:
M,max (19) ΘM , QM,hi , εM i = Qi i , optional caps, action parameterisation . i The action parameterisation maps an executed decision to platform knobs such as WFQ weights, HTB rates, or policing rates. Compilation to constraints. At each tick, the operator uses ΘM and the local information M (t; ΘM ). The construction compiles these set I M (t) to construct the certified feasible set Ucert fields into: • barrier constraints enforcing (12) and any optional floors or caps, • drift constraints enforcing (16) when active, • resource constraints enforcing (3) and action limits, • contract rules defining the exported envelopes in (17). Proof obligations checked by the operator. Theorems in this paper apply on ticks where σ M (t) = CERTIFIED. Certification requires: (i) envelopes ĀM (t) are present and nonnegative, (ii) capacity and action limits are present, (iii) drift activation and barrier constraints are built using

6

q M (t) when telemetry is delayed or bounded, (iv) exported envelopes z̄ M (t) are computed from the executed action uM (t), not the proposal ũM (t), and (v) infeasibility is reported explicitly (no silent fallback). A single feasibility lemma for CERTIFIED. We state one reusable feasibility condition that explains when CERTIFIED is expected and when INFEASIBLE is unavoidable. Let ℓi (t) be the compiled per-class lower bound on total removal si = µi + δi at time t induced by safety and drift constraints (with the operator’s chosen state bound and envelope). Let optional per-class service floors/caps be µi ≥ µi and µi ≤ µi , and let δi ≤ δ i be an optional shedding cap (take δ i = ∞ if uncapped). Lemma 1 (Sufficient feasibility condition). Fix t and suppose the operator has the required inputs (state bound, envelope, and capacity). Define a conservative service requirement ri (t) ≜ max{ µi , ℓi (t) − δ i }, (20) with the convention ℓi − δ i = −∞ when δ i = ∞. If there exists µ ∈ RN ≥0 such that X µi ≤ C(t), ri (t) ≤ µi ≤ µi ∀i,

(21)

i

then there exists an action (µ, δ) satisfying all compiled linear constraints with zero slack, and hence the certified feasible set Ucert (t) is nonempty. In this case, the projection-based operator can report CERTIFIED (up to solver and numerical tolerances). The condition says: after you account for any allowed shedding δ i , the remaining per-class requirement must fit inside capacity and service floors/caps. With actuation delay, the apply-time compilation in Section 5 increases the effective lower bounds ℓi (t) because the operator must protect against arrivals during the delay window while actions are still in flight. Thus Lemma 1 is also the diagnostic test for when certification is structurally possible at a tick.

4

Certified operator and closed-loop realisation

We now define the certified operator, which is the only component allowed to emit the executed action. Definition 1 (Certified operator). Fix a certificate configuration Θ (Section 3.1). The certified operator is a map

M M uM (t), z̄ M (t), σ M (t), rM (t) = CΘ I (t), ũM (t) , (22) where I M (t) contains a backlog estimate or bound, a total envelope ĀM (t), capacity and action limits, and the proposal ũM (t). The outputs are the executed action uM (t), exported envelope z̄ M (t), status flag σ M (t), and diagnostic report rM (t). Status semantics. The status flag takes values in a small set: (23) σ M (t) ∈ {CERTIFIED, INFEASIBLE, MISSING_ENVELOPE, MISSING_STATEBOUND}. M Breach is recorded separately through b (t), because a breach concerns the validity of the declared contract rather than only the feasibility of the projection. Table 1 summarises the resulting guarantee semantics. All theorems in this paper apply to time steps for which σ M (t) = CERTIFIED, bM (t) = 0, the state bound is valid, and the realised service satisfies the tracking lower bound. If any of these conditions fail, the operator still returns a logged action and diagnostic report, but the hard guarantee is not claimed for that tick.

7

4.1

Contract validity and infeasibility semantics

Envelope breach indicator. Let the realised total arrival be AM (t) ≜ aM (t) + inM (t). Define the per-tick breach indicator as bM (t) ≜ I{AM (t) > ĀM (t) + ηA }, (24) where ηA ≥ 0 is a measurement tolerance. Breaches are recorded explicitly and determine when downstream envelope contracts may be used, as described in Section 7. Always-defined behaviour under infeasibility. Infeasibility is expected under overload or under constraints that are too tight for the available capacity. A mechanism that becomes undefined under stress is a poor operational bargain. It is also easy to exploit. For this reason, the emergency policy is part of the operator semantics. Emergency policy: minimise barrier slack. When the certified constraints are infeasible, the operator solves a relaxed projection with explicit nonnegative slack variables. Let u = (µ, δ), and let ℓi (t) denote the compiled lower bound on si = µi + δi induced by safety and drift constraints. With slack vector ξ ≥ 0, the operator solves min ∥u − ũ∥2WM + α 1⊤ ξ (25) µ,δ,ξ X s.t. µi ≤ CM (t), µ ≥ 0, δ ≥ 0, (26) i

(µi + δi ) + ξi ≥ ℓi (t) ∀i. (27) ⋆ If the optimum has ξ = 0, the operator reports CERTIFIED. Otherwise, it reports INFEASIBLE and returns (u⋆ , ξ ⋆ ). Thus behaviour is always defined, and the violation is exported as a quantified and auditable signal. The slack ξ ⋆ certifies how far the system is from satisfying its hard constraints under the current capacity and declared envelopes. The slack ξ ⋆ separates two regimes. When ξ ⋆ = 0, the original guarantees apply on valid certified ticks. When ξ ⋆ > 0, the operator has reached a structurally infeasible point and returns the best-effort action under the stated slack criterion, and produces INFEASIBLE tick. Such INFEASIBLE ticks can arise even with a perfect proposer, for example under very tight Qmax , large envelopes, actuation delay τu , or insufficient resources. We therefore report both the INFEASIBLE fraction and the slack magnitude as diagnostic quantities.

4.2

Certified closed-loop control

The proposer, whether learned or heuristic, observes telemetry history y M (≤ t) and emits a candidate action ũM (t). ũM (t) = πθM (ϕM (y M (≤ t))). (28) M M M In the basic parameterisation, ũ (t) = (µ̃ (t), δ̃ (t)). Certified projection: operator realisation. The certified operator returns platform-level targets, written as (µtar (t), δ(t)). When the platform implements these targets, realised removals satisfy the bounded tracking model in Section 2.1. uM (t) = arg

min

M (t;ΘM ) u∈Ucert

∥u − ũM (t)∥2WM , (29)

M

when σ (t) = CERTIFIED. For bottleneck scheduling with µM and δ M , a practical convex form is the following small

8

quadratic programme: min

∥µM − µ̃M ∥22 + λM ∥δ M − δ̃ M ∥22 + MM 1⊤ δ M X s.t. µM µM δiM ≥ 0, i ≤ CM (t), i ≥ 0,

µM ,δ M

i M,max M M M qi (t) + ĀM ∀i, i (t) − (µi + δi ) ≤ Qi M,hi M M M M qi (t) ≥ Qi ⇒ (µi + δi ) ≥ Āi (t) + εM i

(30) (31) (32)

∀i, (33) with optional linear constraints such as (14) and (15). In implementation, the implication in (33) is enforced by activating the constraint for every index with qiM (t) ≥ QM,hi . i

Figure 1: Certificate-induced projection geometry by class. Left: drift inactive. Right: drift active for class 1. The hatched polygon shows the feasible set induced by the certificate in the (µ1 , µ2 ) plane, measured in bytes per tick. The set is bounded by the capacity C and the compiled per-class lower bound ℓ. Figure 1 illustrates the projection view. The certificate induces a convex feasible region in the (µ1 , µ2 ) plane, and the executed action is the metric projection of the proposal onto that region. When drift is inactive, the feasible set is broad. When drift activates for class 1, the lower bound tightens, the feasible set shrinks, and the projection shifts service toward that class while preserving the capacity constraint. If the feasible set is empty, the operator reports INFEASIBLE and enters the slack-handling mode. Operator-level safety theorem. Theorem 2 (Safety of the certified operator). Assume (5). Consider a module M whose operator M reports σ M (t) = CERTIFIED at time t. Suppose the state used for certification is valid for CΘ the current queue state, and the operator enforces the barrier constraint (12) using the declared arrival envelope ĀM (t). If q M (t) ∈ S M , then q M (t + 1) ∈ S M . Consequently, if q M (0) ∈ S M , the required envelopes and state bounds remain valid, and σ M (t) = CERTIFIED for all t, then q M (t) ∈ S M for all t ≥ 0.

5

Delay, partial observability, and algorithms

Envelope and state-bound construction for deployment. The operator interface needs two quantities. The first is a declared arrival envelope Ā(t). The second is a certified backlog interval, q(t) ∈ [q(t), q(t)].

9

The theorem above treats these quantities as valid inputs. In deployed packet systems, however, they must be constructed from delayed counters, sampled telemetry, and local traffic assumptions. We now describe this construction. In practice, Ā(t) is obtained in one of three ways, depending on what the operator is allowed to assume. 1. Policy envelope (contracted). For traffic classes with explicit contracts (tenant limits, policers, admission control), the envelope is specified by configuration, for example tokenbucket style: Ā(t) = min{B + R∆, Āmax }, (34) where R is a configured rate, B is a burst budget, and ∆ is the control interval. This is the most direct point of contact with network calculus: a token-bucket contract is an arrival-curve style assumption. In our framework, however, it serves as an input contract to runtime certification rather than as the whole analysis. 2. Empirical envelope (calibrated). When no explicit contract exists, we calibrate Ā(t) from a recent history window of measured arrivals, using a high quantile and a slack margin:
Ā(t) = Qp {A(τ )}t−1 (35) τ =t−W + mA , where Qp (·) is the empirical p-quantile (e.g., p = 0.99 or 0.999), W is a window length in ticks, and mA is a configured safety margin. 3. Hybrid envelope (policy plus calibration). A common compromise is to cap the empirical envelope by a configured maximum and to floor it by a minimum contract:  Ā(t) = min Āmax , max{Āmin , Qp (·) + mA } . (36) Backlog bounds from delayed counters and local accounting. Let the platform expose a delayed backlog-related signal at time t (a queue occupancy counter, a byte backlog estimate, or an aggregate) of the form y(t) ≈ q(t − τy ), possibly with aggregation and noise as in (4). To obtain a bound at the current tick, we use two facts that are available to the controller: (i) the declared envelope upper-bounds arrivals between counter samples, and (ii) the controller knows the actions it has already scheduled to apply (including any actuation buffer). A simple upper bound is: τy −1 τy −1 h i X X q(t) = y(t) + Ā(t − τy + s) − ŝ(t − τy + k) + ηq , (37) s=0

+

k=0

where ŝ(·) is the realised (or conservatively lower-bounded) total removal scheduled/applied on each tick and ηq ≥ 0 is a tolerance that absorbs counter noise, timestamp jitter, and aggregation error. If the platform provides a conservative removal lower bound ŝmin (·) (Section 2.1), then (37) remains valid by substituting ŝmin . If only an upper bound on removal is available, we keep safety conservative by relying on (37) only (upper-bound mode). A matching lower bound is optional in the core mechanism. When required (for example, to reduce conservatism in drift-trigger activation), a standard conservative construction is: τy −1 h i X q(t) = y(t) − ŝmax (t − τy + k) − ηq , (38) +

k=0

with ŝmax an upper bound on applied removals. We clip q(t) at 0. When only bounds are available, the operator substitutes q(t) wherever q(t) appears in safety constraints. Drift activation also uses q(t) in the conservative mode. Thus the notation is fixed throughout: safety constraints are certified against the upper backlog bound, while q(t) is used only when a lower bound is explicitly needed. Applied-action consistent certification under actuation delay (conservative). The operator can be read as a domain-specific safety filter: a proposer supplies a candidate action, 10

Algorithm 1 Certified operator step at module M (per time tick) Require: Telemetry history y M (≤ t), bounds [q M (t), q M (t)], exogenous envelope āM (t), inflow ¯ M (t), capacity CM (t) envelope in ¯ M (t) 1: ĀM (t) ← āM (t) + in 2: Proposer outputs (µ̃M (t), δ̃ M (t)) ← πθM (ϕM (y M (≤ t))) 3: Compile per-tick certificate constraints from ΘM using q M (t) and ĀM (t) 4: Solve projection to obtain executed (µM (t), δ M (t)) and set status σ M (t) 5: Export envelopes z̄M →V (t) and diagnostics r M (t) 6: Apply action (immediately or with actuation delay) and update queues via (2)

and an online projection step enforces safety and feasibility [3, 2, 25]. With actuation delay, the operator chooses u(t) now, but the system applies u(t) at t + τu . Meanwhile, actions already placed in the actuation pipeline will be applied on ticks t, t + 1, . . . , t + τu − 1. Action buffer model. Let ŝi (t + k) denote the total removal already scheduled to be applied at future tick t + k from actions chosen earlier (this is known to the controller because it is the controller’s own buffer). Let q i (t) be a valid upper bound on current backlog and let Āi (t + s) be the declared envelope over the delay window. A conservative apply-time bound. A mechanically checkable upper bound on the backlog just before u(t) takes effect is τX τX u −1 u −1 i h ŝi (t + k) . (39) Āi (t + s) − q iapply (t + τu ) ≜ q i (t) + s=0

k=0

+

Applied-action barrier constraint. To ensure the backlog cap at the first tick when the new action is applied, it is sufficient to enforce q iapply (t + τu ) + Āi (t + τu ) − sexec (t) ≤ Qmax , (40) i i exec where si (t) = µi (t) + δi (t) is the removal implied by the executed action returned by the operator at time t. Applied-action drift trigger. A conservative version activates drift using q iapply (t + τu ) and enforces exec q iapply (t + τu ) ≥ Qhi (t) ≥ Āi (t + τu ) + εi . (41) i ⇒ si

5.1

Algorithms

Algorithm 1 is the core online loop for one module M (a queueing/scheduling element). Inputs are deliberately minimal and match what deployments typically have: (i) telemetry history y M (≤ t), which may be delayed and noisy, (ii) a backlog bound [q M (t), q M (t)] (or only q M (t) in the simplest mode), (iii) declared envelopes for exogenous and inflow arrivals, which combine into a total envelope ĀM (t), and (iv) a capacity estimate CM (t) and action limits. The operator compiles three kinds of certificates into constraints: barrier-style safety caps (Type B), drift triggers (Type A), and contract rules that define exported envelopes (Type C). It then solves a projection (or uses a closed-form fast path when applicable) to obtain an executed action that is feasible with respect to these constraints. If the constraints are infeasible, the operator reports this explicitly through σ(t) (and, if enabled, returns an emergency action with quantified slack as in Section 4.1). The module then applies the executed action (immediately or after actuation delay) and updates the queue state by (2). 11

For completeness, we give the DAG propagation, cyclic closure, and stress harness algorithms in Appendix A.1.

6

Stability guarantees

The safety condition can be read as a queue-domain analogue of barrier-function feasibility enforced online by a correction step, while the stability condition is deliberately aligned with drift-style arguments used throughout queueing-network control [3, 2, 17]. We give a Foster– Lyapunov drift result aligned with the enforced drift trigger. For clarity, we drop the module superscript and write qi (t), Āi (t), and si (t). P 2 Lemma 3 (One-step quadratic drift bound). Let V (q) = N i=1 qi . For the update qi (t + 1) = [qi (t) + xi (t)]+ with xi (t) = Ai (t) − si (t), it holds that N N X X V (q(t + 1)) − V (q(t)) ≤ 2 qi (t) xi (t) + xi (t)2 . (42) i=1

i=1

Theorem 4 (Foster–Lyapunov stability under certified drift trigger). Assume 0 ≤ Ai (t) ≤ Āi (t) ≤ Āmax < ∞ and 0 ≤ si (t) ≤ s̄i < ∞ for all classes i = 1, . . . , N and all t. Fix thresholds i Qhi > 0 and margins εi > 0, and suppose the executed action satisfies i qi (t) ≥ Qhi ⇒ si (t) ≥ Āi (t) + εi , ∀i, ∀t. (43) Pi hi . Define Let εmin ≜ min1≤i≤N εi and B0 ≜ N Q i=1 i N X  hi max  e ≜ e 2Qi Āi + (Āmax + s̄i )2 , β ≜ 2εmin B0 + K. (44) K i i=1

Then, for all t, where V (q) =

E[V (q(t + 1)) − P V (q(t)) | q(t)] ≤ −2εmin ∥q(t)∥1 + β, N 2 and ∥q(t)∥ = q 1 i=1 i i=1 qi (t). In particular, T −1 1 X β lim sup E[∥q(t)∥1 ] ≤ . T 2ε min T →∞

(45)

PN

(46)

t=0

Alignment with the operator. Condition (43) is exactly the drift trigger (16) enforced when σ(t) = CERTIFIED with Ai = Āi . Thus the theorem applies to executed actions by construction, independent of proposer quality.

7

Envelope contracts and compositional guarantees

7.1

Contract semantics: how z and z̄ are computed

We make the contract signals concrete so that composition is mechanically checkable. Routing model. Fix a routing specification for each edge U → V . In the simplest (and common)Pcase, each class i at U forwards a fixed fraction rU →V,i ∈ [0, 1] of its removals to V , with V rU →V,i ≤ 1 (the remainder exits the modelled network). More generally, this is a nonnegative class-mapping matrix, but the fraction model is enough to state the idea. U U Realised flow signal. Let sU i (t) = µi (t) + δi (t) denote the realised total removal from queue i at U on tick t (that is, removal that actually occurs on that tick, after any actuation delay is applied). The realised inter-module flow is zU →V,i (t) ≜ rU →V,i sU (47) i (t). N Stacking across classes gives zU →V (t) ∈ R≥0 .

12

Exported envelope. The exported envelope must upper bound what can be sent downstream under the assumptions used for certification. A conservative and easy-to-check choice is z̄U →V,i (t) ≜ rU →V,i s̄U i (t), (48)
U,target U U s̄U (t) ≜ min s (t), q (t) + Ā (t) , i i i i where sU,target (t) is the target removal implied by the applied action on tick t, and q U i (t) is the i U encodes the physical fact that, backlog upper bound used in certification. The cap by q U + Ā i i within one tick, you cannot remove more work than backlog plus arrivals under the declared envelope. Why this form. With (48), zU →V (t) ≤ z̄U →V (t) follows from fixed nonnegative routing U U fractions and the physical bound sU i (t) ≤ q i (t) + Āi (t). Composition therefore relies only on exported envelopes, provided the declared arrival contract is respected.

Figure 2: Fork–join DAG composition, composed envelopes, and contract validity. Top: link utilisation ratios for the fork–join paths, with the tight boundary at utilisation = 1. Middle: inflow to join node B: composed inflow envelope at B ( dashed black) versus realised inflow (median and p10–p90 band), with join breach ticks marked. Bottom: breach and validity rates over time: upstream breach rate (from A or C), join breach rate at B (overall and conditioned on valid ticks), and the valid tick fraction.

13

7.2

Breach detection and semantics

The guarantees in Sections 6 and 7.3 are conditional on the declared arrival envelope. If AM (t) > ĀM (t) + ηA , the operator records a breach, and downstream modules may rely on exported envelopes only on valid ticks. Pessimistic envelopes remain safe but conservative. Optimistic envelopes increase breach and infeasibility rates.

7.3

Compositional guarantees

DAG networks. We use a three-node fork–join DAG example, with nodes A, C, B and edges A → C, A → B, C → B. Node A forks traffic; node B is the join. In topological order A ≺ C ≺ B, envelope propagation is one pass: ¯ C (t) ≥ z̄A→C (t), ¯ B (t) ≥ z̄A→B (t) + z̄C→B (t). in in (49) Theorem 5 (Compositional safety and stability for a DAG). Consider a network of modules connected as a DAG. Suppose each module enforces (i) the safety barrier (12) and (ii) the drift ¯ M . Suppose inflow envelopes trigger (16), both with respect to its total envelope ĀM = āM + in are assigned by (18) using exported outflow envelopes (17) in a topological order. Then: • (Safety) if q M (0) ∈ S M for all modules, then q M (t) ∈ S M for all t. • (Stability) each module satisfies the Foster–Lyapunov drift bound (45) with module-specific constants, hence has a finite long-run average backlog bound as in (46). M and reports σ M (t) = CERTIFIED Operator phrasing. Equivalently, if every module runs CΘ M for all t, then safety and stability follow module-wise, and exported envelopes suffice for composition. Figure 2 instantiates the fork–join DAG in Section 7.3 and visualises the contract semantics behind (18). At the join node B, the composed inflow envelope (dashed black) is formed by summing upstream exported envelopes, and it typically upper-bounds the realised inflow (median with p10–p90 band), even in a near-saturation regime (top panel). We do not treat breaches as harmless noise. Upstream envelope violations reduce the valid-tick fraction, and downstream contracts may be used only on valid ticks. Consistent with this semantics, the breach rate at B, conditioned on valid ticks, is near zero. The remaining breaches occur mainly on ticks already invalidated by upstream breach flags, as shown in the bottom panel. This is the intended fail-loud behaviour: envelope composition supports modular reasoning while its assumptions hold, and withdraws that guarantee when they fail.

Cyclic networks. DAGs avoid circular dependencies in envelope assignment. Cyclic networks require an additional closure condition, since each module’s assumptions may depend on guarantees exported by other modules. ¯ Envelope closure problem. Stack all inflow envelopes in in(t) ∈ Rd≥0 , and all exported outflow envelopes in z̄(t) ∈ Rd≥0 . The interconnection mapping G converts outflow envelopes to inflow envelopes:
¯ in(t) = G z̄(t) , (50) which is typically linear and monotone (routing fractions and class mapping). Each module produces export envelopes as a function of its assumed total envelope, which includes exogenous envelope ā(t) and inflow envelope:
¯ z̄(t) = F ā(t) + in(t) . (51) Closure is the fixed point


¯ ¯ in(t) = Φt in(t) , Φt (x) ≜ G F ā(t) + x . (52)

14

Definition 2 (Monotone Lipschitz envelope maps). A map Ψ : Rd≥0 → Rd≥0 is monotone if x ≤ y implies Ψ(x) ≤ Ψ(y) componentwise. It is Lipschitz with constant L in norm ∥ · ∥ if ∥Ψ(x) − Ψ(y)∥ ≤ L∥x − y∥ for all x, y. Theorem 6 (Cyclic envelope closure under a small-gain condition). Fix time t and suppose: (i) G is monotone and Lipschitz with constant LG , (ii) F is monotone and Lipschitz with constant ¯ ⋆ (t). LF , and (iii) LG LF < 1. Then Φt in (52) is a contraction and has a unique fixed point in Moreover, the iteration
¯ (k+1) (t) ← Φt in ¯ (k) (t) , in k = 0, 1, 2, . . . (53) ⋆ (0) d ¯ (t) from any initial in ¯ (t) ∈ R at a linear rate bounded by LG LF . converges to in ≥0

Operational test. In practice, we use a conservative small-gain diagnostic based on a nonnegative gain matrix upper bound for F combined with routing G. The spectral and norm-based checks, and the cycle-closure phase-transition plot, are in Section 7.4.

7.4

Cyclic closure diagnostics and conservative small-gain tests

¯ = Rz̄ with R ≥ 0 encoding routing fractions and class In many packet models, G is linear: in mapping. If F can be upper bounded by an affine monotone map z̄ ≤ S(ā + x) with S ≥ 0, then Φt (x) ≤ RS(ā + x) and a sufficient small-gain condition is ρ(RS) < 1, (54) where ρ(·) is the spectral radius. A simple instantiation is an affine monotone export rule where each component of z̄ is a nonnegative linear function of the assumed total envelope ā + x: F (ā + x) ≜ S(ā + x), (55) where S ≥ 0 is a gain matrix. In the induced 1-norm, a conservative Lipschitz constant is X LF ≤ ∥S∥1 = max Sij , (56) j

i

The bound is monotone because S is nonnegative. When G(z̄) = Rz̄ with R ≥ 0, we have LG ≤ ∥R∥1 . A sufficient condition for contraction is ∥R∥1 ∥S∥1 < 1. This test is conservative, but computationally inexpensive enough to be verified online. Worked cyclic interpretation. Consider two modules with recirculating traffic. The routing matrix R is obtained from configured traffic fractions, for example the fraction of class i leaving module U and returning to module V . The export-gain matrix S upper-bounds how much a certified outflow envelope can increase when the assumed inflow envelope is enlarged. At a control tick, the operator forms the conservative product RS and checks ρ(RS). If ρ(RS) < 1, the cyclic envelope closure is valid for that tick. If not, the operator can either enlarge envelopes conservatively, mark the closure as invalid, or fall back to a non-compositional local certificate. Figure 3 illustrates the closure test around ρ(RS) = 1. Below the boundary, the fixed-point iteration remains bounded and converges with a small residual. Near and above the boundary, the residual and iteration count increase, and the coupled queue-level view shows the corresponding rise in overload pressure and p99 delay.

15

(a) Closure-only diagnostics versus spectral radius ρ(RS).

(b) Queue-level overload proxy under the same ρ(RS) sweep.

Figure 3: Cycle closure phase transition around the small-gain boundary. We sweep ρ(RS), with the dashed vertical line marking ρ(RS) = 1. (a) Closure-only diagnostics for Algorithm 3: Picard iterate norm ∥x∥2 (and ∥x⋆ ∥2 when defined), iterations-to-stop, and residual ∥x − RS(a + x)∥2 . (b) Coupled queue-level view: growth in the closed-envelope regime aligns with increased overload pressure and sharply increasing p99 delay.

8

Practical integration, adoption, and design trade-offs

This section maps the operator interface onto common packet-system deployments. The operator sits between a proposer and the execution surface. It may run locally at a host, gateway, or switch controller for latency-sensitive loops, or hierarchically, where a central controller proposes actions

16

and each device certifies them against local constraints. In both cases, correctness attaches to the action actually executed at the device. Mapping actions to packet mechanisms. The model action u(t) = (µ(t), δ(t)) is a canonical representation of two families of controls: service allocation and shedding/mitigation. Concrete mappings include: Scheduling and WFQ/DRR weight control. For an egress scheduler with capacity C(t), a common actuation surface is a set of class weights wi (t). Given weights, a conservative per-tick service target can be derived as wi (t) µtar C(t), (57) i (t) = P j wj (t) and certification can be performed directly in (µ, δ) space, then compiled back to weights (Section 8.1). Service floors and caps (14)–(15) map naturally to minimum and maximum weight constraints. Rate limiting and pacing. At hosts and gateways, actuation often takes the form of per-class rate caps or pacing rates. Here µtar i (t) is translated into a rate target over the next interval, and δi (t) corresponds to policing or admission denial. AQM and mitigation knobs. For AQM, the operator can treat δi (t) as a per-tick drop budget (or marking budget) for each class, and can enforce mitigation caps to prevent overreaction under false positives or transient bursts. In all cases, the operator certifies a platform-level target and accounts for platform tracking through the conservative factor in Section 2.1, so that guarantees attach to the realised removal used in the queue update. What must be measured and configured. The operator requires a backlog-related signal, a capacity estimate, an arrival envelope, and action limits. Delayed counters are converted into backlog bounds as in Section 5. The arrival envelope is provided as a policy contract, calibrated from recent history, or set by the hybrid method described earlier. Envelope mismatch is surfaced through breach indicators rather than hidden. Certificate configuration. The certificate configuration Θ specifies backlog caps Qmax , drift thresholds Qhi and margins ε, and any linear constraints such as floors/caps. These are operational policy objects, not proposer internals. Runtime path and overhead. On each tick, the runtime path is: 1. update envelopes Ā(t) and backlog bounds [q(t), q(t)], 2. obtain the proposal ũ(t), 3. compile per-tick constraints from Θ (including delay-consistent constraints when τu > 0), 4. compute the executed action by projection (29) (often via a small QP as in (30)–(33)), 5. export envelope bounds and emit a status flag with diagnostics. The projection problem is small, structured, and admits fast paths in common cases (Section 8.1).

17

Figure 4: Runtime and loop-latency headroom at pinned control interval. Left: Mean certification (operator) step time versus number of queues N , comparing the proposed fast backend against a generic QP baseline. Middle: Per-tick loop breakdown at N = 128 with fast backend and pinned ∆ = 1 ms. Right: Tick utilisation, across control intervals ∆.

Runtime reporting scope. The numbers in Table 3 report the certification step only; proposer execution, telemetry parsing, and platform actuation are excluded from the table. The implementation is the Python certloop package. The fast backend uses a NumPy implementation of projection onto capped simplex constraints with lower bounds, while the generic baseline uses an SLSQP-style constrained optimisation path when the fast structure is not available. The table is averaged over ten seeds in a steady workload at ∆ = 1 ms, with warm-up excluded. The original run metadata did not record CPU model, kernel, or host scheduling state, so these timings should be read as preliminary certification-only timings rather than a full end-to-end systems benchmark. Figure 4 reports pinned-tick microbenchmarks for the certification loop. The left panel reports mean certified-operator step time against the number of queues N . It compares the proposed fast backend with a generic QP baseline. The fast path is lower throughout and scales smoothly in the regime relevant to per-class scheduling. The middle panel decomposes the per-tick loop at N = 128 and ∆ = 1 ms. The right panel reports tick utilisation, with E[step time]/∆ summarised in Table 3. These results support the narrower claim that the certification computation itself is small enough for millisecond-scale control intervals under the measured Python backend.

8.1

Adoptability notes and fast certification paths

The generic operator solves the convex projection (29). In the default case, which is also the one most likely to appear in practice, this projection has a closed-form structure. P Consider a single bottleneck with constraints µi ≥ 0 and i µi ≤ C, together with per-class lower bounds on total removal si = µi + δi ≥ ℓi . When shedding is allowed but penalised, the operator usually sets δ = 0 whenever this is feasible. The executed service then reduces to µ = Π∆(C) (µ̃) subject to µi ≥ ℓi , (58) where Π∆(C) denotes projection onto the capped simplex. This can be implemented in O(N log N ) time by sorting. The QP backend is needed only when extra constraints, such as caps, floors, or multi-resource coupling, remove this simple structure. To reduce tuning burden, we recommend three presets for (Qmax , Qhi , ε): latency-biased, throughput-biased, and default. A simple calibration links backlog caps to delay targets through Qmax ≈ Cdmax , using consistent units. Then Qhi is set as a fraction of Qmax , while ε controls recovery speed after bursts.

18

Table 3: Per-tick certified-operator runtime at ∆ = 1 ms. The table reports certification time only; proposer computation is excluded.

8.2

N

mean tcert (µs)

p95 tcert (µs)

mean/∆ (%)

64 128 512

38.5 37.2 335.0

52.0 50.0 511.5

3.8 3.7 33.5

Positioning and design trade-offs

The certified operator creates an explicit execution boundary. The cost is conservatism when envelopes are loose, state bounds are delayed, or κmin is small. With well-calibrated envelopes, the operator can be less wasteful than static provisioning because it reacts to the certified state. With stale telemetry or pessimistic contracts, it has less room to preserve the proposer’s preferred action. This is the desired behaviour: weaker evidence should produce more cautious execution. Cost of certification.

Figure 5: Price of certification. Top: per-tick projection distance ∥u(t) − ũ(t)∥2 . Bottom: fraction of ticks with certified correction and emergency-mode execution. Figure 5 reports the projection distance ∥u(t) − ũ(t)∥2 , separating feasible correction from emergency mode. Under light load, corrections remain small for well-behaved proposers. Under bursty stress, corrections grow as barrier and drift constraints become active. The emergency fraction identifies ticks where the declared envelopes and available capacity make certification infeasible.

9

Experiments

The experiments examine safety under stress, correction under weak proposers, composition across modules, and the effect of cyclic closure on feasibility and conservatism. We compare four controllers: 1. Proposer only: execute ũ directly. 2. Monitor only: execute ũ and raise alarms when constraints are violated. 3. Naive clipping: clip weights, floors, or caps using a heuristic rule, without solving the projection. 19

Table 4: Execution-audit fields used in experiments. Trace field

Meaning in the implementation

µ̃(t), δ̃(t)

proposer output before certification

µ(t), δ(t) sreal (t)

σ(t), ξ(t)

b(t)

Role in the paper claim

shows the action that would have reached the dataplane without the operator certified action returned object to which safety, drift, by the operator and contract claims attach realised byte removal in checks that the simulator exthe Python queue update ecutes the logged action subject to available backlog and arrivals status flag and slack vec- separates certified ticks from tor infeasible ticks and quantifies violation under overload envelope-breach indicator marks ticks where the declared contract is not valid for composition

Limitation not a safe action by itself still a target for a real scheduler no Linux packetisation or NIC batching guarantees are not claimed when slack is positive does not identify the external cause of breach

4. Certified operator (ours): execute the output of CΘ and record the resulting status flags. The proposer may be backlog-proportional, random, or learned. The safety guarantees apply only on ticks where the certified operator reports CERTIFIED. Python execution audit and scope of the backend. The present evaluation is deliberately Python based. The simulator is a byte-level closed-loop backend: the proposer emits µ̃, the certified operator emits µ, actuation delay is represented by a FIFO action buffer, and the realised removal is computed as the physical service that can be taken from backlog plus arrivals on that tick. Thus the experiments audit the execution boundary and the status semantics of the certified operator. They do not claim to measure the short-window tracking loss of Linux tc, or kernel packet scheduling. That loss is the role of the calibrated κmin parameter in Section 2.1. The conservative reading is therefore: the experiments test whether the certified operator enforces the compiled constraints before execution, whether breaches and infeasibility are surfaced, and whether the closed loop remains well defined under delayed telemetry and actuation. Thus, the present evaluation validates the certified execution boundary in a byte-level closed-loop backend. Stress traces under delayed telemetry and actuation. Figure 6 evaluates delayed telemetry and actuation. Direct execution and naive clipping react late, producing earlier and more persistent threshold excursions. The certified operator reduces violations while constraints remain feasible by compiling barrier and drift constraints over the available state and envelope bounds. The status panel separates certified ticks from infeasible ticks, so overload is reported rather than hidden.

20

Figure 6: Killer stress traces under telemetry and actuation delay.

Figure 7: Certified-operator value across proposer qualities, reported as mean ± standard deviation over seeds. Direct execution of proposals is compared with execution through the certified operator for three proposers: backlog-proportional, random, and adversarial starvation. Top row: worst-queue delay tails, p99 and p99.9, in seconds on a log scale. Bottomleft: mean throughput in MB/s. Bottom-right: fraction of ticks on which the wrapped operator reports CERTIFIED.

21

Certified-operator value across proposer qualities. Figure 7 measures the effect of placing the certified operator between a fixed proposer and the dataplane. For benign proposers, namely backlog-proportional and random, wrapping has little effect on tail delay or throughput. This is the expected result: their actions already lie close to the certified feasible set, so the operator mostly passes them through. For the adversarial starvation proposer, direct execution produces much larger worst-queue delay tails and a sharp loss of delivered throughput. Executing the certified output instead reduces p99 and p99.9 delay and restores throughput, since the executed action must satisfy the barrier and drift-derived lower bounds whenever these constraints are feasible. The CERTIFIED fraction in the bottom-right panel gives the relevant semantics. Guarantees apply only on feasible certified ticks, and the operator reports the remaining cases instead of preserving a fiction of correctness. Across identical seeds, the certified operator consistently reduces delay tails and restores throughput under adversarial starvation, while staying nearly neutral under benign proposers, as shown in Appendix A.2, Figure 11.

Figure 8: Priority inversion under a poor proposer, and the effect of explicit floors and caps. Tail delay for the latency class, c0, is shown at the top. Tail delay for the bulk class, c1, is shown at the bottom. Both are reported at p99 and p99.9 on a log scale. Why floors and caps are first-class certificate constraints. Figure 8 shows a common deployment failure under a poor proposer: priority inversion. When proposals are executed directly, the latency class c0 suffers much worse tail delay, while the bulk class c1 appears artificially healthy. This is not a fine point of tuning. It follows from leaving protection semantics buried inside proposer logic. Explicit linear constraints, such as a per-tick service floor for protected classes (14) and optional caps for flagged classes (15), prevent the inversion by reserving a minimum share of capacity for c0. The certified operator enforces these constraints online, so the protection guarantee attaches to the executed action, not to the proposer’s good intentions. Good intentions, in schedulers as elsewhere, are a poor substitute for a constraint.

22

Figure 9: Envelope mismatch sweep: breach visibility and status semantics. Top: breach rate, defined as the fraction of ticks with b(t) = 1 in (24), and certified-tick fraction. Middle: worst-queue delay p99 over all ticks, with delay budget Qmax . Bottom: delivered rate normalised by capacity. Envelope mismatch is surfaced. Figure 9 sweeps the envelope mismatch parameter δ. When δ ≤ 0, the declared envelope is pessimistic or correct. It becomes optimistic for δ > 0. For pessimistic or correct envelopes, breach is rare and most certified ticks are contract-valid. As the envelope becomes optimistic, the breach rate rises and the valid CERTIFIED fraction falls, because the contract assumption needed for safety and drift guarantees no longer holds. Some ticks may still satisfy the compiled constraints under the declared envelope, but they are not contract-valid and cannot support downstream composition. The middle panel shows the resulting delay growth.

23

Figure 10: Overload transition with emergency fallback. Offered load is swept as a utilisation factor. The panels report emergency-mode fraction, totalbacklog p99, and delivered rate. Overload and emergency semantics. Infeasibility can occur even when envelopes are valid, for example when offered load exceeds capacity or configured caps are too tight. In this regime, the operator remains defined. It reports INFEASIBLE and returns a best-effort action with quantified slack, rather than silently violating the compiled constraints. Figure 10 shows the transition as offered load increases. Emergency-mode ticks rise sharply beyond the stability boundary, total-backlog p99 grows, and delivered rate saturates near capacity. This is the expected signature of overload, not a proposer artefact.

10

Conclusion

The central claim of this paper is that packet-network control should be certified at the point of execution. A proposer may be learned, heuristic, adversarial, or agentic, but the dataplane should act only on the certified operator’s output. On CERTIFIED ticks, the guarantees attach to the executed action, the valid arrival envelope, the valid state bound, the service-tracking assumption, and the exported contract. When these conditions do not hold, the operator records the reason through breach, missing-information, infeasibility, and slack signals. An unsafe proposal should not become a safe action merely because the proposer was well designed. The resulting framework brings backlog caps, service floors, mitigation caps, drift constraints, and envelope contracts into one per-tick certification interface. It also gives a compositional account: feed-forward networks compose through exported envelopes, while cyclic networks require a closure test under a small-gain condition. The evaluation supports this execution boundary under weak proposers, delayed telemetry, delayed actuation, envelope mismatch, overload, and millisecond-scale certification. These results should be read within that scope. They validate the certified operator in a byte-level closed-loop backend, while deployment-level scheduler tracking remains a separate systems question. The framework also opens several natural directions for further work. One useful next direction is to instantiate the service-tracking factor on real dataplanes, including Linux HTB, 24

DRR, programmable switches, and hardware queues. This would turn κmin from a conservative platform parameter into a measured quantity for specific scheduler regimes. Another direction is to strengthen the certification path itself, from configuration to constraint compilation and solver output, through systematic testing, translation validation, or verified compilation. Ethical considerations The study involved no human participants and used no sensitive or personally identifiable user data. No material ethical issues are therefore anticipated.

Declaration of generative AI and AI-assisted technologies in the manuscript preparation process During the preparation of this work the author(s) used AI-assisted tools for language editing and structural refinement. After using this tool/service, the author(s) reviewed and edited the content as needed and take(s) full responsibility for the content of the published article.

References [1] Mohammad Alizadeh, Albert Greenberg, David A. Maltz, Jitendra Padhye, Parveen Patel, Balaji Prabhakar, Sudipta Sengupta, and Murari Sridharan. Data center tcp (dctcp). In Proceedings of the ACM SIGCOMM 2010 Conference, SIGCOMM ’10, page 63–74, New York, NY, USA, 2010. Association for Computing Machinery. [2] Aaron D. Ames, Samuel Coogan, Magnus Egerstedt, Gennaro Notomista, Koushil Sreenath, and Paulo Tabuada. Control barrier functions: Theory and applications. In 2019 18th European Control Conference (ECC), pages 3420–3431, 2019. [3] Aaron D. Ames, Xiangru Xu, Jessy W. Grizzle, and Paulo Tabuada. Control barrier function based quadratic programs for safety critical systems. IEEE Transactions on Automatic Control, 62(8):3861–3876, 2017. [4] Ran Ben Basat, Sivaramakrishnan Ramanathan, Yuliang Li, Gianni Antichi, Minian Yu, and Michael Mitzenmacher. Pint: Probabilistic in-band network telemetry. In Proceedings of the Annual Conference of the ACM Special Interest Group on Data Communication on the Applications, Technologies, Architectures, and Protocols for Computer Communication, SIGCOMM ’20, page 662–680, New York, NY, USA, 2020. Association for Computing Machinery. [5] Muhammad Bilal, Jon Crowcroft, Ruizhi Wang, Xiaolong Xu, and Schahram Dustdar. Large language models for agentic netops and aiops: Architectures, evaluation, and safety. arXiv preprint arXiv:2605.12729, 2026. [6] Muhammad Bilal, Omer Tariq, and Hasan Ahmed. Nos-gate: Queue-aware streaming ids for consumer gateways under timing-controlled evasion. IEEE Transactions on Consumer Electronics, pages 1–1, 2026. [7] Muhammad Bilal and Xiaolong Xu. Network-optimised spiking neural network (nos) scheduling for 6g o-ran: Spectral margin and delay-tail control. arXiv preprint arXiv:2510.11291, 2025. [8] Allan Borodin, Jon Kleinberg, Prabhakar Raghavan, Madhu Sudan, and David P. Williamson. Adversarial queuing theory. J. ACM, 48(1):13–38, January 2001. [9] Jean-Yves Le Boudec and Patrick Thiran. Network Calculus: A Theory of Deterministic Queuing Systems for the Internet, volume 2050 of Lecture Notes in Computer Science. Springer, 2001. 25

[10] R.L. Cruz. A calculus for network delay. i. network elements in isolation. IEEE Transactions on Information Theory, 37(1):114–131, 1991. [11] R.L. Cruz. A calculus for network delay. ii. network analysis. IEEE Transactions on Information Theory, 37(1):132–141, 1991. [12] A. Demers, S. Keshav, and S. Shenker. Analysis and simulation of a fair queueing algorithm. In Symposium Proceedings on Communications Architectures &amp; Protocols, SIGCOMM ’89, page 1–12, New York, NY, USA, 1989. Association for Computing Machinery. [13] Salma Emara, Baochun Li, and Yanjiao Chen. Eagle: Refining congestion control by learning from the experts. In IEEE INFOCOM 2020 - IEEE Conference on Computer Communications, pages 676–685, 2020. [14] S. Floyd and V. Jacobson. Random early detection gateways for congestion avoidance. IEEE/ACM Transactions on Networking, 1(4):397–413, 1993. [15] Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. Comprehensive formal verification of an os microkernel. ACM Trans. Comput. Syst., 32(1), February 2014. [16] Yuliang Li, Rui Miao, Hongqiang Harry Liu, Yan Zhuang, Fei Feng, Lingbo Tang, Zheng Cao, Ming Zhang, Frank Kelly, Mohammad Alizadeh, and Minlan Yu. Hpcc: high precision congestion control. In Proceedings of the ACM Special Interest Group on Data Communication, SIGCOMM ’19, page 44–58, New York, NY, USA, 2019. Association for Computing Machinery. [17] Michael J. Neely. Stochastic Network Optimization with Application to Communication and Queueing Systems. Synthesis Lectures on Learning, Networks, and Algorithms. Springer Cham, 2010. [18] A.K. Parekh and R.G. Gallager. A generalized processor sharing approach to flow control in integrated services networks: the single-node case. IEEE/ACM Transactions on Networking, 1(3):344–357, 1993. [19] A.K. Parekh and R.G. Gallager. A generalized processor sharing approach to flow control in integrated services networks: the multiple node case. IEEE/ACM Transactions on Networking, 2(2):137–150, 1994. [20] Jonathan Perry, Amy Ousterhout, Hari Balakrishnan, Devavrat Shah, and Hans Fugal. Fastpass: a centralized "zero-queue" datacenter network. SIGCOMM Comput. Commun. Rev., 44(4):307–318, August 2014. [21] Thomas Arthur Leck Sewell, Magnus O. Myreen, and Gerwin Klein. Translation validation for a verified os kernel. SIGPLAN Not., 48(6):471–482, June 2013. [22] M. Shreedhar and George Varghese. Efficient fair queueing using deficit round robin. SIGCOMM Comput. Commun. Rev., 25(4):231–242, October 1995. [23] Vishal Shrivastav. Stateful multi-pipelined programmable switches. In Proceedings of the ACM SIGCOMM 2022 Conference, SIGCOMM ’22, page 663–676, New York, NY, USA, 2022. Association for Computing Machinery. [24] L. Tassiulas and A. Ephremides. Stability properties of constrained queueing systems and scheduling policies for maximum throughput in multihop radio networks. IEEE Transactions on Automatic Control, 37(12):1936–1948, 1992. 26

[25] Kim Peter Wabersich and Melanie N. Zeilinger. A predictive safety filter for learning-based control of constrained nonlinear dynamical systems. Automatica, 129:109597, 2021. [26] Keith Winstein and Hari Balakrishnan. Tcp ex machina: Computer-generated congestion control. In Proceedings of the ACM SIGCOMM 2013 Conference on SIGCOMM, SIGCOMM ’13, pages 123–134, New York, NY, USA, 2013. Association for Computing Machinery. [27] Zhengxu Xia, Yajie Zhou, Francis Y. Yan, and Junchen Jiang. Genet: automatic curriculum generation for learning adaptation in networking. In Proceedings of the ACM SIGCOMM 2022 Conference, SIGCOMM ’22, page 397–413, New York, NY, USA, 2022. Association for Computing Machinery. [28] Lei Zhang, Yong Cui, Mowei Wang, Kewei Zhu, Yibo Zhu, and Yong Jiang. Deepcc: Bridging the gap between congestion control and applications via multiobjective optimization. IEEEACM Transactions on Networking, 30(5):2274–2288, 2022. [29] Hao Zheng, Chengyuan Huang, Xiangyu Han, Jiaqi Zheng, Xiaoliang Wang, Chen Tian, Wanchun Dou, and Guihai Chen. µmon: Empowering microsecond-level network monitoring with wavelets. In Proceedings of the ACM SIGCOMM 2024 Conference, ACM SIGCOMM ’24, pages 274–290, New York, NY, USA, 2024. Association for Computing Machinery.

A

Appendices

A.1

Algorithms

This appendix gives the auxiliary procedures used by the main text. Algorithm 2 gives the executable form of DAG envelope propagation used in Theorem 5: upstream modules export bounds, and downstream modules aggregate them in topological order. Algorithm 3 gives the cyclic counterpart, where the inflow envelope is found by fixed-point iteration and is valid only when the small-gain test succeeds. Algorithm 4 summarises the stress harness used in Section 9, including delayed telemetry, delayed actuation, timing-shaped arrivals, breach indicators, and status traces. Algorithm 2 Envelope propagation in a DAG, one forward pass Require: DAG modules in topological order M1 ≺ M2 ≺ · · · ≺ ML , exogenous envelopes āMℓ (t) ¯ Mℓ (t) ← 0 for all ℓ 1: Set in 2: for ℓ = 1 to L do 3: Run the module step, Algorithm 1, to obtain exported envelopes z̄Mℓ →V (t) 4: for all outgoing neighbours V of Mℓ do ¯ V (t) ← in ¯ V (t) + z̄M →V (t) 5: in ℓ 6: end for 7: end for

A.2

Supportive Results

27

Algorithm 3 Cyclic envelope closure by fixed-point iteration Require: Exogenous envelope ā(t), maps F and G, tolerance η > 0, maximum iterations Kmax ¯ (0) (t) ← 0 1: Initialise in 2: for k = 0 to Kmax − 1 do ¯ (k) (t)) 3: z̄ (k) (t) ← F (ā(t) + in (k+1) ¯ 4: in (t) ← G(z̄ (k) (t)) (k+1) ¯ ¯ (k) (t)∥ ≤ η then 5: if ∥in (t) − in 6: break 7: end if 8: end for ¯ ¯ (k+1) (t) (closed envelopes) 9: Output: in(t) ← in

Algorithm 4 Stress harness for delayed telemetry, delayed actuation, and timing-shaped arrivals Require: Envelope sequence Ā(t), telemetry delay τy , actuation delay τu , capacity C(t), horizon T 1: Initialise queues q(0) and an action buffer of length τu 2: for t = 0 to T − 1 do 3: arrivals A(t) within or beyond Ā(t) 4: Form telemetry y(t) = Hq(t − τy ) + ν(t) 5: Proposer outputs ũ(t) from y(≤ t) 6: Operator sets (u(t), σ(t)) ← CΘ (ũ(t), y(t)), while baselines set u(t) ← ũ(t) 7: Apply delayed action uapplied (t) = u(t − τu ) 8: Update queues and log violations, breach flags, status flags, and runtime 9: end for

Figure 11: Certified-operator value per seed, paired with and without certification. Each proposer is evaluated on the same seeds in wrapped and unwrapped modes, with lines connecting paired runs. The paired view shows that improvements under the adversarial proposer are consistent across seeds for both delay tails and throughput. It also shows that the wrapped mode’s CERTIFIED fraction remains below one in this regime.

28

Seed-paired evidence for wrapper value. Figure 11 provides a seed-paired robustness check. Certified and direct-execution runs use identical random seeds. For backlog-proportional and random proposers, the paired points nearly coincide, indicating that certification is mostly non-invasive when proposals are already well behaved. Under the adversarial starvation proposer, certification reduces delay tails and restores throughput. Non-certified ticks in these runs are mainly INFEASIBLE ticks caused by tight compiled lower bounds under stress. Envelope breaches are analysed separately in the envelope-mismatch experiment.

29