# The axes The project classifies every verification method by where its inputs come from and how its output is judged. Two more axes complete the frame: the guarantee a passing run earns and the effect scope a method reaches. Each method page carries its own *Classification* section. **[Input](https://quality.stereobooster.com/input.md)** and **[oracle](https://quality.stereobooster.com/oracle.md)** are independent: a method's position is one value on each, or a *set* of oracle values where one run is judged by several oracles at once. **[Guarantee](https://quality.stereobooster.com/guarantee.md)** (how strong a claim a passing run makes) is *not* a third independent axis: it is *capped* by the other two and derived from them ([why](https://quality.stereobooster.com/guarantee.md#not-an-independent-axis)). It is still recorded per method, because the reachable ceiling is rarely the tier a method actually achieves. All of this classifies the **method**. **[Effect](https://quality.stereobooster.com/effect.md)** is a different kind of thing: a property of the **code under test** (what the code touches, from pure through stateful, I/O-bound and nondeterministic), read to *select* an adequate method. From the method's side the same cut becomes **effect scope**, and that is what a method page records. The [terminology page](https://quality.stereobooster.com/terminology.md) maps the conventional test categories onto the axes. ## What the model is for **Methods become comparable on a shared axis.** "Should we add property tests or fuzzing?" is a question about input. Both apply to pure functions; the difference is whether the inputs are schema-shaped or unfiltered, and what oracle each carries. **A suite's own gaps become visible.** A team running only example tests has covered one column of the input axis and nothing else. A team running fuzzing only on pure functions and example tests on boundary-crossing code has gaps in the middle. **The argument about levels dissolves.** Most of the energy spent on "what *level* is this test?" belongs instead in "where do the inputs come from, and what's the oracle?" The axes give specific names to the decisions the levels vocabulary hides. ## The same check at three rigor levels Methods that look unrelated are often one question asked at different strengths. Where the [oracle](https://quality.stereobooster.com/oracle.md) stays fixed — *what* gets checked — and only the [input](https://quality.stereobooster.com/input.md) varies, a single property splits across families under separate names. How much of the input space a run covers sets the [guarantee](https://quality.stereobooster.com/guarantee.md): a property can be **proved** for all inputs, **tested** on a sample, or **observed** on live traffic. One such property is the predicate `x > 0`: | Level | Method | Family | | --- | --- | --- | | **Proved** (all inputs) | [refinement & dependent types](https://quality.stereobooster.com/refinement-and-dependent-types.md), [theorem proving](https://quality.stereobooster.com/theorem-proving.md) | types / formal | | **Tested** (sampled inputs) | [property-based testing](https://quality.stereobooster.com/property-based-testing.md) | tests | | **Observed** (live inputs) | [contracts & runtime assertions](https://quality.stereobooster.com/contracts-and-runtime-assertions.md) | runtime | The same predicate is checked three ways: a type system rejects the program for it, a property test throws thousands of generated inputs at it, or a runtime assertion fires on the one that slips through in production. [Contracts as specifications](https://quality.stereobooster.com/contracts-as-specifications.md) map this level-by-level. The pattern isn't special to that oracle. Equivalence between a new implementation and the old one splits the same way: | Level | Method | Family | | --- | --- | --- | | **Proved** (all inputs) | [equivalence checking](https://quality.stereobooster.com/equivalence-checking.md) | formal | | **Tested** (sampled inputs) | [differential testing](https://quality.stereobooster.com/differential-testing.md) | tests | | **Observed** (live inputs) | [parallel run](https://quality.stereobooster.com/parallel-run.md) | runtime | The levels are a menu, not a hierarchy: the highest one the stakes justify is the one to use, and a lower one serves where the higher is infeasible — proof doesn't scale to a whole program, and unpredictable inputs surface only in production. ## Locating methods on the axes A few methods, picked to span the extremes of each axis: | Method | Input | Oracle | Guarantee | | ------------------------- | --------------- | ----------------------- | --------------- | | Example test | Fixed | Any | Empirical | | Fuzzing | Generative | Errors | Empirical | | Type checking | — | Predicate (type) | Exhaustive¹ | | seL4-style proof | — | Predicate | Mathematical| | Production monitoring | Live | Probabilistic | Heuristic | ¹ Within the explicit bounds of what the type system is able to express. Every method's full position, plus the quality dimensions it serves, is in the per-family tables in the [methods catalog](https://quality.stereobooster.com/methods.md). **Visibility** (black-box, gray-box, white-box) is not one of the axes: a method keeps its coordinates whether or not the source is at hand. It decides which coordinates are *available* — a generative-feedback input needs a feedback channel, and a structural coverage criterion needs instrumentation. The [terminology page](https://quality.stereobooster.com/terminology.md#visibility-black-box-gray-box-white-box) sets out the gradient. ## The model is a *device*, not a claim The axes claim no empirical superiority over any other vocabulary. No study compares teams that use this framing with teams that use something else. The model makes hidden decisions visible. A team using any single-axis taxonomy has implicitly chosen positions on the other axes (a fixed input, an equality oracle, and an *empirical* guarantee being the most common defaults) without acknowledging those are choices. The model is for thinking, not for ranking. The ranking question (*which methods actually catch bugs?*) is the empirical question answered case-by-case in the [methods catalog](https://quality.stereobooster.com/methods.md). ## Prior taxonomies The axes are not new: they assemble established taxonomies, one per axis, into a single cross-method frame. Where the field already has a standard vocabulary, the axes reuse it: - **[Oracle](https://quality.stereobooster.com/oracle.md)** ← Barr et al.'s oracle survey (Barr et al. 2015)[^barr2015]: *specified / derived / implicit / human*, refined by metamorphic arity (Chen et al. 2018)[^chen2018] and the atomic-vs-aggregated cut (Dobslaw et al. 2025)[^dobslaw2025]. - **[Input](https://quality.stereobooster.com/input.md)** ← Anand et al.'s test-generation survey (Anand et al. 2013)[^anand2013]: random, search-based, symbolic, combinatorial, model-based. - **[Guarantee](https://quality.stereobooster.com/guarantee.md)** ← soundness (program analysis) for the tiers; assurance levels (RTCA 2011; IEC 2006)[^do178c] [^iec62304] are a *related but distinct* scale (consequence of failure, not claim strength), not the tiers' source. - **[Effect](https://quality.stereobooster.com/effect.md)** ← Koka's effect rows (Leijen 2014; Lucassen and Gifford 1988)[^leijen2014] [^lucassen1988] and Google's test *size* (Winters et al. 2020)[^winters2020], recomposed for testing (chiefly by splitting nondeterminism into magnitude tiers). What's specific here is the *assembly*: one orthogonal frame spanning tests, types, formal methods, and monitoring (not the individual axes), used to tell look-alike methods apart — noting which single coordinate separates each confusable pair. A 2025 faceted taxonomy for LLM testing organizes around SUT / Goal / Oracle / Input (Dobslaw et al. 2025)[^dobslaw2025]; the faceting approach recurs, though that work shares an author with the oracle survey and its facets don't map one-to-one to ours, so it is lineage, not independent confirmation. ## Referenced by - [Quality dimensions](https://quality.stereobooster.com/quality-dimensions.md) · Quality dimensions - [Effect scope](https://quality.stereobooster.com/effect.md) · The axes - [Methods](https://quality.stereobooster.com/methods.md) · Methods - [Conventional](https://quality.stereobooster.com/conventional.md) · Conventional - [Conventional terminology](https://quality.stereobooster.com/terminology.md) · Conventional - [Testing folklore](https://quality.stereobooster.com/testing-folklore.md) · Conventional - [About this project and how it is checked](https://quality.stereobooster.com/about.md) · Overview - [Choosing methods](https://quality.stereobooster.com/choosing.md) · Overview - [Software Quality](https://quality.stereobooster.com/index.md) · Overview ## References [^barr2015]: Barr, Earl T., Mark Harman, Phil McMinn, Muzammil Shahbaz, and Shin Yoo. 2015. "[The Oracle Problem in Software Testing: A Survey](https://ieeexplore.ieee.org/ielx7/32/7106034/06963470.pdf)." *IEEE Transactions on Software Engineering* 41 (5): 507–25. . [^chen2018]: Chen, Tsong Yueh, Fei-Ching Kuo, Huai Liu, et al. 2018. "[Metamorphic Testing: A Review of Challenges and Opportunities](https://www.cs.hku.hk/data/techreps/document/TR-2017-04.pdf)." *ACM Computing Surveys* 51 (1): 1–27. . [^dobslaw2025]: Dobslaw, Felix, Robert Feldt, Juyeon Yoon, and Shin Yoo. 2025. *[Challenges in Testing Large Language Model Based Software: A Faceted Taxonomy](https://arxiv.org/pdf/2503.00481)*. arXiv:2503.00481. . [^anand2013]: Anand, Saswat, Edmund K. Burke, Tsong Yueh Chen, et al. 2013. "[An Orchestrated Survey of Methodologies for Automated Software Test Case Generation](https://romisatriawahono.net/lecture/rm/survey/software%20engineering/Software%20Testing/Anand%20-%20Automated%20Software%20Test%20Case%20generation%20-%202013.pdf)." *Journal of Systems and Software* 86 (8): 1978–2001. . [^do178c]: RTCA. 2011. *[DO-178C: Software Considerations in Airborne Systems and Equipment Certification](https://www.rtca.org/do-178/)*. . [^iec62304]: IEC. 2006. *[IEC 62304: Medical Device Software — Software Life Cycle Processes](https://webstore.iec.ch/en/publication/6792)*. . [^leijen2014]: Leijen, Daan. 2014. "[Koka: Programming with Row Polymorphic Effect Types](https://arxiv.org/pdf/1406.2061)." *Proceedings of MSFP 2014 (Mathematically Structured Functional Programming)* 153: 100–126. . [^lucassen1988]: Lucassen, John M., and David K. Gifford. 1988. "[Polymorphic Effect Systems](https://ailang.sunholo.com/assets/files/lucassen-gifford-1988-0ae4870d6303ed164b78696901c7f22d.pdf)." *Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '88)*, 47–57. . [^winters2020]: Winters, Titus, Tom Manshreck, and Hyrum Wright, eds. 2020. *[Software Engineering at Google: Lessons Learned from Programming Over Time](https://abseil.io/resources/swe-book/html/ch11.html)*. O'Reilly Media. . ## Acronyms - SUT — system under test