Paper deep dive
Integrating High-Level Requirements to Low-Level Tests with Machine-Readable V&V Specifications
Mansur Arief, Nur Ahmad Khatim, Ali Akarma, Ahmad Alfan Alfian Irfan
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 91%
Last extracted: 7/21/2026, 5:26:43 AM
Summary
The paper introduces VNVSpec, an open-source framework that bridges the gap between high-level systems engineering requirements and low-level software tests. It provides a machine-readable, executable specification language that supports requirement decomposition, quality checking, and automated traceability linking to test results (from pytest, JUnit, etc.). The framework generates audit-ready reports, compliance matrices, and assurance cases, addressing regulatory needs for AI and cyber-physical systems.
Entities (10)
Relation Signals (9)
TraceLink â hasrelationtype â derives_from
confidence 95% ¡ A TraceLink is a typed edge with relations such as derives_from, verifies, mitigates, or maps_to.
TraceLink â hasrelationtype â verifies
confidence 95% ¡ A TraceLink is a typed edge with relations such as derives_from, verifies, mitigates, or maps_to.
VNVSpec â uses â Jest
confidence 95% ¡ The framework supports JUnit XML ingestion which covers JavaScript runners like Jest.
VNVSpec â uses â PyTest
confidence 95% ¡ The framework includes a pytest plugin to capture test outcomes.
VNVSpec â uses â JUnit
confidence 95% ¡ The framework includes a JUnit XML ingester to convert result files.
VNVSpec â supportscompliancewith â EU AI Act
confidence 92% ¡ The framework produces EU AI Act Annex IV technical-documentation skeleton for regulatory teams.
VNVSpec â alignswith â ISO/IEC/IEEE 29148
confidence 90% ¡ The framework checks requirement quality based on rules derived from systems engineering guidelines including ISO/IEC/IEEE 29148.
Requirement â linksto â Evidence
confidence 90% ¡ An Evidence record captures which requirement it verifies.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Modern software teams have mature tools for low-level testing, such as pytest, JUnit, and Jest, which make it inexpensive to write unit tests and run them on every commit. Systems engineering, in parallel, has developed rigorous principles for design verification and validation (V&V), which has worked very well across engineering discipline to align user expecations and requirements with developers' deliverables. In practice, however, the two rarely connect, and the link between users' high-level requirements and the low-level tests that machines actually run is maintained by hand, if at all. This gap is increasingly costly for AI-enabled and cyber-physical systems, for which regulators now ask for traceable evidence that high-level requirements are met, while raw test results provide little of the structure such evidence requires. We introduce VNVSpec, an open-source framework that makes V&V specifications machine-readable and executable. With this framework, users state high-level requirements directly or import them from catalogs derived from published standards. Then, the framework checks requirement quality, supports decomposition into module-level requirements with explicit metrics and acceptance criteria, links these requirements to test results through a traceability graph, and compiles the collected evidence into verdicts and audit-ready reports. We evaluate the framework by self-application, in which it is continuously assessed in CI against its own specification of 36 requirements verified by 449 tests, completed within limited time which scales linearly and thus can handle up to 10,000 requirements. We also discuss how the framework extends to testing black-box AI models and AI coding agents. The framework, its full test suite, the catalogs, and the benchmark scripts are available at this https URL.
Tags
Links
- Source: https://arxiv.org/abs/2607.17686v1
- Canonical: https://arxiv.org/abs/2607.17686v1
Trouble viewing inline? Open PDF directly â
Full Text
48,244 characters extracted from source content.
Expand or collapse full text
Integrating High-Level Requirements to Low-Level Tests with Machine-Readable V&V Specifications Mansur Arief Ali Akarma Nur Ahmad Khatim Ahmad Alfan Alfian Irfan Abstract Modern software teams have mature tools for low-level testing, such as pytest, JUnit, and Jest, which make it inexpensive to write unit tests and run them on every commit. Systems engineering, in parallel, has developed rigorous principles for design verification and validation (V&V), which has worked very well across engineering discipline to align user expecations and requirements with developersâ deliverables. In practice, however, the two rarely connect, and the link between usersâ high-level requirements and the low-level tests that machines actually run is maintained by hand, if at all. This gap is increasingly costly for AI-enabled and cyber-physical systems, for which regulators now ask for traceable evidence that high-level requirements are met, while raw test results provide little of the structure such evidence requires. We introduce VNVSpec, an open-source framework that makes V&V specifications machine-readable and executable. With this framework, users state high-level requirements directly or import them from catalogs derived from published standards. Then, the framework checks requirement quality, supports decomposition into module-level requirements with explicit metrics and acceptance criteria, links these requirements to test results through a traceability graph, and compiles the collected evidence into verdicts and audit-ready reports. We evaluate the framework by self-application, in which it is continuously assessed in CI against its own specification of 36 requirements verified by 449 tests, completed within limited time which scales linearly and thus can handle up to 10,000 requirements. We also discuss how the framework extends to testing black-box AI models and AI coding agents. The framework, its full test suite, the catalogs, and the benchmark scripts are available at https://github.com/ai-vnv/vnvspec. I Introduction Software engineering and systems engineering have each solved one half of the same verification and validation (V&V) problem. On the software side, low-level testing has become inexpensive: a developer writes a unit test in pytest [18] or a property-based test in Hypothesis [19], the continuous integration (CI) system runs it on every commit, and a pass-or-fail result comes back in minutes. On the systems side, high-level V&V has become rigorous: the INCOSE handbook [12], ISO/IEC/IEEE 29148 [15], and the NASA Systems Engineering Handbook [24] define how to write verifiable requirements, how to decompose them, how to plan verification activities, and how to maintain traceability from stakeholder need down to test evidence. However, both fields are often disconnected, which makes it difficult to trace and answer basic questions about the relationship between high-level requirements and low-level tests. Requirements traceability has been studied for a few decades [10, 6], and model-based systems engineering (MBSE) tools built around SysML [8, 20] do maintain these links. However, MBSE toolchains are heavyweight, live outside the developer workflow, and rarely connect to the test frameworks that developers actually run. In practice, high-level requirements live in a procurement or tender document or a ticket system, unit tests live in the code repository, and the mapping between the two is reconstructed manually by the technical team, if it is maintained at all. As a result, engineers can rarely answer, at any given commit, three basic questions: which user requirements are covered by which tests, which requirements have no test at all, and which standard clauses the current test evidence actually supports. The rise of AI applications makes this gap more consequential, for at least three reasons. First, AI-enabled systems are hard to specify, and their requirements practices lag behind their testing needs [1, 32, 28]. Second, regulation has arrived: the EU AI Act [7] requires technical documentation with exactly this requirements-to-evidence structure, and standards such as ISO/PAS 8800 [14], ISO 21448 [13], and UL 4600 [30] ask for argued, traceable safety evidence for AI and autonomous systems. Third, AI coding agents now write a growing share of production code. An agent that generates code from a user request has no standard way to record what the user asked for, how that request was decomposed, and which tests demonstrate that each part was met; without such a record, the output is unauditable by construction. Figure 1: The VNVSpec framework. High-level requirements enter from users or from standards-derived catalogs and pass a quality gate. They are decomposed into module-level requirements with explicit metrics and further into test cases whose results are captured as evidence records by existing test tools. Every link is an edge in a traceability DAG. Assessment rolls evidence up the graph into verdicts and produces role-specific outputs: compliance matrices for auditors, CI reports for developers, and GSN assurance cases for safety engineers. We address this gap by introducing VNVSpec, an open-source framework that makes the V&V specification itself a typed, machine-readable, and executable artifact, which is summarized in Fig. 1. The idea is to treat the specification as data: requirements, interface contracts, operational design domains, hazards, and evidence records are all typed objects that can be validated, composed, diffed, and traced. High-level requirements enter either from the user directly or from catalogs of curated requirements derived from published standards and framework documentation. The framework then supports the decomposition path that systems engineering prescribes, from high-level requirement, to module-level requirement with a defined metric and acceptance criterion, to concrete test cases. Test results flow back in from existing tools, and the framework rolls them up through the traceability graph into verdicts, compliance matrices, and assurance-case exports. Our contributions are two-fold. The first is a typed specification language for V&V, with immutable, serializable models for requirements, contracts, hazards, operational design domains, and evidence, together with a quality checker that flags vague or unverifiable requirements at authoring time. The second is a bridge to existing test tooling: a pytest plugin, JUnit XML ingestion that turns results from JavaScript, Java, and C++ test runners into requirement-linked evidence, an evidence collector for analysis scripts and formal verification runs, and model adapters that assess PyTorch and HuggingFace models directly. We illustrate when each evidence route applies through three worked examples, using pytest, Jest, and CROWN-based certified output bounds. We evaluate the framework by self-application and by measurement: the experiments in Section IV-C quantify the runtime of every stage of the pipeline, its scaling behavior up to 10,000 requirements, the overhead the integrations impose on existing test runs, and the detection behavior of the quality checker under seeded defects. We further envision agentic modules that decompose high-level specifications into unit tests, which motivates our future work. The remainder of this paper is organized as follows. Section I reviews related work on requirements quality, traceability, executable specifications, MBSE, and AI standards. Section I describes the design of the framework. Section IV illustrates the workflow, the choice among evidence routes, and the experimental evaluation. Section V discusses the experimental results in light of the claimed contributions. Section VI presents limitations and future work, and Section VII concludes. I Related Work I-A Requirements Quality and Traceability Requirements engineering doctrine is well established. ISO/IEC/IEEE 29148 [15] defines the characteristics of good requirements. The INCOSE Guide to Writing Requirements [11] turns these characteristics into concrete, checkable rules: use active voice, avoid vague terms, state a single verifiable condition, and so on. Traceability, the ability to follow a requirementâs life in both directions, was formalized by Gotel and Finkelstein [10], and its practical failures are well documented [6]. A substantial line of work treats lost traceability as a recovery problem and reconstructs links after the fact with word embeddings and sequential semantics [37, 5]. Recovery is needed precisely because links were never captured when the work was done: traceability maintained by hand decays, and the field has repeatedly called for traceability that arises as a by-product of normal work rather than as a separate activity. VNVSpec takes this position literally: trace links are typed objects created where the work happens, in code and in CI, and a scanner derives links automatically from requirement-ID references in the codebase. I-B Model-Based Systems Engineering MBSE replaces document-centric systems engineering with models, typically in SysML [8]. MBSE tools do maintain requirement decomposition and verification links, and the approach is standard practice in aerospace and automotive programs [20]. Our aim is not to replace MBSE. The observation is that most software teams, including most teams building AI systems, will not adopt a SysML toolchain, and MBSE tools do not integrate with pytest or a JavaScript test runner. VNVSpec carries the useful discipline of MBSE (typed requirements, decomposition, and traceability) into the developerâs own environment: plain Python objects, YAML or TOML files in the repository, and CI. I-C Executable Specifications and Requirements-as-Code Closer to our approach are practices that keep requirements next to the code. Behavior-driven development (BDD) expresses acceptance criteria in the Gherkin language and binds them to executable step definitions in tools such as Cucumber [33]. Requirements-as-code tools such as Doorstop [4] and Sphinx-needs [31] store requirement items as version-controlled text with typed links, and Eclipse Capra [21] maintains traceability links across heterogeneous development artifacts. These tools share our premise that requirements belong in the repository, but each covers only a slice of the requirement-to-evidence chain: BDD binds acceptance scenarios to tests but has no requirement quality checking, standards mapping, or verdict semantics; Doorstop and Sphinx-needs manage requirement items and links but do not consume test results as evidence; and Capra manages links without a specification model or assessment logic. VNVSpec combines these slices in a single typed model and adds the layers an audit requires: quality gates, standards registries, conservative verdict roll-up, and assurance-case export. I-D Testing of ML-Enabled Systems and AI Standards Software engineering for machine learning is an active field. Amershi et al. documented how ML changes the development workflow [1], and Sculley et al. described the resulting technical debt [29]. Testing of ML programs has been on the forefront research agenda in safety, security, and reliability domains since at least Nakajima and Buiâs work on dataset coverage as a test adequacy criterion [23], if not earlier. The ML Test Score [3] offers a rubric of tests that production ML systems should have, and Zhang et al. survey the ML testing landscape [36]. On the documentation side, model cards [22] and datasheets [9] record properties of models and datasets. These lines of work provide content (what to test and what to document) but not structure: none of them defines a machine-checkable chain from a stated requirement through a metric to a test result. Formal neural-network verification [16, 34] provides strong evidence for specific properties; in our framing they are evidence generators that need a formal specification framework. Finally, a cluster of standards now targets AI and autonomous systems directly: ISO/PAS 8800 for road-vehicle AI safety [14], ISO 21448 for safety of the intended functionality [13], UL 4600 for autonomous products [30], the NIST AI Risk Management Framework [25], and the EU AI Act [7], whose Annex IV specifies required technical documentation. All of them presuppose the same underlying structure: identified hazards, derived requirements, defined metrics, and traceable evidence. Assurance cases in Goal Structuring Notation (GSN) [17, 2] are the established notation for arguing that this structure is complete. Today, teams typically assemble this material manually for each audit, which is cumbersome and error-prone. Our framework addresses these needs. I The Proposed Framework Fig. 1 shows the overall framework, whose design follows four principles. First, specifications are data: every concept is a typed, immutable object that serializes losslessly to JSON, YAML, and TOML, so a specification is a reviewable, diffable file in the repository rather than a document in a separate tool. Second, the framework meets developers where they are: it does not run tests itself, but consumes the output of the test tools teams already use and contributes the layer those tools lack, the mapping from test results back to requirements. Third, standards are data too: clauses and curated best practices ship as importable registries and catalogs. Fourth, traceability is an enforced DAG: every link is an explicit edge in a directed acyclic graph (i.e., a graph whose links never loop back on themselves), and cyclic links are rejected at construction time, so rolling coverage up the graph is always well defined. We discuss each component briefly. I-A The Specification Language A Requirement carries an identifier, a normative statement, a rationale, a verification method (test, analysis, inspection, demonstration, or formal proof), acceptance criteria, a priority, and optional links to source documents and standards clauses. A Spec aggregates requirements, hazards, an operational design domain, and inputâoutput contracts, and validates global properties at construction time, such as uniqueness of requirement and hazard IDs. Specs can be written in Python, YAML, or TOML and loaded with Spec.from_file(); the three formats round-trip without loss. This matters in practice because requirement authors and test authors are often different people with different preferred tools. The three tiers in Fig. 1 are conventions we adopt. A tier-1 requirement states what the user needs. A tier-2 requirement refines it with a technical metric and a threshold, and derives_from links record the decomposition. A tier-3 artifact is a test whose result becomes an Evidence record linked by a verifies edge. Systems engineering handbooks describe exactly this decomposition [12, 24]; the framework makes each step a checkable object with actual tests. I-B Requirement Quality Checking Vague requirements are the earliest and cheapest defect to catch. Requirement.check_quality() implements eight rules derived from the systems engineering guidelines [11]: detection of vague and unbounded terms (âfast,â âuser-friendly,â âas appropriateâ), of escape clauses, of multiple conditions packed into one statement, of missing verification criteria, of passive voice that hides the responsible actor, and related defects. Profiles adjust strictness by context, since a formal safety requirement and a web-app requirement should not be held to identical phrasing rules. The checker runs at authoring time and in CI, so a requirement that cannot be verified is flagged before anyone writes a test against it. I-C Standards Registries and Requirement Catalogs VNVSpec provides two kinds of reusable content: registries and catalogs. Registries are clause databases for published standards such as ISO/PAS 8800, ISO 21448, UL 4600, the EU AI Act, and NIST AI RMF. Requirements reference clauses by identifier, and the compliance exporter (Section I-F) computes, for any chosen standard, which clauses are addressed by which requirements. Catalogs are curated requirement sets that encode published best practices for specific frameworks. Each catalog requirement passes a six-criteria inclusion gate: it must be actionable, verifiable, sourced from authoritative documentation, version-pinned to the target framework, mapped to standards clauses where applicable, and covered by an automated compatibility test. Currently, five catalogs hold 116 requirements, of which 71% carry at least one standards mapping (Table I). A team starting a FastAPI service does not begin from a blank page; it begins from Spec.extend() over the security, observability, and API-design catalogs, then adds project-specific requirements. This is the âstandards as high-level requirementsâ entry path in Fig. 1: the user can state requirements directly, or state which catalogs and standards apply. TABLE I: Example requirement catalogs. âMappedâ counts requirements carrying at least one standards-clause mapping. Catalog Primary sources Reqs. Mapped ml.pytorch_training PyTorch docs, NIST AI RMF 32 20 ml.huggingface_inference Transformers docs 25 14 web.fastapi OWASP API Top 10 [27] 22 20 web.sqlalchemy SQLAlchemy 2.0, Alembic docs 18 9 optimization.pyomo Pyomo docs 19 19 Total 116 82 I-D Traceability A TraceLink is a typed edge: source, target, and a relation such as derives_from, verifies, mitigates, or maps_to. build_trace_graph() assembles links into a directed graph and rejects cycles, so the requirement-to-evidence structure is a DAG by construction. Because hand-maintained links decay, auto_trace() scans the project tree for requirement-ID references, in test names, markers, docstrings, and comments, and generates verifies links automatically. The practical effect is that a developer who writes @pytest.mark.vnvspec("REQ-001") above a test has already done the traceability work. I-E Evidence Collection and Test Integration Evidence records are the point where the specification meets actual test results. An Evidence record captures a verification activity: which requirement it verifies, the kind of activity (test, analysis, inspection, demonstration, simulation, or formal proof), a verdict of pass, fail, or inconclusive, a timestamp, an artifact URI, and structured details such as metric values or certified bounds. Four routes produce evidence: ⢠The pytest-vnvspec plugin captures test outcomes during a normal pytest run and emits evidence records for every test marked with a requirement ID. It validates marker references against the spec at collection time, generates inconclusive evidence for any test-method requirement with no linked test, and supports a configurable fail-on policy (any, blocking, or never). ⢠The JUnit XML ingester converts result files from any runner that emits the format, which covers the JavaScript, Java, and C++ ecosystems, into evidence. The low-level tool does not need to know VNVSpec exists. ⢠EvidenceCollector, a context manager, wraps ad-hoc verification scripts, such as an analysis notebook, a black-box validation run, or a formal verification tool, and turns assertions and explicit verdicts into evidence records, validating every requirement against the spec. ⢠Adapters (such as TorchAdapter for n.Module models for PyTorch, TransformerAdapter, AutoregressiveAdapter, and VLMAdapter for HuggingFace encoder, generative, and vision-language models) wrap a model behind a common protocol and drive it over assessment data with budget-aware batching, out-of-memory recovery, and activation and gradient hooks, emitting per-requirement evidence directly. Assessment rolls the collected evidence up the trace graph into a report. The verdict logic is deliberately conservative: under the default strict policy, a requirement with any inconclusive evidence and no failures is judged inconclusive, reflecting the principle that the absence of evidence should never be mistaken for compliance. The CLI exposes the outcome through structured exit codes (0 for pass, 1 for failures, 2 for inconclusive, 3 for a spec validation error, 4 for a usage error, and 5 for an internal error), so a CI pipeline can gate on each condition distinctly. I-F Reporting and Export A single specification and a single body of evidence serve several audiences. The exporters produce an HTML report and Markdown summary for developers; a static V&V dashboard site with per-requirement detail pages, a standards-compliance table, and a version-history timeline; an XLSX/CSV compliance matrix with per-clause gap analysis for auditors; a GSN assurance case in Mermaid notation [2] for safety engineers; and an EU AI Act Annex IV technical-documentation skeleton populated from the spec for regulatory teams. A locally generated badge SVG and a Shields.io endpoint JSON surface the current verdict on the repository README. A GitHub Actions integration runs assessment on every push, publishes the badge, comments verdict summaries on pull requests, and diffs reports between commits so that a silently vanished piece of evidence is caught as a regression. IV Workflow, Routes, and Evaluation IV-A Workflow Example We illustrate the intended use via example: a team building an image classification service. The team imports the PyTorch training catalog, adds a user-level requirement, decomposes it, and gates CI on the assessment. In the following, Listing 1 shows the workflow, and Listing 2 shows the tier-3 step. Running pytest produces evidence; vnvspec assess builds the trace graph, checks that REQ-USER-001 is covered through REQ-MOD-003, and fails CI if it is not. vnvspec export then produces the report, the compliance matrix against the chosen standard, and the GSN argument, all from the same objects. Nothing in the flow required the team to leave Python and adopt another tool. The same flow is designed to admit an AI agent in the authoring loop. The decomposition steps, tier 1 to tier 2 to tier 3, are exactly the steps a coding agent performs implicitly when it turns a user request into code and tests. VNVSpec gives that process an explicit, checkable artifact: the agent proposes requirements and decompositions as Requirement objects, the GtWR checker and the human review them as data, and the trace graph records what the agent claimed. ⏠from vnvspec import Requirement, Spec from vnvspec.catalog.ml import pytorch_training # Tier 1: user requirement + catalog baseline user_req = Requirement( id="REQ-USER-001", statement="The service shall not return a " "diagnosis when input quality is " "outside the ODD.", verification_method="test", acceptance_criteria=["Out-of-ODD inputs " "yield an abstain response."], ) spec = Spec( name="diagnosis-service", requirements=[user_req], ).extend(pytorch_training.reproducibility) # Tier 2: decomposition with a metric mod_req = Requirement( id="REQ-MOD-003", statement="The input gate shall reject " "images with blur metric above " "0.35 (variance of Laplacian).", verification_method="test", acceptance_criteria=["Rejection rate on " "the blurred eval set is 100%."], ) Listing 1: From catalog and user requirement to CI verdict. ⏠import pytest @pytest.mark.vnvspec("REQ-MOD-003") def test_blur_gate_rejects_blurred_inputs( gate, blurred_eval_set): for img in blurred_eval_set: assert gate(img).action == "abstain" Listing 2: Tier 3: an ordinary pytest test, linked by marker. IV-B Choosing an Evidence Route: pytest, Jest, and CROWN The evidence routes serve different situations, depending on where the test that ultimately verifies the requirement naturally lives. We illustrate when each route applies. Route 1: pytest. If the decomposed requirement is implemented and checked in Python, the tier-3 test is an ordinary pytest test linked by a marker, as in Listing 2. This is the simplest route: evidence is captured during the test run the team already executes, and the marker itself serves as the trace link, so there is no separate export or conversion step that can fall out of date. It is the appropriate default whenever the property can be checked against concrete cases from within the Python test suite, whether the subject is a data-processing function, a service endpoint, or a trained model. Route 2: Jest through JUnit XML. High-level requirements do not respect language boundaries. Consider the user requirement REQ-USER-002, âthe clinician interface shall display the abstain state whenever the service abstains,â which decomposes to the React front-end that the team tests with Jest [26]. Rather than porting these tests to Python, the team keeps its native runner and transfers only the results, using JUnit XML, a test-result file format that most test runners can emit. The Jest test names the requirement in its title, and a three-line jest-junit configuration function turns that reference into a vnvspec property in the emitted JUnit XML (Listing 3). The ingester then converts the XML file into requirement-linked evidence (Listing 4, first part); skipped tests become inconclusive evidence, and references to unknown requirement IDs produce warnings rather than being silently dropped. Nothing in the JavaScript toolchain imports or depends on VNVSpec, and the same path serves any runner that emits JUnit XML, including those in the Java and C++ ecosystems. ⏠// ResultView.test.jsx (Jest) test("abstain banner shown [REQ-USER-002]", () => render(<ResultView result=abstain() />); expect(screen.getByRole("alert")) .toHaveTextContent("No diagnosis: input " + "outside supported domain"); ); // junitProperties.js (jest-junit hook): // title reference -> <property name="vnvspec"> module.exports = (tc) => const m = /\[(REQ-[A-Z0-9-]+)\]/ .exec(tc.title); return m ? vnvspec: m[1] : ; ; Listing 3: A Jest test verifying a high-level UI requirement. Route 3: CROWN (for deep learning models). Modules that embed machine learning models often carry requirements that must hold for every input in a continuous range, not just for the examples in a test set. Consider REQ-MOD-004: âFor every image in the blurred certification set and any perturbation δ with âδâââ¤8/255\|δ\|_â⤠8/255, the blur score shall remain above the rejection threshold 0.35.â A pytest test can sample perturbations, but no finite number of samples can establish a property that must hold across an entire continuous set, so example-based evidence for this requirement is inconclusive by nature. Neural network verification methods address exactly this situation. CROWN [35] computes guaranteed lower and upper bounds on a networkâs outputs that hold for every input within a specified perturbation range, and auto_LiRPA [34] provides an open-source implementation. Listing 4 wraps the certification run in an EvidenceCollector and records the outcome with kind="formal_proof", attaching the perturbation budget, the method, and the worst certified bound. ⏠import torch from auto_LiRPA import (BoundedModule, BoundedTensor) from auto_LiRPA.perturbations import ( PerturbationLpNorm) from vnvspec import EvidenceCollector with EvidenceCollector(spec) as c: # Route 2: ingest the Jest run (JUnit XML) c.from_pytest_junit("jest-junit.xml") # Route 3: CROWN bounds on the blur score bm = BoundedModule(blur_net, torch.empty_like(xs)) xb = BoundedTensor(xs, PerturbationLpNorm( norm=float("inf"), eps=8 / 255)) lb, _ = bm.compute_bounds( x=(xb,), method="CROWN") certified = lb > 0.35 # per-image guarantee c.record( "REQ-MOD-004", "pass" if bool(certified.all()) else "inconclusive", kind="formal_proof", message=f"int(certified.sum())/" f"len(xs) images certified", method="CROWN", eps=8 / 255, worst_lower_bound=float(lb.min()), ) report = c.build_report() Listing 4: Certifying output bounds with CROWN and recording evidence. The mapping from certification outcome to verdict illustrates the importance of strict verdict policydd. If the certified lower bound stays above the threshold for every image, the requirement receives a pass verdict that holds over the entire perturbation range, a guarantee that no finite test suite can provide. If CROWN fails to certify an image, this is not a counterexample: the bounds are guaranteed to be correct but are not always tight, so a loose bound only means that certification did not succeed. The evidence is therefore recorded as inconclusive, which keeps the requirement visibly open rather than silently passing. Only a concrete violating input, found for example by a falsification method, justifies a fail verdict. In the final report, the formal-proof evidence appears alongside the pytest and Jest evidence under the same requirement graph, and the compliance matrix reports each item with its evidence kind, so an auditor can distinguish a sampled check from a formal certificate at a glance. IV-C Experimental Evaluation We evaluate the framework along four questions. RQ1: Is the specification language expressive enough for a nontrivial system, and does continuous self-assessment catch real defects? RQ2: How do the core operations scale with specification size? RQ3: What overhead do the integrations impose on existing test workflows? RQ4: How reliably does the quality checker detect seeded requirement defects? IV-C1 Setup All measurements use the released packages, vnvspec 0.3.2 (from PyPI) and pytest-vnvspec 0.2.0, on deliberately CI-class hardware: a 2-core Intel Xeon at 2.80 GHz with 8 GB of RAM, Python 3.11, and pytest 9.1 on Linux. This choice is intentional, since the frameworkâs primary execution environment is a CI runner, not a workstation. We report medians of five runs (three for the two largest configurations). The benchmark scripts are part of the replication package. IV-C2 RQ1: Self-Application A specification framework should be able to specify itself. Since version 0.1.0, VNVSpec has been developed against its own specification, self-spec.yaml, kept in the repository and assessed in CI on every commit, under a stated policy that a change that breaks self-assessment is rolled back, not the specification. The self-spec currently holds 36 requirements (12 blocking, 17 high, 7 medium priority) covering the core model contracts, the trace layer, the quality checker, the registries and exporters, the error hierarchy, and meta-level requirements about backward compatibility and packaging. Each requirement is verified by the ordinary test suite, 449 tests under a 95% branch-coverage gate, and the most recent released assessment reports passing evidence for every requirement with none inconclusive. The self-spec caught real regressions during development: the backward-compatibility requirement turned an implicit norm into a released contract, and the dependency-declaration requirement was added after a CLI import error on clean installs; its automated check has prevented recurrence. The measured cost of this gate is small. End-to-end, vnvspec validate on the self-spec takes 0.54 s of wall-clock time including interpreter startup. The component costs are smaller still: loading the YAML spec takes 31 ms; quality-checking all 36 requirements takes 1.8 ms and reports 62 warnings and zero errors; building the trace graph takes 0.2 ms; and the exports take between 0.1 ms (GSN) and 8.1 ms (XLSX compliance matrix), with gap analysis against the 29-clause EU AI Act registry at 0.3 ms. IV-C3 RQ2: Scalability Table I reports the median runtime of each core operation on synthetic specifications of 10 to 10,000 requirements. All operations scale approximately linearly. YAML serialization and parsing dominate at every size; the frameworkâs own logic is comparatively cheap, with quality checking at 0.35 s and graph construction at 0.12 s even for 10,000 requirements. A 1,000-requirement specification, larger than any specification we have encountered in practice, round-trips through YAML in under 1.4 s and is quality-checked in 29 ms, which supports the claim runnable on every commit. TABLE I: Median runtime (seconds) vs. specification size, on 2-core CI-class hardware. QC = quality check of all requirements. Operation 10 100 1,000 10,000 Construct + validate <<0.001 <<0.001 <<0.001 0.002 Serialize to YAML 0.005 0.048 0.510 5.42 Load from YAML 0.009 0.087 0.868 10.2 QC (all requirements) <<0.001 0.003 0.029 0.352 Build trace graph <<0.001 <<0.001 0.004 0.118 Verdict roll-up <<0.001 <<0.001 <<0.001 0.002 IV-C4 RQ3: Integration Overhead Two experiments measure what the bridge costs the developer. First, we ran a suite of 400 no-op pytest tests, each marked with a distinct requirement ID, against a 400-requirement specification, with and without the plugin enabled. The suite takes 0.90 s without the plugin and 1.23 s with it, including spec loading, marker validation, evidence capture for all 400 tests, and writing the JSON report: an overhead of roughly 0.8 ms per test. Because the tests themselves do nothing, this is the worst case in relative terms; against any real test body the absolute per-test cost is what matters. Second, the JUnit XML ingester processes a 5,000-case result file, with embedded requirement properties and a 4% failure rate, in 0.46 s (about 11,000 cases per second), recovering all 4,800 pass and 200 fail verdicts correctly. IV-C5 RQ4: Quality Checker Under Seeded Defects We mutated each of the 36 self-spec requirement statements with four defect-seeding operators aligned with the GtWR rule classes, and counted a defect as detected when the mutant produces strictly more error- or warning-level findings than its unmutated original. Table I shows the results. The checker detects appended escape clauses and removed acceptance criteria perfectly (36/36 each). Injected vague terms are detected in 17 of 36 cases; the misses occur when the original statement already triggers the same lexical rule, so the mutation adds no new finding under our strict counting. Appended second conditions evade detection entirely (0/36): the current conjunction rule does not flag the added âshallâ clause. We report these negative results deliberately, and return to them in Section V. Two complementary observations: quality-checking the shipped artifacts yields zero error-level findings for both the self-spec (62 warnings) and all 116 catalog requirements (186 warnings), which reflects the intended two-tier use of severities, with errors gating and warnings advising. TABLE I: Seeded-defect detection by the GtWR quality checker Operator Seeded defect Detected Escape clause â, where possible and as appropriateâ 36/36 Missing criteria acceptance criteria removed 36/36 Vague terms âfast and user-friendlyâ appended 17/36 Packed conditions second âshallâ clause appended 0/36 V Discussion The experimental results bear on the two claimed contributions in different ways, and we discuss each in turn. For the first contribution, the typed specification language, RQ1 establishes expressiveness in the only way available short of a user study: the language specifies a nontrivial multi-package system, including meta-level requirements about backward compatibility and packaging that most requirement notations cannot express as checkable objects, and the resulting gate caught real regressions. The RQ4 results qualify the quality-checker component of this contribution honestly. Lexically visible defect classes are caught reliably: escape clauses and missing verification criteria, arguably the two defects with the highest downstream cost, are detected at 36/36. Structurally visible defects are not: a packed second condition passes the current conjunction rule unflagged, and vague-term injection is masked whenever the original already carries a finding of the same class. The checker should therefore be understood as the cheap first filter the design intends, one that raises the floor at authoring time, and not as a substitute for requirement review. The severity distribution across the shipped artifacts (zero errors, hundreds of advisory warnings over 152 requirements) shows the two-tier gate operating as designed in practice. For the second contribution, the bridge to existing test tooling, RQ2 and RQ3 turn the phrase âcheap enough to run on every commitâ from a design goal into a measurement. The full self-assessment gate costs 0.54 s end-to-end; the plugin adds 0.8 ms to each test of a suite that already exists; ingesting five thousand externally produced results costs half a second; and every core operation scales linearly to specification sizes an order of magnitude beyond any we have observed in practice, with the dominant cost being YAML parsing rather than any framework logic. These are the costs that determine whether traceability survives contact with a real CI pipeline, because a gate that developers can feel is a gate that gets disabled. The route experiments of Section IV-B complement the numbers by showing that the same evidence model absorbs results from a Python runner, a JavaScript runner that has never heard of the framework, and a formal verifier, without modification to any of them. VI Limitations and Future Work We identify three limitations along with future works. Evaluation validity: All evaluation in this paper was conducted by the frameworkâs own authors, on the framework itself, on a single machine, with seeded-defect operators of our own choosing. The measurements answer cost and scalability questions credibly, but they say nothing about authoring effort, defect-finding power relative to a baseline process, or audit-preparation time. The corresponding future work is a controlled study with external teams, measuring these three quantities against a documented baseline; the frameworkâs report-diffing facility provides the instrumentation, and we plan to conduct the study with community developers. Depth of the quality checker: The checker is heuristic, rule-based, and lexical, and RQ4 highlights its current state: it detects escape clauses and missing criteria perfectly but misses packed conditions entirely. More fundamentally, it inspects phrasing rather than correctness, so a precise, verifiable requirement can still be the wrong requirement; validation in the full sense still needs humans in the loop. The corresponding future work is a semantic tier for the checker, including conjunction analysis and language-model-assisted review, evaluated against the seeded-defect protocol. Ecosystem coverage: The five catalogs encode best-practice judgments pinned to framework versions and will drift as those frameworks evolve; whether community contribution under the published inclusion gate scales is an open question. The largest future opportunity, however, is agentic development: an AI coding agent run inside the VNVSpec protocol must state the tier-1 requirements it believes the user has, pass them through the quality gate, decompose them with explicit metrics, and produce tests that trace back up, so that the human reviews requirements and verdicts rather than raw diffs, and an auditor receives the same compliance matrix a human team would produce. The current study provides the protocol and data model, and we deliberately left to future work to orchestrating agents against them. VII Conclusion Low-level test tooling and systems-engineering V&V doctrine are both mature, but the connection between them has remained a manual and decaying artifact. This paper introduced VNVSpec, an open-source framework that makes that connection executable: typed requirements with quality checking, standards clauses and curated catalogs as importable data, an enforced traceability graph from user requirement to test evidence, evidence routes that span pytest, JUnit-emitting runners such as Jest, and formal bound-propagation tools such as CROWN, and role-specific exports generated from a single source of truth. The framework is self-hosting: it is developed against its own 36-requirement specification, verified by 449 tests under a 95% branch-coverage gate, with a rollback policy on self-assessment failures. The experiments show that this discipline costs little, with the full self-assessment gate at 0.54 s, per-test plugin overhead at 0.8 ms, and linear scaling to specification sizes well beyond practical need, while the seeded-defect study marks precisely where the quality checkerâs rule-based approach ends and future semantic checking must begin. If AI systems and AI-written software are to be certified, the requirement-to-evidence chain has to become a first-class engineering object, and our work provides a concrete proposal to achieve it by combining software and systems engineering approaches. References [1] S. Amershi, A. Begel, C. Bird, R. DeLine, H. Gall, E. Kamar, N. Nagappan, B. Nushi, and T. Zimmermann (2019) Software engineering for machine learning: a case study. In Proceedings of the 41st International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP), p. 291â300. Cited by: §I, §I-D. [2] Assurance Case Working Group (2021) Goal structuring notation community standard version 3. Note: SCSC-141C, Safety-Critical Systems Club Cited by: §I-D, §I-F. [3] E. Breck, S. Cai, E. Nielsen, M. Salib, and D. Sculley (2017) The ML test score: a rubric for ML production readiness and technical debt reduction. In Proceedings of the IEEE International Conference on Big Data, p. 1123â1132. Cited by: §I-D. [4] J. Browning and R. Adams (2014) Doorstop: text-based requirements management using version control. Journal of Software Engineering and Applications 7 (3), p. 187â194. Cited by: §I-C. [5] L. Chen, D. Wang, J. Wang, and Q. Wang (2019) Enhancing unsupervised requirements traceability with sequential semantics. In Proceedings of the 26th Asia-Pacific Software Engineering Conference (APSEC), p. 23â30. Cited by: §I-A. [6] J. Cleland-Huang, O. C. Z. Gotel, J. Huffman Hayes, P. Mäder, and A. Zisman (2014) Software traceability: trends and future directions. In Future of Software Engineering (FOSE), p. 55â69. Cited by: §I, §I-A. [7] European Parliament and Council (2024) Regulation (EU) 2024/1689 laying down harmonised rules on artificial intelligence (AI Act). Note: Official Journal of the European Union Cited by: §I, §I-D. [8] S. Friedenthal, A. Moore, and R. Steiner (2014) A practical guide to SysML: the systems modeling language. 3rd edition, Morgan Kaufmann. Cited by: §I, §I-B. [9] T. Gebru, J. Morgenstern, B. Vecchione, J. W. Vaughan, H. Wallach, H. DaumĂŠ I, and K. Crawford (2021) Datasheets for datasets. Communications of the ACM 64 (12), p. 86â92. Cited by: §I-D. [10] O. C. Z. Gotel and A. C. W. Finkelstein (1994) An analysis of the requirements traceability problem. In Proceedings of the First International Conference on Requirements Engineering, p. 94â101. Cited by: §I, §I-A. [11] INCOSE Requirements Working Group (2023) Guide to writing requirements. Technical report Technical Report INCOSE-TP-2010-006-04, International Council on Systems Engineering. Cited by: §I-A, §I-B. [12] INCOSE (2023) INCOSE systems engineering handbook: a guide for system life cycle processes and activities. 5th edition, Wiley. Cited by: §I, §I-A. [13] ISO (2022) ISO 21448:2022 â road vehicles â safety of the intended functionality. Note: International Organization for Standardization Cited by: §I, §I-D. [14] ISO (2024) ISO/PAS 8800:2024 â road vehicles â safety and artificial intelligence. Note: International Organization for Standardization Cited by: §I, §I-D. [15] ISO/IEC/IEEE (2018) ISO/IEC/IEEE 29148:2018 â systems and software engineering â life cycle processes â requirements engineering. Note: International Organization for Standardization Cited by: §I, §I-A. [16] G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer (2017) Reluplex: an efficient SMT solver for verifying deep neural networks. In Proceedings of the International Conference on Computer Aided Verification (CAV), LNCS, Vol. 10426, p. 97â117. Cited by: §I-D. [17] T. Kelly and R. Weaver (2004) The goal structuring notation â a safety argument notation. In Proceedings of the DSN Workshop on Assurance Cases, Cited by: §I-D. [18] H. Krekel et al. (2004) Pytest: helps you write better programs. Note: https://docs.pytest.org Cited by: §I. [19] D. R. MacIver, Z. Hatfield-Dodds, et al. (2019) Hypothesis: a new approach to property-based testing. Journal of Open Source Software 4 (43), p. 1891. Cited by: §I. [20] A. M. Madni and M. Sievers (2018) Model-based systems engineering: motivation, current status, and research opportunities. Systems Engineering 21 (3), p. 172â190. Cited by: §I, §I-B. [21] S. Maro and J. SteghĂśfer (2016) Capra: a configurable and extendable traceability management tool. In Proceedings of the 24th IEEE International Requirements Engineering Conference (RE), p. 407â408. Cited by: §I-C. [22] M. Mitchell, S. Wu, A. Zaldivar, P. Barnes, L. Vasserman, B. Hutchinson, E. Spitzer, I. D. Raji, and T. Gebru (2019) Model cards for model reporting. In Proceedings of the Conference on Fairness, Accountability, and Transparency (FAT*), p. 220â229. Cited by: §I-D. [23] S. Nakajima and H. N. Bui (2016) Dataset coverage for testing machine learning computer programs. In Proceedings of the 23rd Asia-Pacific Software Engineering Conference (APSEC), p. 297â304. Cited by: §I-D. [24] NASA (2016) NASA systems engineering handbook. Technical report Technical Report NASA/SP-2016-6105 Rev2, National Aeronautics and Space Administration. Cited by: §I, §I-A. [25] NIST (2023) Artificial intelligence risk management framework (AI RMF 1.0). Technical report Technical Report NIST AI 100-1, National Institute of Standards and Technology. Cited by: §I-D. [26] OpenJS Foundation (2014) Jest: delightful JavaScript testing. Note: https://jestjs.ioOpen-sourced by Facebook in 2014 Cited by: §IV-B. [27] OWASP Foundation (2023) OWASP API security top 10. Note: https://owasp.org/API-Security/ Cited by: TABLE I. [28] M. Rahimi, J. L. C. Guo, S. Kokaly, and M. Chechik (2019) Toward requirements specification for machine-learned components. In Proceedings of the IEEE 27th International Requirements Engineering Conference Workshops (REW), p. 241â244. Cited by: §I. [29] D. Sculley, G. Holt, D. Golovin, E. Davydov, T. Phillips, D. Ebner, V. Chaudhary, M. Young, J. Crespo, and D. Dennison (2015) Hidden technical debt in machine learning systems. In Advances in Neural Information Processing Systems (NeurIPS), Vol. 28, p. 2503â2511. Cited by: §I-D. [30] UL Standards & Engagement (2023) UL 4600: standard for safety for the evaluation of autonomous products. 3rd edition. Note: UL Standards & Engagement Cited by: §I, §I-D. [31] useblocks GmbH (2024) Sphinx-needs: requirements, specifications, and test cases inside sphinx. Note: https://sphinx-needs.readthedocs.io Cited by: §I-C. [32] A. Vogelsang and M. Borg (2019) Requirements engineering for machine learning: perspectives from data scientists. In Proceedings of the IEEE 27th International Requirements Engineering Conference Workshops (REW), p. 245â251. Cited by: §I. [33] M. Wynne and A. Hellesøy (2012) The cucumber book: behaviour-driven development for testers and developers. Pragmatic Bookshelf. Cited by: §I-C. [34] K. Xu, Z. Shi, H. Zhang, Y. Wang, K. Chang, M. Huang, B. Kailkhura, X. Lin, and C. Hsieh (2020) Automatic perturbation analysis for scalable certified robustness and beyond. In Advances in Neural Information Processing Systems (NeurIPS), Vol. 33, p. 1129â1141. Cited by: §I-D, §IV-B. [35] H. Zhang, T. Weng, P. Chen, C. Hsieh, and L. Daniel (2018) Efficient neural network robustness certification with general activation functions. In Advances in Neural Information Processing Systems (NeurIPS), Vol. 31, p. 4944â4953. Cited by: §IV-B. [36] J. M. Zhang, M. Harman, L. Ma, and Y. Liu (2022) Machine learning testing: survey, landscapes and horizons. IEEE Transactions on Software Engineering 48 (1), p. 1â36. Cited by: §I-D. [37] T. Zhao, Q. Cao, and Q. Sun (2017) An improved approach to traceability recovery based on word embeddings. In Proceedings of the 24th Asia-Pacific Software Engineering Conference (APSEC), p. 81â89. Cited by: §I-A.