Source-linked AI summary
Robustness-Aware Evaluation and Enhancement of Mutation-Based Fuzzing for Bug Discovery
Zirui Liu, Mengfan Xu, Juan Zhai, Shiqing Ma, Barry Nelson
TL;DR
Fuzzing’s stochasticity makes it difficult to know which results to trust and how many trials are enough. The paper models fuzzing and introduces bug-triggered splitting; on Magma, splitting achieves a higher real-bug rate in 38 of 40 fuzzer-program pairs at matched CPU.
Problem
Fuzzing’s stochasticity creates substantial variation across campaigns, leaving practitioners to run many expensive trials for sound conclusions.
Source: §1 · p. 1Method
Results
38 of 40 fuzzer-program pairs on Magma had a higher real-bug rate with splitting at matched CPU; the median increase was +52%.
Source: §1.1 · p. 2Takeaways & Limitations
Splitting guarantees no fewer raw bug events than an embedded continuation path for any realized split tree.
Source: §1.1 · p. 2LLM-based fuzzers whose mutation distributions change unpredictably over time fall outside the paper’s current scope.
Source: §3.1 · p. 3
Abstract
from arXiv · showhide
Mutation-based fuzzing is widely used to discover software vulnerabilities, but its randomness complicates rigorous evaluation and reliable bug detection. Prior work measures this variability empirically but lacks a theory with computable convergence and sample-complexity guarantees. We address both problems. First, we estimate robustness from independent campaigns by measuring variation in bug-trigger rates after accounting for compute. For $M$ campaigns of length $T$, finite-trial error decreases at the standard $M^{-1/2}$ rate, while finite-length error is bounded when temporal bug correlations decay. We then introduce splitting, a black-box wrapper that copies a fuzzer's queue state after a bug trigger and continues from that state in multiple branches, directing more effort toward the discovered region. For any realized split tree, branching cannot reduce the raw number of bug-triggering events relative to a single continuation path. Expected detection also improves when states receiving more branches tend to yield more bugs later. In a simplified model, splitting reduces variance per unit compute when $p<\sqrt{2}-1$, where $p$ is the fraction of time spent in the bug region. At matched compute, splitting finds more real bugs per CPU-hour than the baseline in 38 of 40 Magma ground-truth cells (median +52\%; 34 of 38 individually significant) and never finds fewer distinct bugs. It changes CVE-2019-19926 from undetected (0/20 trials) to reliably detected (20/20; Fisher $p<10^{-4}$), with six additional detection improvements, five involving CVEs. On FuzzBench, splitting finds more unique bugs in 53 of 70 pairs and reduces cross-campaign variation in 66 of 70, with a median reduction of about $10\times$. Every branch counts toward the compute budget. With about 0.14\% overhead, splitting provides a practical way to measure and improve fuzzers.
1 Introduction
Fuzzing’s stochastic outcomes make it difficult to know which results to trust, while existing evaluation lacks a principled, bug-centric measure of robustness. The paper develops a theoretically grounded robustness metric and introduces splitting to measure and enhance fuzzers.
1 Introduction
- Fuzzing’s campaign-to-campaign variability complicates trustworthy evaluation, and existing metrics do not guarantee capture of the process’s true stochastic variation.The variability also reflects movement between input regions; clustered bugs make time spent in bug-rich regions consequential for bug finding.Source: §1 · p. 1
1.1 Main Contributions
- Robustness is effort-normalized variance in bug-detection rate, estimated from independent campaigns with M^-1/2 finite-trial error and bounded finite-length error under geometric decay.An initialization correction in the two-state approximation is up to 46× tighter than the worst-case bound.Source: §1.1 · p. 2
- Splitting forks a trajectory when it discovers a bug; for any realized split tree, its raw bug-event count is no lower than an embedded continuation path.Expected bug-detection rate increases when states receiving more branches also tend to yield more future bugs.Source: §1.1 · p. 2
- At matched compute, splitting finds more unique bugs than independent replication in 53 of 70 FuzzBench pairs and reduces variance per unit compute in an idealized model when p < √2−1.It allocates effort after a bug is observed and starts from the discovered state.Source: §1.1 · p. 2
- 38 of 40 Magma pairs show higher real-bug rates at matched CPU (median +52%), while FuzzBench finds more unique bugs in 53 of 70 matched-CPU pairs.Splitting never finds fewer distinct bugs on Magma; it also changes AFL++ detection of CVE-2019-19926 from 0/20 to 20/20 trials.Source: §1.1 · p. 2
- FuzzBench cross-campaign variance falls in 66 of 70 pairs, with a median reduction of approximately 10×.The black-box wrapper has approximately 0.14% overhead and supports online or offline deployment.Source: §1.1 · p. 2
2 Related Work
Prior evaluation work leaves open how to quantify robustness around bug detection with theoretical guarantees. This paper adapts Markov-chain tools to fuzzing and introduces bug-signal-guided splitting as a black-box enhancement.
2 Related Work
- Prior fuzzer-evaluation studies report randomness and limitations of coverage or bug-count metrics, but lack a theoretically grounded criterion for trial selection and robustness.Existing robustness assessments use indirect coverage proxies or across-trial summaries without a theoretically backed variance dimension.Source: §2 · p. 2
- The framework models mutation over the input space, treating coverage and bug-triggering as output functions rather than modeling coverage states.This avoids relying on coverage transitions that depend on a growing corpus and need not be Markovian.Source: §2 · p. 3
- The paper adapts MCMC variance-estimation and chain-diagnostic machinery to the mutation process and bug-detection rate, adding convergence guarantees and splitting.Prior benchmarking work documented variation with trial count, duration, and benchmark selection.Source: §2 · p. 3
- Unlike rare-event splitting with hand-tuned importance functions, the fuzzing method uses bug signals and forks the full queue state, with a non-regression guarantee for realized split trees.This distinguishes it from restart-from-crash and corpus-synchronizing parallel fuzzing.Source: §2 · p. 3
3 Problem Formulation
The formulation treats mutation as a Markov chain over inputs and bug triggering as an output of that chain. It defines bug-detection rate and effort-normalized variance as linked measures of effectiveness and robustness.
3 Problem Formulation
- The fuzzer’s input sequence is modeled as a Markov chain over the finite input domain, with bug-triggering determined by a behavioral output function.The input string supplies the randomness; the output process need not itself be Markov.Source: §3 · p. 3
- The model uses a stationary-induced two-state surrogate for bug/no-bug outputs; geometric output autocorrelation decay is observed in every evaluated cell.The output process is not generally Markov, and output Markovianity is not required.Source: §3 · p. 3, §3.1 · p. 3
3.1 Modeling
- Mutation operators such as bit flips, splicing, dictionary insertion, and havoc are represented as input-chain transitions with a fixed-in-code distribution.For stateful fuzzers, the state can be expanded to include internal state when needed.Source: §3.1 · p. 3, §3 · p. 3
- The model assumes time-homogeneous, geometrically ergodic input chains; mutation distributions that shift over a campaign can instead be handled by windowed estimation over approximately stationary segments.Unpredictably changing LLM-based mutation distributions are outside the current scope.Source: §3.1 · p. 3
- Bug-detection rate characterizes the fraction of executed inputs that trigger bugs, while its underlying event count is random across campaigns.The study focuses theoretically on bug-trigger events, the process underlying unique-bug discoveries.Source: §3.1 · p. 4
- Robustness measures variability in campaign outcomes while charging the computational effort required to attain that variability level.The formulation considers both terminating and non-terminating regimes.Source: §3.1 · p. 4
- Bug-trigger rates and unique-bug counts are closely connected empirically, but unique-bug discovery also deduplicates against the previously discovered set.Splitting increases trigger events in 39 of 40 Magma cells and yields at least as many distinct real bugs in all 40.Source: §3.1 · p. 4
4 Evaluation Framework
The evaluation framework runs independent real-fuzzer campaigns and derives bug-detection and robustness estimates from their trajectories. Its estimators distinguish campaign variability from uncertainty in the estimated mean and account for computational effort.
4 Evaluation Framework
- The Monte Carlo evaluation runs M independent fuzzer campaigns of T mutation steps each, producing independent sample trajectories from real executions.The framework uses real fuzzers on real programs rather than a synthetic simulator.Source: §4 · p. 4
- The classical simulation procedure supplies M trajectories; the contribution is estimators that quantify robustness and guide the joint choice of M and T.Figure 1 summarizes the evaluation and enhancement framework.Source: §4 · p. 4, Figure 1 · p. 4
- The mean campaign rate estimates bug-detection rate, while sample variance across campaigns measures how much root campaigns differ.Campaign-outcome variance and uncertainty in the grand mean are distinct quantities.Source: §4 · pp. 4–5
- Robustness is estimated as campaign sample variance scaled by T, making effort-normalized variability directly computable from simulation outputs.The framework separately evaluates how closely computable variance tracks the quantity it estimates.Source: §4 · p. 5
- Estimator accuracy separates finite-M estimation error from bias caused by finite campaign duration.Bug-detection ability is also evaluated through the estimated rate, equivalently the total bug count across independent trials.Source: §4 · p. 5
5 Theoretical Guarantees for Evaluation
The paper gives computable guarantees for estimating effort-normalized fuzzing robustness, separating finite-campaign sampling error from initialization and finite-horizon effects. It also provides a rule for choosing campaign length and trial count, with scope tied to geometric forgetting by the input chain.
5 Theoretical Guarantees for Evaluation
- Theorem 6 decomposes robustness-estimation error into O(M^-1/2) sampling error, initialization error, and finite-horizon autocovariance bias.The finite-horizon bound requires geometrically decaying autocovariances of the binary output process, not that the bug indicator itself be Markov.Source: §5 · p. 5
- The two-state specialization makes the initialization term up to 46× tighter than the worst-case bound and at least 1.8× tighter in every cell.For example, the bound for Honggfuzz on openssl tightens from 17.3 to 0.37.Source: §5 · p. 5
- On the evaluated suites, the sample-size rule stabilizes near M = 20 campaigns of T = 12 h.Choose T so the horizon-dependent margin is below the target ε, then choose the smallest M that meets the remaining margin.Source: §5 · p. 5
- The guarantee requires the input chain to forget its starting point geometrically, but does not require the binary bug indicator itself to be Markov.Under behavioral drift, the reported diagnostics describe locally consistent campaign phases.Source: §5 · p. 5
6 Enhancement of Fuzzing
Splitting reallocates fuzzing effort from a bug-triggering state, using a black-box wrapper that leaves fuzzer internals unchanged. The paper compares it with power scheduling and independent replication, and describes its branching and deployment procedure.
6 Enhancement of Fuzzing
- Splitting is a black-box plug-in that uses bug signals to direct additional effort from the discovered state, without a handcrafted importance function or changes to fuzzer internals.The proposed method forks a trajectory into descendant runs initialized at the current input with independently sampled randomness.Source: §6 · p. 5, §6.2 · p. 6
6.1 Relationship to Power Scheduling
- At equal compute, splitting-wrapped AFL has higher terminal BDR than AFLFast and MOpt on all ten benchmarks, with median gains of 25% and 22%, respectively.Both comparisons have Wilcoxon p = 0.002; the method also improves AFL++, whose power schedule it composes with, by up to 125%.Source: §6.1 · p. 6
- Unlike independent replication, splitting waits for a bug and branches from the queue state where it occurred rather than exploring uniformly.The parent stops when it splits; descendants continue independently from copies of the current queue state.Source: §6.1 · p. 6, §6.2 · p. 6
6.2 Methodology based on Splitting
- Across 187 full-length online trials, stop, copy, and relaunch overhead has a median of 0.14% of wall time.A cap of three split depths and two branches bounds trials to eight concurrent leaves, each charged for its CPU-hours.Source: §6.1 · p. 6
19 Output: ET, NT and {kt}T
The analysis gives conditions for variance reduction and bug-rate gains under splitting, while distinguishing theoretical guarantees for fixed trees from the adaptive schedule used in experiments. It also identifies a trade-off between detection gains and variance reduction.
19 Output: ET, NT and {kt}T
- The CPU accounting charges every active leaf for the compute it consumes, and each arm is charged its actual compute.The splitting rate weights active paths equally, while the raw event count records all bug-triggering events.Source: §19 · p. 6, §6.3.2 · p. 7
6.3.1 Variance Comparison
- In the idealized two-state model, splitting reduces variance per unit CPU when p < √2 − 1 ≈ 0.414, where p is the fraction of time in the bug region.The ratio bound requires positivity; the checkable condition holds in 102 of 110 evaluated cells and all 40 Magma cells.Source: §6.3.1 · p. 7
(Proof in Appendix F.2.)
- For the deployed adaptive schedule, CPU-weighted variance is lower in 66 of 70 matched-CPU pairs, with a median split-to-baseline ratio of 0.098.The fixed-tree bound does not cover the additional variance term from choosing forks based on observed bugs; the experiments measure the net effect.Source: (Proof in Appendix F.2.) · p. 7
6.3.2 Bug Detection Rate Comparison
- For any realized split tree, the raw bug-event count never falls below that of one designated continuation path; comparison with a separate equal-CPU Monte Carlo arm is empirical.The equally weighted rate improves only under the condition stated by the theorem.Source: (Proof in Appendix F.3.) · pp. 7–8
(Proof in Appendix F.3.)
- Expected bug-detection rate strictly increases when the covariance between how often states split and their future bug yield is positive.In the multistage schedule, both branching and future yield can rise with observed bug activity when bugs cluster.Source: (Proof in Appendix F.3.) · p. 8
6.3.3 Discussions
- When the event surplus is small, splitting improves detection and variance together; when it is large, it trades variance for a larger detection gain.The discussion bounds the BDR increment by 1/(2T) times the difference in bug-event counts.Source: §6.3.3 · p. 8
7 Numerical Experiments
The numerical experiments evaluate splitting for bug discovery and campaign variance at matched compute across FuzzBench and Magma, alongside comparisons with related approaches and model diagnostics. They also describe offline scheduling, practical guidance, research context, and released artifacts.
7.3.3 Comparisons
- At matched CPU, splitting beats the independent-instance baseline on raw unique bugs in 53 of 70 FuzzBench pairs and lowers terminal variance in 66 of 70.For CPU-weighted variance, the terminal reduction among winning pairs has a median of 3.4× and reaches 243×; the terminal 1/kt-weighted unique-bug rate is strictly greater in all 70 pairs.Source: §7.1 · p. 8, §7.3.3 · pp. 9–10, Figure 4 · p. 11
7.3.1 Monte Carlo Simulation
- Monte Carlo variance is heterogeneous across fuzzer–benchmark pairs, while splitting contracts variance earlier on some targets and can raise it where bug discovery expands substantially.Baseline variance decreases on LIBHEVC, LIBHTP, and STB but is flat-to-rising on PHP and POPPLER; on LIBFUZZER/GROK and LIBFUZZER/PHP, splitting’s variance rise accompanies rate gains up to +800%.Source: §7.3.1 · p. 9, Figure 2 · p. 9, §7.3.2 · p. 9
7.4 Ablation Study
- The online, history-free splitting variant reduces normalized variance and improves terminal rate in all 12 settings, while offline guidance lowers window-averaged variance in 11 of 12.The ablation compares three fuzzers across four benchmarks; both variants share fork-on-bug and differ only in the signal selecting split times.Source: §7.4 · p. 10
7.5 Ground-Truth Validation with Magma
- Splitting converts sqlite3 AFL++ detection of CVE-2019-19926 from 0/20 baseline trials to 20/20, and adds detections of five other CVEs across poppler, openssl, and libtiff.The CVE-2019-19926 conversion has one-sided Fisher p < 10−4; the other listed conversions are individually Fisher-significant at M=20.Source: §7.5 · pp. 10–11
7.6 Comparison with corpus-synchronizing parallel fuzzing
- Against an eight-worker corpus-synchronizing pool, splitting achieves a higher bug-event rate on every program by 1.41–2.82× (median 1.90×) and leads on distinct bugs per CPU-hour on five of eight.The pool gains little from doubling workers from four to eight, while splitting wraps mutation-based fuzzers without requiring synchronization support.Source: §7.6 · pp. 11–12
7.7 Model Diagnostics for the Assumptions
- Across 110 cells, autocorrelation decays geometrically toward the noise floor with a positive gap, while the surrogate’s λ̂2 is nonnegative in 102 cells.Phase-specific estimates show γ̂ shifts of 0.08–0.86 between early and late halves, while adaptive-scheduler pairs remain more homogeneous; the geometric decay holds within each phase.Source: §7.7 · pp. 12–13, Figure 7 · p. 13
7.5 Ground-Truth Validation with Magma
- Splitting finds more real bugs per CPU-hour in 38 of 40 Magma cells (median +52%; 34/38 significant) and never lowers raw distinct-bug counts.Across 40 fuzzer–program pairs, splitting ties or improves unique-bug counts; Table 3 summarizes the ground-truth comparison.Source: §7.5 · p. 10, Table 3 · p. 12
8 Implications for Fuzzing Practice
- On the evaluated suites, about two-thirds of pairwise robustness rankings separate around M=20 trials and T=12 h, and practice should report both effectiveness and robustness.The paper presents this as an empirical recommendation for these suites, not a universal claim; Honggfuzz ranks first in effectiveness but last in robustness.Source: §8 · p. 13, Table 4 · p. 13
- Splitting helps most when bugs arrive in bursts separated by long silences; use offline splitting when history exists and online splitting otherwise.Source: §8 · p. 13
9 Conclusion
- At matched compute, splitting improves unique-bug discovery in 53 of 70 FuzzBench pairs and lowers CPU-weighted variance in 66 of 70; online mode improves 38 of 40 Magma cells.Online splitting improves ground-truth bugs per CPU-hour in 38 of 40 Magma cells with no loss in raw distinct-bug counts, and changes CVE-2019-19926 from 0/20 to 20/20.Source: §9 · p. 13
Ethical Considerations
- Experiments used mature, legacy benchmarks exclusively in non-production settings and report no newly discovered deployed-system vulnerabilities or risks to individuals.The study states that responsible disclosure was not required and that it followed responsible research standards.Source: Ethical Considerations · p. 14
Open Science
- The released artifacts include experiment data, offline and online splitting implementations, reproduction scripts, and per-fuzzer figure grids; proofs remain in the appendices.The artifacts are available anonymously and are to be archived in a permanent repository upon publication.Source: Open Science · p. 14
A.1 Offline Splitting Implementation (Section 7.2)
- Offline splitting uses historical bug-count curves to identify persistent sparse tails, then branches only after a new bug on a running trial.Fuzzer-conditioned earliest detection times and ordered stages use persistence-smoothed sparsity, avoid extrapolating beyond observable intervals, and enforce a minimum gap between stages.Source: §A.1 · p. 14
A.2 Online Splitting Implementation (Section 7.4)
The online ablation uses past observations within each trial to select split times, while the accompanying theory states assumptions and separates sources of estimation error.
A.2 Online Splitting Implementation (Section 7.4)
- The online variant uses past-only sparsity and persistence to enter split stages, then splits at the next observed bug after zone entry.Its warm-up is S = max{w,H}; it uses stage thresholds and a minimum inter-stage gap.Source: §A.2 · p. 15
- The online ablation preserves the splitting mechanism, changes only the sparsity score, and is broadly deployable.Source: §A.2 · p. 15
B.1 Assumptions
- For genuinely non-stationary regimes, the framework uses windowed estimation with random restarting and aggregates estimates across approximately stationary windows.The transition process is assumed time-homogeneous for fixed mutation rules; internal state can be folded into an augmented state.Source: §B.1 · p. 15
- Convergence guarantees assume geometric ergodicity; observed output autocorrelation is a diagnostic consistent with geometric decay, not proof of it.The binary bug-output process itself is not assumed to be Markov.Source: §B.1 · p. 15
B.2 Additional Metrics and Results
- Under geometrically decaying stationary autocovariances, finite-horizon bias is bounded; initialization discrepancy vanishes for a stationary start but is not generally controlled by autocovariance decay alone.Source: §B.2 · p. 16, (Proof in Appendix F.5.) · p. 16
- The error decomposition separates finite-trial estimation, initialization, and finite-horizon autocovariance bias; only the finite-trial term depends on M.Concentration is at the M^-1/2 rate, while T enters through bias terms.Source: (Proof in Appendix F.5.) · p. 16
B.3 Assumptions and Proofs of the Core Guarantees
The section develops computable robustness bounds for fuzzing and explains their assumptions, then describes how splitting reallocates effort from bug-trigger states. Its guarantees include finite-campaign error control and conditions under which splitting reduces variance.
B.3 Assumptions and Proofs of the Core Guarantees
- The exact two-state starting-state term can be evaluated over every start and is up to 59× smaller than the general bound on the reported parameter range.A gap-only initialization term cannot distinguish a campaign starting at stationarity from one starting far from it.Source: §B.3 · p. 17
- Theorem 6’s bound does not require a Markov bug indicator, but its finite-horizon term requires geometrically decaying autocovariances.For reversible input chains, Lemma 7 supplies such a geometric envelope; the two-state estimate is an effective decay rate unless the bug indicator itself behaves as a two-state chain.Source: §B.3 · p. 17
C.1 From Section: Problem Formulation
- Coverage-target discovery can replace bug discovery when bugs are unknown or extremely rare, preserving an informative robustness measure even when BDR = 0.The analysis carries over because the target indicator remains a deterministic function of the input chain.Source: §C.1 · p. 17
C.2 From Section: Evaluation Framework
- Table 5 summarizes the key notation used throughout the paper.Source: Table 5 · p. 18
C.3 From Section: Theoretical Guarantees
- The Honggfuzz-on-openssl example gives a two-state calibrated interval of 0.37, within approximately 3× of the observed deviation, but this is not a general-chain guarantee.The interval is computed inside the stated two-state model.Source: §C.3 · p. 18
C.4 From Section: Splitting
- Splitting reduces dominant covariance contributions when it adds branches mainly in clustered bug regions; the analysis distinguishes independent forks from a separate coupled-noise construction.The anti-correlated-descendant construction quantifies an additional reduction that the implementation does not exploit.Source: §C.4 · p. 18, §14 · p. 18
C.5 From Section: Numerical Experiments
The numerical experiments compare splitting with independent runs at equal total compute and report gains on both FuzzBench and Magma. The conclusion maps which assumptions each guarantee requires.
C.5 From Section: Numerical Experiments
- Splitting finds more unique bugs in 53/70 FuzzBench pairs and more bugs per CPU-hour in 38/40 Magma cells, with no lower raw distinct-bug count in any Magma cell.In Magma, 34 of the 38 per-CPU-hour gains are individually significant; the ground-truth conclusion is established at M=20.Source: §C.5 · p. 18
- The variance reduction is approximately 10× in 66/70 pairs, and the clustered-bug theory gives the condition p < √2−1.The section identifies this condition with the non-saturated rare-bug regime, where the variance metric is informative.Source: §C.5 · p. 18
C.6 From Section: Conclusion
- The dependency map distinguishes the assumptions: positivity or reversibility is needed only for the variance lower bound, while the never-worse identity assumes nothing.The concentration bound requires only a geometric autocovariance envelope and carries its confidence level explicitly.Source: Table 6 · p. 19
D Additional Numerical Results
The appendix collects experimental details and proofs that clarify the scope of the theory. These include an ergodicity assumption, the variance-reduction condition, and a covariance criterion for increased expected value.
D Additional Numerical Results
- The experiments ran on Ubuntu 24.04.2 LTS with Intel Xeon Platinum 8480+ processors and 2.0 TB of RAM.The appendix also points to the full per-fuzzer Magma table and figure grids in the artifact.Source: D Additional Numerical Results · p. 19
E Discussions on the Assumptions
- The analysis assumes ergodicity, which rules out mutation processes trapped in restricted input-space regions; relaxing this assumption is left for future work.The authors report that empirical results align with theoretical predictions even when ergodicity is not enforced.Source: E Discussions on the Assumptions · p. 19
F.1 Proof of Theorem 2
- On the two-state surrogate, the variance ratio is below 1 exactly when p < √2−1.The proof first gives the condition p < r/(2+r), then substitutes r = (1−p)/p.Source: §F.1 · p. 20
F.3 Proof of Theorem 4
The appendix proves pathwise and probabilistic properties of splitting and the robustness bounds. It also specifies the scope of the variance result, initialization correction, and drift-sensitive estimates.
F.3 Proof of Theorem 4
- For any realized split tree, counting bug-trigger events across all branches cannot yield fewer than counting only the designated continuation path.The tree records every branch, while the designated path records only one branch at each time.Source: §F.3 · pp. 20–21
F.4 Proof of Proposition 5
- Reweighting a measure by m raises the expectation of V exactly when Covµ(m,V) > 0.Source: §F.4 · p. 21
F.5 Proof of Theorem 6
- Theorem 6 combines finite-trial sampling error, initialization error, and finite-horizon autocovariance bias, then uses a union bound across fuzzers.The proof identifies the sample variance across independent roots as unbiased for the finite-horizon variance.Source: §F.5 · p. 22
F.6 The exact starting-state term of Theorem 6
- For the two-state chain, the proof maximizes the exact starting-state term over possible starting probabilities to obtain a closed-form worst-start bound.Source: §F.6 · p. 22
F.7 Proof of Lemma 7
- For a reversible input chain, geometric contraction of the relevant quantity yields the stated bound on σ².Source: §F.7 · p. 28
F.8 Robustness of UA,R to the plug-in gap and to drift
- Shorter windows reduce drift bias but inflate the bound through horizon terms, creating a bias–variance trade-off in window length.The proof also states that underestimating the gap is conservative.Source: §F.8 · p. 28
F.9 Bug Detection Rate of Splitting
- The splitting identities hold pathwise for any realized tree shape; the bound makes the nonstationary fork starting point explicit through κ.On the two-state surrogate, κ = 1/π(B); a single two-way fork with κ = 1 recovers Theorem 2.Source: §F.9 · p. 28