Dependable AI-Assisted Engineering: A Formal Framework for AI Participation and Assurance in Safety-Critical Workflows

Puxue Tan

cs.CVOct 2, 2026

Dependable AI-Assisted Engineering: A Formal Framework for AI Participation and Assurance in Safety-Critical Workflows

Authors: Puxue Tan

Organizations: School of Mechanical and Aerospace Engineering Queen’s University Belfast 50 Malone Road, Belfast, UK

Abstract

Generative AI can produce engineering artefacts, but generation alone does not determine whether or how those artefacts should enter safety-critical workflows. This paper develops a formal framework for assigning AI participation and assurance at the level of individual workflow units. Each unit has a participation and assurance record covering its engineering requirement, an approved operational formalization where applicable, the applicable mechanism, fallback where applicable, evidence obligations and the applicable guarantee, plus a deployment-readiness status. The framework distinguishes deterministic verification, statistically calibrated admission, authorized human judgement supported by AI advice, authorized human adjudication of AI-produced artefacts, retained deterministic tool paths and explicit non-participation; these arrangements carry different kinds of guarantee rather than levels on a common scale. The framework also separates formalization fidelity from verifier soundness, provides a staged classification and readiness procedure, and derives conditions for comparing a gated AI-assisted unit with an incumbent process under recurring-population assumptions. We instantiate and apply the framework in an executed 17-unit wing-spar structural-analysis workflow combining deterministically gated AI-generated CAD, retained deterministic computation and human judgement. The AI-generated CAD program passed all 23 deterministic checks and was admitted at the first attempt. Favourable stress magnitudes did not suffice to pass the stress criteria where the predeclared mesh-convergence evidence was insufficient; those criteria were instead referred to engineering judgement. The case demonstrates selective AI participation and explicit evidence handling at unit level; no claim is made of workflow-level dependability, certification, structural safety or productivity.

Figures & tables

Figure 3.1: Overview of the workflow-unit participation and assurance framework. Regime classification, assurance evidence and deployment readiness are distinct; the regimes carry different guarantee kinds and are not ordered on a scalar assurance scale. Stage 1 (Section 4.2 ) assigns Type D, Type E or C[assist], or passes the unit to Stage 2, which selects the admission rule for units whose deliverable AI may produce. The record box shows the fields of Definition 6 (* where applicable) together with the record’s readiness status. Under a READY record, the prescribed mechanism produces, admits or authorizes the deliverable, or a declared fallback produces it; under a NOT READY record (dashed outline), the existing non-AI process produces it (Definition 15 ). PASS denotes a favourable study outcome label (Section 5.6 ), which readiness does not imply.

Figure 5.1: Executed workflow and regime allocation. AI-generated CAD (Type A) enters only through a deterministic gate (ADMIT/REJECT) with a predeclared bounded fallback; meshing, deck handling, solution, extraction and evaluation use deterministic tools (Type D). Residual CAD adequacy and criteria formalization are C[adjudicate]; adequacy and interpretation judgements are C[assist]. Representative units are shown; the executed set comprises 17 units (A 1, D 6, C[adjudicate] 4, C[assist] 6; no B or E), all READY. Dotted outlines mark mechanisms, not workflow units. The predeclared fallback allowed at most three attempts through a bounded repair loop, then engineer-authored CAD through the same gate, then a recorded halt; it was not invoked.

Workflow unit	AI role in this execution	Regime	Acceptance / execution mechanism
CAD program generation	AI generated the program	A	Deterministic gate measures the produced geometry against an approved operational formalization; admission only if every clause is met; declared fallback
Residual CAD adequacy	AI-generated geometry under review; AI compiled evidence	C[adjudicate]	Study author accepts or rejects the artefact on aspects outside the formalized scope
Mesh generation	None	D	Scripted mesher with frozen quality rules
Solver input-deck generation	None	D	Deterministic deck writer and separate deterministic deck checker
Finite-element solution	None	D	Pinned solver within a declared validity domain
Result extraction and numerical checks	None	D	Deterministic parsers, equilibrium checks, convergence metrics

Table 5.1: Representative workflow units of the wing-spar workflow and their regimes.

Stage	Control / evidence	Observed outcome
CAD gate (Type A)	Bounded execution under containment monitoring; 23 geometric and validity checks against the approved formalization; predeclared fallback	ADMIT at attempt 1; 23/23 checks; no containment violations detected; fallback unused; candidate unmodified a
Mesh	Lineage check to gate-admitted geometry; frozen quality rules; geometry-conformity check; repeated meshing	3 levels of quadratic triangular shell elements (3,218 / 12,152 / 47,046 elements); all pass; same-host canonical hashes identical
Solver input decks	Separate deterministic deck checker; regeneration comparison	21/21 pass; byte-identical regeneration
Solver	Pinned binary hash; completion and error/warning record	21/21 complete; no errors or warnings recorded
Numerical integrity	Precision-aware force and moment equilibrium; output-consistency conditions	12/12 linear static jobs pass; all conditions satisfied
Frozen inputs	Hash manifest and solver pin re-verified after the run	61/61 manifest entries and solver binary unchanged (contemporaneous report; later re-hash: Supplement S1.5)

Table 5.2: Execution and integrity evidence.

Figure 5.2: Mesh-convergence evidence under the frozen rule. (a) Medium-to-fine relative change of the tip displacement

\delta_{tip}

, the smallest positive buckling factors

\lambda_{+,\min}

and

\lambda_{-,\min}

, and the web, flange (

\sigma_{proj}

) and stiffener stress metrics (“S1” in the figure denotes the group-maximum stress rule of the frozen engineering plans; Supplement S5.1), divided by the frozen tolerance (1 % for displacement and buckling factors, 5 % for the stress metrics; dashed line: tolerance). Hatched bars and bold values exceed the tolerance (NOT_CONVERGED): the flange project metric

\sigma_{proj}

(25.9 %) and the stiffener stress (16.4 %). (b) Stresses at positive ultimate load versus mesh level (3,218 / 12,152 / 47,046 elements): raw flange root-corner maximum (255.1 / 299.3 / 340.2 MPa), flange project metric

\sigma_{proj}

(medium 182.6, fine 246.5 MPa), stiffener and web peaks, the nominal root reference (171.3 MPa) and

F_{ty}

= 469 MPa; bold labels mark NOT_CONVERGED quantities. The post-hoc interior-flange diagnostic is not plotted and was not a verdict input. Full values: Supplement S5.

Clause	Evaluator verdict	Final disposition
Q-1+ / Q-1 $-$ — stress at limit load (positive / negative)	NOT_CONVERGED	ADJUDICATE
Q-2+ / Q-2 $-$ — stress at ultimate load (positive / negative)	NOT_CONVERGED	ADJUDICATE
Q-3+ / Q-3 $-$ — linear buckling (positive / negative)	PASS	PASS
Q-4 — tip deflection (reporting only)	REPORTED	Not applicable
Q-5 — linear vs geometrically nonlinear diagnostic	SUPPORTED	ADJUDICATE (predeclared)

Table 5.3: Clause verdicts and final dispositions.

Regime	Decision or execution locus	Evidence and governance focus
A	Deterministic verifier against an approved formalization	Approval of the formalization; evidence for verifier soundness; governance of admission and fallback; versioning of verifier and formalization
B	Calibrated statistical gate	Declared recurring population; fixed generator version; reference labels; calibration assumptions; monitoring and recalibration after material change
C[adjudicate]	Authorized human acceptance or rejection of an AI-produced artefact	Identified, authorized adjudicator; recorded acceptance, rationale and AI provenance
C[assist]	Authorized human judgement, with AI material as labelled advice	Identified, authorized person producing the judgement or deliverable; recorded rationale and provenance of AI advisory material
D	Established deterministic tool path	Stated validation evidence; operation within the declared validity domain
E	Non-AI execution	Governance as in the non-AI activity; record that no AI artefact contributed

Table 6.1: Decision or execution locus and evidence/governance focus by regime.

Appendix figures & tables4 assets

Supplementary material from the paper’s appendix.

Appendix

#	Workflow unit	AI role in this execution	Regime
T1	Geometry specification	AI-originated baseline values; adopted by the study author	C[adjudicate]
T2a	CAD program generation	AI generated the program	A
T2b	Residual CAD adequacy	AI-generated geometry under review; AI compiled evidence	C[adjudicate]
T3a	Meshing	None	D
T3b	Discretization adequacy	Advisory: AI compiled evidence and proposed findings	C[assist]
T4a	Deck generation and checking	None	D

Appendix

Table 8

#	Mechanism	Fallback (where relevant)	Readiness
T1	Study author adopts the specification	Author re-specifies geometry	READY
T2a	Deterministic geometric gate (S3)	$\leq$ 3 attempts via bounded repair loop $\rightarrow$ engineer-authored CAD through the same gate $\rightarrow$ halt	READY
T2b	Study author accepts or rejects	Reject $\rightarrow$ T2a fallback path	READY
T3a	Scripted mesher: input lineage check, frozen quality rules, conformity check	Halt	READY
T3b	Study author judges adequacy	Further refinement, if decided	READY
T4a	Deterministic deck writer + independent deck checker	Halt	READY

Appendix

Table 9

Clause	Family	Condition (abridged)
E-1	Execution	Exit code 0 within a 120 s budget
E-2	Execution	Exactly one STEP file, with the declared name
U-1	Units	STEP declares metre as its single length unit
U-2	Units	After calibrated metre import, X span = 2.400 m $\pm$ 1 $\times$ 10 -6 m
V-1	Validity	Fresh-process re-import yields a non-empty shape
V-2	Validity	BRep validity of the compound and every face

Appendix

Table 10

Judgement	Regime	Decision
Residual CAD adequacy	C[adjudicate]	The study author judged the admitted geometry adequate for the study and accepted it with limitations. Defensive code branches unnecessary in the pinned environment were recorded rather than edited, because the predeclared protocol allowed modification only through the repair loop.
Formalization of acceptance criteria	C[adjudicate]	The study author approved the criteria (S5.1) before any result.
Discretization adequacy	C[assist]	The study author accepted the three-level study with limitations. Tip displacement, buckling factors and the web stress converged; flange $\sigma_{proj}$ and the stiffener did not. No further refinement was made within this study.
Analysis adequacy and Q-5	C[assist]	The study author kept Q-5 at ADJUDICATE per the predeclared rule and judged the NLGEOM moment deficit consistent with $\theta$ 2 /2 (S6.3). It was not used as release-supporting evidence.
Result interpretation	C[assist]	The study author identified the first buckling mode in both senses as a global lateral-torsional mode of the laterally unrestrained cantilever, so the factors depend on the idealization of tip and lateral restraint.
Response to unresolved stress clauses	C[assist]	Recorded as a limitation, with no design change. Model refinement was deferred to a new versioned iteration, and no criterion was changed.

Appendix

Table 11

Explore similar work

Compliance-by-Construction Argument Graphs: Using Generative AI to Produce Evidence-Linked Formal Arguments for Certification-Grade Accountability
Apr 5, 2026Mahyar T. MoghaddamAI Accountability AI Assurance
SDU Software Engineering, Odense, Denmark
The Competence Shadow: Theory and Bounds of AI Assistance in Safety Engineering
Mar 26, 2026Umair SiddiqueHuman Oversight of AI Human-AI Collaboration
Independent Research, Ottawa, ON, Canada
Workflow-Level Design Principles for Trustworthy GenAI in Automotive System Engineering
Feb 23, 2026Chih-Hong Cheng, Brian Hsuan-Cheng Liao, Adam Molin +1LLM Safety Requirements Engineering
Carl von Ossietzky University of Oldenburg, Oldenburg, Germany · DENSO AUTOMOTIVE Deutschland Germany, Eching, Germany

Apr 5, 2026J/K move · Enter open · S save

Compliance-by-Construction Argument Graphs: Using Generative AI to Produce Evidence-Linked Formal Arguments for Certification-Grade Accountability

Mahyar T. Moghaddam

SDU Software Engineering, Odense, Denmark

AI Accountability AI Assurance Evidence-Grounded Generation Computational Argumentation

Open paper AskPDF arXiv

High-stakes decision systems increasingly require structured justification, traceability, and auditability to ensure accountability and regulatory compliance. Formal arguments commonly used in the certification of safety-critical systems provide a mechanism for structuring claims, reasoning, and evidence in a verifiable manner. At the same time, generative artificial intelligence systems are increasingly integrated into decision-support workflows, assisting with drafting explanations, summarizing evidence, and generating recommendations. However, current deployments often rely on language models as loosely constrained assistants, which introduces risks such as hallucinated reasoning, unsupported claims, and weak traceability. This paper proposes a compliance-by-construction architecture that integrates Generative AI (GenAI) with structured formal argument representations. The approach treats each AI-assisted step as a claim that must be supported by verifiable evidence and validated against explicit reasoning constraints before it becomes part of an official decision record. The architecture combines four components: i) a typed Argument Graph representation inspired by assurance-case methods, ii) retrieval-augmented generation (RAG) to draft argument fragments grounded in authoritative evidence, iii) a reasoning and validation kernel enforcing completeness and admissibility constraints, and iv) a provenance ledger aligned with the W3C PROV standard to support auditability. We present a system design and an evaluation strategy based on enforceable invariants and worked examples. The analysis suggests that deterministic validation rules can prevent unsupported claims from entering the decision record while allowing GenAI to accelerate argument construction.

Abstract

Explore similar work

Compliance-by-Construction Argument Graphs: Using Generative AI to Produce Evidence-Linked Formal Arguments for Certification-Grade Accountability

The Competence Shadow: Theory and Bounds of AI Assistance in Safety Engineering

Workflow-Level Design Principles for Trustworthy GenAI in Automotive System Engineering