Architectural Verification and Assurance Framework for Fictional Autonomous Kill-Web Systems: A Public-Safe Laboratory Metamodel

The deployment of distributed, autonomous multi-agent systems—frequently conceptualized in theoretical frameworks as autonomous “kill-webs”—introduces profound and unprecedented complexities in safety assurance, formal verification, and system validation. Traditional safety engineering methodologies, which rely heavily on component reliability metrics and static, end-of-lifecycle testing, are fundamentally inadequate for evaluating non-deterministic, learning-enabled, and highly coupled distributed systems operating under the open-world assumption. To address this, the theoretical KillWebs.com laboratory platform is proposed as a synthetic, public-safe testbed for constructing, managing, and evaluating dynamic assurance cases.
This report establishes the architectural and procedural foundation for the KillWebs.com platform. It synthesizes advanced methodologies in formal verification, eliminative argumentation, Systems-Theoretic Process Analysis (STPA), runtime assurance (RTA), and software supply-chain integrity. The framework provides a structured approach to continuously verifying synthetic autonomous architectures using unclassified, non-lethal scenarios, separating the mathematical verification of software components from the validation of the complex socio-technical human-machine system.

1. Assurance-Case Metamodel and Graph Structure

To continuously evaluate the safety and reliability of complex autonomous architectures, the underlying assurance-case metamodel must support dynamic, machine-readable, and modular reasoning. The proposed metamodel is heavily grounded in the Object Management Group’s (OMG) Structured Assurance Case Metamodel (SACM) version 2.2, which standardizes the representation of assurance cases through distinct packages for Argumentation, Artifacts, and Terminology1. Furthermore, it integrates the principles of Goal Structuring Notation (GSN) Version 3 and “Assurance 2.0” (Eliminative Argumentation), which require developers to actively seek out and formally refute doubts and counterclaims to achieve indefeasible confidence5.
The metamodel represents an assurance case as a directed acyclic graph (DAG) composed of specific nodes and edges that formalize the dialectical reasoning process. The structural graph includes:

• Top-Level Claims: The ultimate propositions of safety or security for the target system, carrying external significance (e.g., “The synthetic swarm will not engage targets outside the designated geofence”).
• Subclaims: Decomposed assertions that logically support the top-level claim, breaking the argument down into verifiable elements.
• Supporting Evidence: Artifacts, test results, formal proofs, or simulation logs that provide empirical or mathematical backing for a subclaim4.
• Contradictory Evidence: Artifacts or test results that directly refute a claim, initiating an automatic re-evaluation of the argument branch5.
• Assumptions: Explicitly declared environmental or operational conditions under which the claims are considered valid, essential for establishing the system’s operational design domain (ODD).
• Counterclaims: Alternate hypotheses or adversarial assertions challenging the validity of a claim, often generated through Socratic or dialectical examination5.
• Defeaters (Doubts): Formal representations of vulnerabilities, gaps in reasoning, or epistemic uncertainties. Defeaters actively attack claims, evidence, or the inference rules connecting them5. Under Eliminative Argumentation, a claim is only considered sound if all associated defeaters are actively refuted or mitigated.
• Verification Activities: The specific processes (e.g., bounded model checking, human-in-the-loop simulation) executed to generate evidence.
• Residual Risks: Unresolved or accepted defeaters that fall within an acceptable, quantified threshold of mission tolerance9.
• Review Roles: Cryptographically signed identities of the human or automated agents responsible for auditing and authorizing specific graph nodes, maintaining adherence to independence standards.
• Configuration Versions: Links mapping specific claims to exact cryptographic hashes of the software and hardware configurations under test.
• Invalidating Changes: Formal triggers that define the exact environmental, software, or policy shifts that render a claim or piece of evidence obsolete.
• Current Claim States: The dynamic, real-time evaluation of a claim’s validity.

1.1 Defined Conservative Claim States

Because autonomous architectures operate in highly dynamic environments, static binary states (Pass/Fail) are insufficient. The metamodel enforces conservative claim states that reflect the epistemic confidence of the graph at any given moment.

2. Machine-Readable Claim and Evidence Schema

To enable programmatic evaluation, the KillWebs.com platform represents the SACM metamodel via a JSON-LD schema. This schema utilizes W3C PROV-O for robust provenance tracking, ensuring that every fact and audit trail is exportable to compliance frameworks11. The schema is designed for seamless interoperability with software supply chain metadata formats like in-toto and SLSA12.

3. Dependency-Propagation Model

The assurance case operates as a reactive DAG. The dependency-propagation model dictates how information—specifically doubt, invalidation, and probabilistic confidence—flows upward from evidence to top-level claims. The propagation strictly follows the principles of Eliminative Argumentation6. Confidence in a claim is not merely the aggregate of positive evidence, but the explicit absence of unrefuted defeaters.
The propagation rules govern state transitions across the graph. If an evidence node transitions to an Unresolved or Withdrawn state (for example, due to the introduction of contradictory test results), the parent subclaim immediately transitions to Suspended pending re-review. This suspension cascades upward to the Top-Level Claim until the graph is repaired, or an alternative, redundant subclaim (such as a diverse verification method) fulfills the requirement9. Conversely, changes in global assumptions propagate downward. If the assumed maximum latency of a communication network is altered, this top-down propagation triggers the invalidation rules of any evidence or subclaim reliant on the previous assumption.
The injection of a defeater node alters the flow of confidence. The introduction of a new defeater immediately transitions the target node to Unresolved. The target node cannot return to a Supported state until a counter-evidence node or a second-level defeater successfully refutes the primary defeater, or until the defeater is formally accepted as a residual risk posing a negligible threat5. Probabilistic methods, utilizing Bayesian Belief Networks or Fréchet bounds, can be integrated to assess the residual risk of these unresolved doubts, prioritizing investigation based on the defeater’s potential impact on the overall assurance case9.

4. Change-Impact Algorithm Specification

To handle the continuous integration and deployment (CI/CD) pipelines characteristic of modern software, the KillWebs.com platform utilizes a rigorous change-impact analysis algorithm. This algorithm determines exactly how the public lab must react when dynamic conditions shift, operating on a set of deterministic rules20.

1. Software Changes: When a cryptographic hash of a compiled binary or source file changes, the system compares the new hash against the baseline. If they differ, all evidence nodes derived from the baseline are marked as stale, propagating a suspension state upward through the graph.
2. Model Changes: If the system architecture model or state machine is updated, an automated dependency graph traversal executes, setting all downstream claims utilizing the altered interfaces or control loops to an unresolved state until re-verified.
3. Threshold or Policy Changes: If an operational policy, such as synthetic rules of engagement, is modified, the algorithm automatically injects a defeater labeled “Policy non-compliance risk” to the top-level safety claim, forcing a review of all subordinate engagement logic.
4. Stale Evidence: A chronological monitor evaluates the timestamp of evidence generation. When the current time exceeds the declared expiration date of the evidence, the evidence node transitions to a suspended state pending re-review or automated re-generation.
5. Contradicted Evidence: If new evidence (such as field telemetry or continuous integration test results) conflicts with existing evidence, both evidence nodes are immediately set to unresolved, triggering a mandatory manual arbitration by an independent verification auditor.
6. Source Correction: When an external data source or third-party dependency issues a correction or retraction, the algorithm triggers a re-evaluation of all evidence generated using that source, recursively walking the provenance chain.
7. Authority Expires: If a reviewer’s cryptographic certificate or laboratory accreditation (e.g., ISO/IEC 17025) expires, all approvals associated with that signature are suspended until the authority is renewed and the claims are re-attested21.
8. Human-Supervision Condition Changes: If telemetry indicates that human operator availability drops below the assumed threshold for maintaining a human-in-the-loop, claims dependent on human oversight transition from fully supported to supported with qualifications, triggering a degraded autonomous operating mode23.
9. Operating Environment Moves Outside Tested Envelope: If sensor data reveals that the operating environment parameters (e.g., sensor noise levels, adversary electronic warfare presence) fall outside the assumptions of the tested envelope, the top-level claim is withdrawn for the current scope, as the system is outside its valid operational design domain.
10. Recovery Control Fails: If a Simplex architecture fallback or secondary recovery control fails during a runtime assurance test, an active defeater labeled “Loss of Runtime Assurance” is applied directly to the root safety claim, halting synthetic deployment25.
11. New Dependency Introduced: The introduction of a new component in the Software Bill of Materials (SBOM) sets all integration claims related to the parent module to unresolved until the new dependency undergoes specific verification activities.
12. Reproducibility Failure: If an automated re-run of a verification activity fails to reproduce the original evidence exactly, the original evidence is immediately withdrawn due to a lack of deterministic reliability.

5. Catalog of Hazards and Unsafe Control Actions

Standard hazard analysis techniques, such as Fault-Tree Analysis (FTA) or Failure Modes and Effects Analysis (FMEA), historically treat accidents as the result of component failures or linear event chains. However, high-consequence autonomous systems often fail due to unsafe interactions between perfectly functioning components, flawed requirements, or software logic errors. Therefore, the KillWebs.com metamodel employs Systems-Theoretic Process Analysis (STPA) to identify systemic risks26. STPA treats safety as a control problem, focusing on Unsafe Control Actions (UCAs) issued within a hierarchical control structure comprising controllers, actuators, and feedback loops29.
The following catalog models a synthetic, unclassified “Autonomous Overwatch Network” consisting of a human operator, a central planner, and distributed swarm agents. Control actions become unsafe under four conditions: not providing the action, providing it unsafely, providing it too early/late/out of sequence, or stopping too soon/applying too long27.

6. Catalog of Assurance Evidence Types

The generation of evidence requires distinct methodologies depending on whether the subject is a deterministic software component or a complex socio-technical system involving human-machine teaming.

6.1 Component Behavior Evidence

• Bounded Model Checking & Formal Verification: Mathematical proofs of correctness are utilized to explore the finite state space of system models. Tools such as UPPAAL (for timed automata and real-time constraints) and TLA+ (for distributed consensus algorithms like Paxos and Raft) are used to prove the absence of deadlocks, ensure network consensus despite Byzantine failures, and mathematically verify collision avoidance logic34.
• Signal Temporal Logic (STL) and Runtime Assurance (RTA): Because formal verification cannot feasibly cover the infinite continuous state spaces of machine-learning components or highly complex environments, RTA monitors are deployed as safety wrappers. STL provides a formal specification language to describe temporal properties over continuous signals (e.g., utilizing operators like Eventually, Always, and Until)38. The system calculates the robustness degree—a quantitative measure of how well a constraint is satisfied39. If the robustness degree approaches zero, indicating an imminent violation, the RTA triggers a deterministic, formally verified fallback controller via a Simplex architecture25. Advanced semantics, such as Cumulative-Time STL (CT-STL) and robustness-to-go, allow the RTA to evaluate historical persistence and suffix trajectories during model predictive control38.
• Contract-Based Design: This method supports compositional verification, where individual software modules guarantee certain outputs provided that their inputs meet rigorously specified assumptions, allowing for the mathematical composition of system-level safety properties42.

6.2 Combined Human-Machine System Evidence

• Human-in-the-Loop (HITL) Simulations: Evidence must be gathered by evaluating the system’s interface with actual operators. Metrics include response latency, situational awareness, and susceptibility to automation bias. HITL is critical for proving that a human can realistically exercise veto power within the required time constraints of an autonomous kill-web43.
• Workload and Cognitive Overload Modeling: Empirical data is required to demonstrate that the volume of alerts, sensor data, and telemetry generated by a distributed swarm does not exceed the human operator’s cognitive processing capacity during high-stress, multi-agent scenarios23. Frameworks must incorporate Dynamic Role and Task Allocation (DRTA) to shift burdens between AI and human agents to prevent bottlenecks23.
• Adversarial and Edge-Case Testing: Simulated injection of edge cases (e.g., spoofed sensor data, communication degradation) is utilized to observe the combined response and cross-species trust calibration of the human-AI team23.

7. Limitations of Simulation: The Reality Gap

A core principle of the KillWebs.com platform is the formal recognition of the “reality gap.” The platform dictates a strict rule: simulation alone is fundamentally insufficient for the certification of autonomous kill-webs43. The assurance graph must explicitly declare what cannot be proven virtually, requiring corresponding defeaters to remain active until physical world validation occurs.
Simulation cannot definitively prove:

1. Physical Hardware Degradation: Unmodeled kinetic friction, thermal limits, battery degradation, and actuator wear under sustained physical stress and G-forces over time.
2. Adversarial Electronic Warfare (EW): Complex, real-world spectrum denial, GPS spoofing, and advanced persistent threats (APTs) manipulating the physical layer of communication networks in ways that pristine simulation models fail to anticipate.
3. Human Psychological Factors: The profound physiological stress, fatigue, adrenaline response, and moral panic experienced by human operators when dealing with real-world lethal consequences cannot be accurately replicated in a low-stakes simulator45.
4. Weather and Atmospheric Anomalies: Micro-climates, unpredictable aerodynamic shear, and complex visual occlusions (fog, dust, glare) that degrade electro-optical and infrared sensors in ways that algorithmic statistical noise models cannot fully capture.

8. Independence and Reviewer-Competence Requirements

To prevent confirmation bias, conflict of interest, and regulatory capture, the platform strictly enforces the Independent Verification and Validation (IV\&V) standards outlined in IEEE 1012-201650.
For high-consequence systems—assigned Software Integrity Level (SIL) 4 due to the potential for catastrophic loss of life or mission failure—IEEE 1012 mandates three specific forms of independence for the reviewing authority:

• Technical Independence: The IV\&V team must utilize different analysis tools, compilers, test methodologies, and problem formulations than the primary development team to avoid repeating the same systemic errors52.
• Managerial Independence: The IV\&V team must report to a different chain of command, completely isolating them from the programmatic schedule or cost pressures that often drive engineering compromises53.
• Financial Independence: The IV\&V budget must be controlled separately from the development budget, ensuring that verification efforts cannot be financially starved by the system acquirer52.

Furthermore, laboratories providing empirical data to the KillWebs platform must demonstrate competence through ISO/IEC 17025 accreditation. This ensures that the testing environment, calibration of instruments, and software validation of the laboratory equipment itself meet stringent international metrology and quality standards, proving that the tools generating the evidence are themselves sound21.

9. Provenance and Reproducibility Policy

The integrity of an assurance case graph is entirely dependent on the integrity of its underlying evidence. An altered test log, a compromised compiler, or a maliciously injected dependency can fatally undermine the graph. Therefore, the KillWebs.com policy mandates compliance with the Supply-chain Levels for Software Artifacts (SLSA) v1.0 standard12.
To achieve SLSA Level 3 (the required baseline for KillWebs.com assurance evidence), the build and test environments must be fully automated, hermetic, and hardened against interference55. Every artifact—source code, compiled binary, formal proof output, and test result—must be accompanied by non-falsifiable provenance metadata.
This provenance is achieved using the in-toto attestation framework. Whenever a verification activity (e.g., a UPPAAL model checking run) concludes, the test runner generates an in-toto attestation wrapping the results. This attestation is signed using keyless signature infrastructure (such as Sigstore) tied strictly to the isolated machine identity, utilizing the Verification Summary Attestation (VSA) and Software Supply Chain Attribute Integrity (SCAI) predicates14. The KillWebs.com assurance graph automatically rejects any evidence node lacking a valid, cryptographically verified in-toto attestation, enforcing absolute reproducibility.

10. Synthetic Assurance-Case Example

To illustrate the metamodel in action, consider a synthetic assurance case for a fictional “Swarm Area Denial System” designed to monitor a geographic zone.
Top-Level Claim (C1): The swarm will safely monitor the zone and will not initiate kinetic engagement without explicit, verified human authorization. (Current State: Supported with qualifications).

• Subclaim (SC1.1): The swarm correctly identifies human targets versus non-combatants.
• Evidence (E1.1.1): Visual classifier test results across 10,000 synthetic varied environments with SLSA Level 3 provenance. (State: Supported).
• Defeater (D1): The classifier exhibits high false-positive rates when subject to adversarial optical noise (e.g., laser dazzlers). (State: Active).
• Counter-claim (CC1): Sensor fusion with thermal imaging mitigates optical dazzle.
• Evidence (E1.1.2): Formal verification of the sensor-fusion voting algorithm. (State: Supported).
• Result: D1 is refuted by CC1 and E1.1.2. SC1.1 transitions to Supported.
• Subclaim (SC1.2): The human operator maintains constant veto capability over swarm actions.
• Evidence (E1.2.1): Network architecture simulation guarantees sub-50ms latency for abort commands.
• Defeater (D2): Electronic jamming can sever the network link, removing the human-in-the-loop32.
• Mitigation/Assumption (A1): If the link is lost, the swarm defaults to a deterministic “Return to Base” (RTB) safe mode.
• Evidence (E1.2.2): An RTA monitor using Signal Temporal Logic (STL) continuously calculates the robustness degree of the network link’s heartbeat. If the robustness degree falls below 0.1, the RTA explicitly overrides the main planner and executes RTB. (State: Supported)40.
• Result: D2 is mitigated by A1 and E1.2.2. SC1.2 transitions to Supported.

11. Expected Claim-State Transitions and Ten Invalidating-Change Scenarios

The dynamic nature of the KillWebs.com platform relies on its ability to transition claim states automatically in response to invalidating changes. The following ten scenarios represent critical shifts that immediately degrade the state of the synthetic assurance case:

1. Compiler Toolchain Update: The introduction of a new GCC or LLVM version alters the generated machine code. The change-impact algorithm marks all prior Object Code Verification (OCV) evidence as Stale, transitioning the dependent claims to Suspended pending re-review.
2. STL Monitor Bound Adjustment: Modifying the temporal bounds of an STL constraint (e.g., changing a requirement from “must abort within 2 seconds” to “1.5 seconds”) invalidates prior RTA simulation logs. The specific RTA evidence node becomes Unresolved.
3. Human Operator Interface Redesign: A change in the UI layout invalidates previous HITL cognitive load studies, as muscle memory and visual scanning patterns are disrupted. The human-factors evidence transitions to Withdrawn for the current scope.
4. Discovery of a New CVE in a Base Image: A vulnerability identified in the container runtime hosting the central planner invalidates the SLSA Level 3 security assumptions. A defeater is injected, and the top-level claim transitions to Unresolved.
5. Adversarial Tactic Shift: Intelligence indicates a simulated adversary has developed a new spoofing technique not covered in the original STPA hazard log. A novel Defeater is injected to the root node, reducing confidence until mitigated.
6. Loss of ISO/IEC 17025 Accreditation: The third-party lab providing wind-tunnel data for the UAV aerodynamics loses accreditation21. All associated aerodynamic evidence transitions to Suspended, as the source’s competence is no longer verified.
7. Sensor Firmware Patch: An undocumented vendor update to a LIDAR sensor alters its noise profile, contradicting the assumptions made in the sensor-fusion formal proof. The proof’s evidence node is marked as Contradicted.
8. Geospatial Environment Alteration: High-resolution mapping reveals that the designated operational test zone has experienced unexpected urban development, moving the environment outside the previously tested assumptions. The top-level claim transitions to Withdrawn for the current scope.
9. Key Compromise in the Supply Chain: The cryptographic key used to sign the in-toto attestations is revoked. The platform instantly renders all provenance data signed by that key Unresolved, halting deployment.
10. Simplex Fallback Violation: Field telemetry reveals a hardware fault that prevents the Simplex fallback controller from engaging within the required timeframe25. This realizes a catastrophic defeater, transitioning the top-level safety claim to Unresolved.

12. Verification Matrix

The intensity and scope of verification activities required for an assurance case scale with the Software Criticality Index (SwCI) and the Level of Rigor (LOR), adapted from the MIL-STD-882E standard and the Joint Software Systems Safety Engineering Handbook (JSSSEH)59.

13. Release Acceptance Checklist

Prior to transitioning a fictional system model from “Development” to “Approved for Synthetic Deployment” on KillWebs.com, the automated CI/CD pipeline must validate the following comprehensive checklist:

1. Graph Completeness: The top-level claim resolves exclusively to Supported within declared bounds or Supported with qualifications.
2. Defeater Resolution: All identified Defeaters are formally linked to validated refuting evidence or documented as accepted, quantified residual risks within the allowed threshold9.
3. Provenance Verification: 100% of evidence nodes possess cryptographically valid in-toto Verification Summary Attestations meeting SLSA Level 358.
4. Independence Validation: Cryptographic signatures on SwCI 1 and 2 evidence nodes match registered, organizationally independent IV\&V auditor keys compliant with IEEE 1012.
5. Hazard Log Traceability: Every Unsafe Control Action (UCA) identified in the STPA is explicitly mapped to a mitigating Subclaim in the graph.
6. RTA Configuration Match: The Signal Temporal Logic (STL) parameters compiled into the runtime monitor exactly match the parameters verified in the offline model checker.

14. Graph Completeness Does Not Equal Certification

A fundamental tenet of the KillWebs.com laboratory is that a fully resolved, complete assurance graph does not equate to system safety certification. This limitation stems directly from the Open World Assumption and the philosophical limits of eliminative induction7.
An assurance case graph represents an epistemic state—it reflects the sum total of what the engineers and auditors currently know and have anticipated. However, autonomous systems operate in an “open world” characterized by infinite, unpredictable environmental variables and aleatory uncertainty. A complete graph simply means that all identified defeaters have been successfully mitigated or refuted. It cannot guarantee the absence of unidentified defeaters, such as black swan events, emergent adversarial behaviors, or unmodeled physical laws. Therefore, the graph justifies indefeasible confidence based only on the current body of knowledge. It is fundamentally provisional and must remain continuously active to ingest new empirical data, field anomalies, and adversarial countermeasures.

15. Proposed KillWebs.com Lab, API, Accessibility Model, and Test Plan

The KillWebs.com platform operates as a secure, cloud-based public laboratory designed to democratize the evaluation of synthetic assurance cases for high-consequence systems.
API and Data Model: The platform exposes a REST and GraphQL API for interacting with the JSON-LD assurance graphs.

• POST /api/v1/evidence: Ingests in-toto attestations and test logs from external CI/CD runners, updating the provenance metadata of the graph.
• PUT /api/v1/defeater: Allows independent red-teams to programmatically inject defeaters into existing claims, instantly triggering the dependency-propagation algorithm to evaluate the logical soundness of the target branch.
• GET /api/v1/graph/{id}/state: Returns the real-time dynamic state of the assurance case, recalculating the status of all nodes based on active defeaters and evidence staleness.

Accessibility Model and Roles: The platform utilizes a strict Role-Based Access Control (RBAC) model aligned with the IEEE 1012 independence requirements to prevent conflicts of interest.

• Developers hold write access to propose claims and upload evidence.
• IV\&V Auditors hold the exclusive cryptographic authority to transition critical evidence states to Supported.
• Red-Team Analysts are granted broad access to continuously inject counter-claims and defeaters into the graph, fostering adversarial testing.
• Public Viewers (in the context of an unclassified synthetic lab) are granted access to view the read-only DAG to study assurance methodologies and understand the current epistemic confidence in the system.

Test Plan and Execution Engine: The KillWebs.com architecture includes a continuous, event-driven execution engine. When a system model or external dependency changes, the platform dynamically provisions isolated, ephemeral sandboxes (e.g., hardened Kubernetes pods) to execute regression tests. It automatically runs UPPAAL model checkers against updated timed automata to ensure the absence of deadlocks. Concurrently, it executes Python-based Real-Time Analog Monitoring Tool (RTAMT) scripts to re-evaluate STL robustness degrees over synthetic telemetry streams25. If a robustness degree drops below the defined safety threshold during a synthetic run, the associated evidence automatically fails. This failure ripples up the assurance graph via the dependency-propagation model, maintaining a continuously accurate, mathematically rigorous reflection of the autonomous system’s safety posture.

Works cited

1. Structured Assurance Case Metamodel (SACM) - KDM Analytics, https://kdmanalytics.com/publications-resources/standards/structured-assurance-case-metamodel-sacm/
2. About the Structured Assurance Case Metamodel Specification Version 2.2, https://www.omg.org/spec/SACM/2.2/About-SACM
3. Making Modular Assurance Cases Work Using Structured Assurance Case Metamodel (SACM) - ResearchGate, https://www.researchgate.net/publication/371947060_Making_Modular_Assurance_Cases_Work_Using_Structured_Assurance_Case_Metamodel_SACM
4. Structured Assurance Case Metamodel (SACM), v2.1 - Object Management Group (OMG), https://www.omg.org/spec/SACM/2.1/PDF
5. arXiv:2405.15800v1 [cs.AI] 16 May 2024, https://arxiv.org/pdf/2405.15800
6. Assurance Case Arguments in the Large - the CERN LHC Machine Protection System, https://criticalsystemslabs.com/wp-content/uploads/2024/09/Assurance-Case-Arguments-in-the-Large_merged.pdf
7. arXiv:2004.10474v3 [cs.SE] 14 Jan 2021, https://www.csl.sri.com/\~rushby/papers/assurance2-arxiv.pdf
8. Incremental Assurance Through Eliminative Argumentation - Critical Systems Labs, https://criticalsystemslabs.com/wp-content/uploads/2024/09/Incremental-Assurance-Through-EA_merged.pdf
9. Quantifying Confidence in Assurance 2.0 Arguments - arXiv, https://arxiv.org/pdf/2604.00034
10. Assessing Confidence with Assurance 2.0 - Computer Science Laboratory, https://www.csl.sri.com/users/rushby/papers/confidence22.pdf
11. semantica - PyPI, https://pypi.org/project/semantica/
12. Confidential Containers(CoCo) and Supply-chain Levels for Software Artifacts (SLSA), https://confidentialcontainers.org/blog/2025/02/17/confidential-containerscoco-and-supply-chain-levels-for-software-artifacts-slsa/
13. What Is in-toto? Securing the Software Supply Chain End to End | Sbomify, https://sbomify.com/2024/08/14/what-is-in-toto/
14. Understanding Software Provenance Attestation: The Roles of SLSA and in-toto, https://mikael.barbero.tech/blog/post/2023-12-28-slsa-and-in-toto/
15. Software attestations - SLSA.dev, https://slsa.dev/spec/v1.0/attestation-model
16. Mil-STD-882 System Safety Overview | PDF | Risk | Verification And Validation - Scribd, https://www.scribd.com/document/775407598/Understanding-Mil-STD-882-System-Safety
17. EH01-17-00200 MIL-STD-882E Trifold.indd - APT Research, https://www.apt-research.com/wp-content/uploads/2021/04/00-EH01-17-00200-MIL-STD-882E-Trifold.pdf
18. Confidence in Assurance 2.0 Cases | Request PDF - ResearchGate, https://www.researchgate.net/publication/383764781_Confidence_in_Assurance_20_Cases
19. An Investigation of Proposed Techniques for Quantifying Confidence in Assurance Arguments | Request PDF - ResearchGate, https://www.researchgate.net/publication/308874696_An_Investigation_of_Proposed_Techniques_for_Quantifying_Confidence_in_Assurance_Arguments
20. Enhancing Code Understanding for Impact Analysis by Combining Transformers and Program Dependence Graphs - NSF PAR, https://par.nsf.gov/servlets/purl/10554377
21. ISO/IEC 17025 - Certified Lead Auditor, https://gaqm.org/certifications/iso_certifications/iso-iec-17025-cla
22. Spreadsheet Validation for ISO/IEC 17025 | PDF - Scribd, https://www.scribd.com/document/819638839/305790503-Software-validation-applied-to-spreadsheets-used-in-laboratories-working-under-ISOIEC-17025
23. Human-Machine Social Hybrid Intelligence: A Collaborative Decision-Making Framework for Large Model Agent Groups and Human Experts - arXiv, https://arxiv.org/html/2510.24030v1
24. Keeping the human in the loop: are autonomous decisions inevitable? - ResearchGate, https://www.researchgate.net/publication/390391405_Keeping_the_human_in_the_loop_are_autonomous_decisions_inevitable
25. RTAMT- Runtime Robustness Monitors with Application to CPS and Robotics - arXiv, https://arxiv.org/html/2501.18608v1
26. System-Theoretic Process Analysis (STPA) - Emergent Mind, https://www.emergentmind.com/topics/system-theoretic-process-analysis-stpa
27. Risk Analysis Method of Aviation Critical System Based on Bayesian Networks and Empirical Information Fusion - MDPI, https://www.mdpi.com/2079-9292/14/12/2496
28. STPA: A Systems Approach to Process Hazard Analysis - GATE Energy, https://www.gate.energy/the-brainery/stpa
29. Risk Assessment in the Design phase of Maritime Autonomous Ships – A Human-centred approach - SINTEF, https://www.sintef.no/globalassets/project/hfc/documents/hoem-2022-phd-thesis-risk-assessment-in-the-design-phase-of-maritime-autonomous-ships.pdf
30. Risk-Based Control of Autonomous Surface Ships - NTNU, https://assor.folk.ntnu.no/PhD%20Thesis/Thomas%20Johansen%20PhD_thesis_final.pdf
31. Examples of unsafe control actions | Download Table - ResearchGate, https://www.researchgate.net/figure/Examples-of-unsafe-control-actions_tbl1_331278996
32. (PDF) HUMAN-IN-THE-LOOP SYSTEMS FOR ETHICAL AI - ResearchGate, https://www.researchgate.net/publication/393802734_HUMAN-IN-THE-LOOP_SYSTEMS_FOR_ETHICAL_AI
33. Distributed Consensus Network: A Modularized Communication Framework and Reliability Probabilistic Analysis - arXiv, https://arxiv.org/html/2502.12069v1
34. Distributed Consensus Network: A Modularized Communication Framework and Reliability Probabilistic Analysis - arXiv, https://arxiv.org/pdf/2502.12069
35. [1606.01387] Formal Verification of Multi-Paxos for Distributed Consensus - arXiv, https://arxiv.org/abs/1606.01387
36. Features | UPPAAL, https://uppaal.org/features/
37. Formal Verification of Collision Avoidance for Nonlinear Autonomous Vehicle Models, https://www.es.mdu.se/pdf_publications/6224.pdf
38. Signal Temporal Logic (STL) - Emergent Mind, https://www.emergentmind.com/topics/signal-temporal-logic-stl
39. Ro-To-Go! Robust Reactive Control with Signal Temporal Logic - arXiv, https://arxiv.org/html/2503.05792v1
40. Runtime Assurance from Signal Temporal Logic Safety Specifications - Sam Coogan, https://coogan.ece.gatech.edu/papers/pdf/baird2023acc.pdf
41. REDriver: Runtime Enforcement for Autonomous Vehicles - arXiv, https://arxiv.org/pdf/2401.02253
42. ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems - arXiv, https://arxiv.org/pdf/2511.02164
43. Real-Time HW and Human-in-the-Loop Simulations for the Validation of Detect and Avoid Advanced Functionalities in ATM Future Scenarios | Semantic Scholar, https://www.semanticscholar.org/paper/Real-Time-HW-and-Human-in-the-Loop-Simulations-for-Corraro-Bove/51afad5bf5c0e69966a9055af05971df3f1a1e1a
44. FAA Human-Systems Integration Branch (ANG-E5B) 2005-Human-in-the-Loop Simulation, https://hf.tc.faa.gov/publications/2005-human-in-the-loop-simulation/
45. Human-AI interaction in safety-critical network infrastructures - PMC - NIH, https://pmc.ncbi.nlm.nih.gov/articles/PMC12454906/
46. Teammates Instead of Tools: The Impacts of Level of Autonomy on Mission Performance and Human–Agent Teaming Dynamics in Multi-Agent Distributed Teams - Frontiers, https://www.frontiersin.org/journals/robotics-and-ai/articles/10.3389/frobt.2022.782134/full
47. Novel Human-in-the-Loop (HIL) Simulation Method to Study Synthetic Agents and Standardize Human–Machine Teams (HMT) - MDPI, https://www.mdpi.com/2076-3417/10/23/8390
48. Rapid Verification and Validation of Strategic Autonomous Algorithms Using Human-in-the-Loop Architectures, https://www.aa.washington.edu/sites/aa/files/research/afsl/publications/lum_journal_human_in_the_loop_2009.pdf
49. Humans in the Loop - wp0 | Vanderbilt University, https://wp0.vanderbilt.edu/lawreview/wp-content/uploads/sites/278/2023/03/Humans-in-the-Loop.pdf
50. Information Technology Project Management Policy Effective Date - Radford University, https://www.radford.edu/policies/_documents/information-technology-project-management.pdf
51. IEEE Standard for System, Software, and Hardware Verification and Validation - GitHub, https://raw.githubusercontent.com/Orthant/IEEE/master/1012-2016.pdf
52. 11 July 2022 National Institute of Standards and Technology (NIST) U.S. Department of Commerce 100 Bureau Drive Gaithersburg, MD - IEEE-USA, https://ieeeusa.org/assets/public-policy/policy-log/2022/071122.pdf
53. HOW SHOULD WE REGULATE AI? - IEEE-USA, https://ieeeusa.org/assets/public-policy/committees/aipc/How-Should-We-Regulate-AI.pdf
54. ISO/IEC 17025 Software Test Laboratory Accreditation Testing - Eurolab, https://www.testinglab.com/isoiec-17025-software-test-laboratory-accreditation-testing
55. SLSA Framework: The Definitive Guide for Securing Your Software Supply Chain, https://www.practical-devsecops.com/slsa-framework-guide-software-supply-chain-security/
56. In-depth Look at Achieving SLSA Level-3 Compliance - Harness, https://www.harness.io/blog/an-in-depth-look-at-achieving-slsa-level-3-compliance-with-harness
57. in-toto and SLSA, https://slsa.dev/blog/2023/05/in-toto-and-slsa
58. Verification Summary Attestation (VSA) - SLSA.dev, https://slsa.dev/spec/v1.2-rc2/verification_summary
59. MIL-STD-882E - LDRA, https://ldra.com/882e/
60. 17803 Software Safety Functionality Hazard Assessment - NDIA Conference Proceedings, https://ndia.dtic.mil/wp-content/uploads/2015/system/17803_Whitford.pdf
61. Artifact Provenance and Attestations: From SLSA to in-toto | Secure Pipelines, https://secure-pipelines.com/ci-cd-security/artifact-provenance-attestations-slsa-in-toto/
62. Whitepaper: Safe AI. How is this possible? - Fraunhofer-Institut für Kognitive Systeme IKS, https://www.iks.fraunhofer.de/content/dam/iks/documents/whitepaper-safeai.pdf