Formal Decision Traces for Data-Driven Verification and Post- Quantum Attestation in Cyber-Resilient Explainable AI Systems

Formal Decision Traces for Data-Driven Verification and Post- Quantum Attestation in Cyber-Resilient Explainable AI Systems | Research Square window.SnipcartSettings = { analytics: { enabled: false } }; (function() { var accessVector = localStorage.getItem('access_vector') || ''; window.dataLayer = window.dataLayer || []; if (accessVector) { window.dataLayer.push({ user: { profile: { profileInfo: { snid: accessVector } } } }); } })(); (function(w,d,s,l,i){w[l]=w[l]||[];w[l].push({'gtm.start':new Date().getTime(),event:'gtm.js'});var f=d.getElementsByTagName(s)[0],j=d.createElement(s),dl=l!='dataLayer'?'&l='+l:'';j.async=true;j.src='https://www.googletagmanager.com/gtm.js?id='+i+dl;f.parentNode.insertBefore(j,f);})(window,document,'script','dataLayer','GTM-K279D39R'); Browse Preprints In Review Journals COVID-19 Preprints AJE Video Bytes Research Tools Research Promotion AJE Professional Editing AJE Rubriq About Preprint Platform In Review Editorial Policies Our Team Advisory Board Help Center Sign In Submit a Preprint Cite Share Download PDF Method Article Formal Decision Traces for Data-Driven Verification and Post- Quantum Attestation in Cyber-Resilient Explainable AI Systems Tiffany A. Ceasor This is a preprint; it has not been peer reviewed by a journal. https://doi.org/ 10.21203/rs.3.rs-8736256/v1 This work is licensed under a CC BY 4.0 License Status: Posted Version 1 posted You are reading this latest preprint version Abstract As artificial intelligence systems are deployed in complex, interconnected cyber-physical environments—spanning healthcare diagnostics, critical infrastructure management, and autonomous vehicle control—the limitations of traditional explainability methods become increasingly consequential. Post-hoc explanation techniques such as SHAP and LIME describe model behavior but cannot guarantee constraint satisfaction, leaving safety-critical systems vulnerable to adversarial manipulation and providing insufficient assurance for trustworthy AI deployment. This paper presents a theoretical framework and architecture for Formal Decision Traces (FDTs), a data-driven verification approach that integrates Satisfiability Modulo Theories (SMT) solvers with neural language models to produce machine-checkable proof certificates for system outputs, bridging the gap between explainable analytics and formal AI security. We make four contributions: (1) We present a theoretical framework for verified explainability and formally define FDTs as structured verification artifacts, establishing their advantages over attention-based and feature attribution methods for cyber-resilient applications. (2) We analyze the adversarial robustness properties of SMT-verified outputs, providing formal guarantees that constraint-based verification detects any encodable violation—a completeness property that probabilistic guardrails cannot achieve. (3) We propose post-quantum secure attestation using NIST FIPS 204 (ML-DSA) lattice-based signatures, addressing the quantum threat to long-lived verification records in safety-critical domains. (4) We validate the architecture through a proof-of-concept implementation using the Z3 SMT solver across three safety-critical domains (healthcare, SCADA, autonomous vehicles), characterizing verification performance at 2–4 ms per query (N = 100 trials), demonstrating dual-channel cross-validation agreement across 21 test cases, confirming tamper detection across all FDT components, and measuring solver scalability to 500 constraints at sub-2 ms. These results provide empirical evidence that the proposed architecture is computationally feasible for real-time cyber-physical system integration. AI security Explainable analytics Post-quantum systems Cyber resilience Data-driven verification Trustworthy AI Formal verification SMT solvers Cyber-physical systems Safety-critical AI Neurosymbolic systems Machine learning security 1 Introduction The deployment of artificial intelligence in complex, interconnected cyber-physical environments has created unprecedented demand for systems that are simultaneously capable, explainable, and resilient to adversarial manipulation [1, 2]. As AI assumes decision-making responsibility in healthcare diagnostics, critical infrastructure management, and autonomous transportation, stakeholders require assurances that go beyond understanding—they require proof that system outputs satisfy domain-specific safety constraints. Traditional approaches to AI trustworthiness have emphasized post-hoc explainability: techniques such as attention visualization, SHAP values, and counterfactual explanations that describe why a model produced a particular output [3, 4]. Sadeghi et al. [5] provide a comprehensive review of explainable AI methods in healthcare, categorizing approaches into feature-oriented, global, concept, surrogate, local pixel-based, and human-centric methods, and emphasize that model explainability and interpretability are vital for the successful deployment of AI in safety-critical clinical practice. However, these methods share a fundamental limitation: they are descriptive rather than normative, explaining what happened without guaranteeing that outputs satisfy specified constraints. This explanatory gap has practical consequences for cyber-resilient systems. Adversarial attacks on neural networks have demonstrated that models can be manipulated to produce incorrect outputs while maintaining plausible explanations [6, 7]. In safety-critical domains, a healthcare AI that explains its diagnostic reasoning may still hallucinate critical findings; an infrastructure management system that visualizes its attention patterns may still recommend actions violating safety constraints. As AI systems are increasingly deployed in interconnected environments where trust, transparency, and resilience are critical, the research community requires methodological innovations that integrate formal verification with machine learning to build secure, interpretable, and sustainable intelligent ecosystems [8]. Satisfiability Modulo Theories (SMT) verification offers a principled foundation for addressing this challenge. SMT solvers determine whether logical formulas are satisfiable under rich background theories including arithmetic, strings, and arrays [9]. When integrated with neural generation, SMT verification provides mathematical guarantees that outputs satisfy encoded constraints, producing machine-checkable proof certificates rather than interpretive explanations [10, 11]. This integration represents a form of data-driven verification: the verification system operates on the actual data produced by AI models, checking each output against formally specified constraints in real time. This paper introduces Formal Decision Traces (FDTs), a verification framework for cyber-resilient explainable AI in safety-critical systems. Unlike traditional explanations, FDTs provide cryptographically attested proof certificates demonstrating constraint satisfaction, enabling distributed verification, tamper detection, and audit trails suitable for high-assurance environments. We further address the implications of quantum computing for verification infrastructure, proposing post-quantum secure attestation mechanisms using NIST-standardized lattice-based signatures to ensure long-term integrity of verification records. Contributions. This paper makes four primary contributions: 1. Theoretical Framework and Formal Specification: We present a theoretical framework for verified explainability and formally define FDTs as structured verification artifacts comprising constraint specifications in SMT-LIB 2.6 format, output encodings, proof certificates, and cryptographic attestations, establishing their theoretical advantages over traditional XAI methods for cyber-resilient applications. 2. Adversarial Robustness Analysis: We analyze the security properties of SMT-verified outputs against semantic adversarial attacks, providing formal guarantees (Theorems 1–2) that constraint-based verification detects any encodable constraint violation, complementing probabilistic guardrail approaches with mathematical completeness. 3. Post-Quantum Security Framework: We examine cryptographic requirements for long-term FDT integrity and propose lattice-based signature schemes (ML-DSA, FIPS 204) for verification attestation that remain secure against quantum adversaries, with hybrid attestation strategies for the classical-to-quantum transition period. 4. Architecture Validation and Performance Characterization: We validate the framework through a proof-of-concept implementation using the Z3 SMT solver with dual-channel cross-validation, characterizing verification performance across three safety-critical domains (healthcare, SCADA, autonomous vehicles) and providing empirical evidence that formal verification adds acceptable latency (2–4 ms) for real-time integration in cyber-physical systems. The remainder of this paper is organized as follows. Section 2 reviews related work in explainable analytics, formal verification, and AI security. Section 3 presents the FDT framework architecture. Section 4 analyzes adversarial robustness properties. Section 5 addresses post-quantum security considerations. Section 6 presents empirical evaluation results. Section 7 discusses limitations and future directions. Section 8 concludes. 2 Related Work 2.1 Explainable Analytics for Safety-Critical AI Explainable AI (XAI) encompasses techniques for making machine learning models interpretable to human users [ 3 ]. Feature attribution methods including LIME [ 12 ], SHAP [ 13 ], and Integrated Gradients [ 14 ] identify input features most influential to predictions. Attention visualization reveals which input tokens neural networks attend to during processing [ 15 ]. Counterfactual explanations describe minimal input changes that would alter predictions [ 16 ]. Sadeghi et al. [ 5 ] provide an extensive systematic review of XAI in healthcare, identifying six methodological categories and emphasizing that black-box AI applications in high-stakes decision-making situations have increased the demand for transparency and explainability since wrong predictions may have severe consequences. Their analysis demonstrates that while XAI methods have advanced significantly, current approaches remain fundamentally post-hoc descriptions of model behavior. Rudin [ 17 ] argues that explanations of black-box models are fundamentally unreliable and advocates for inherently interpretable models. Our work takes a complementary approach: rather than replacing neural models with interpretable alternatives, we augment neural generation with formal verification that proves constraint satisfaction regardless of model interpretability, providing a form of data-driven verification that operates directly on model outputs. 2.2 Formal Verification for Machine Learning Formal verification techniques have been applied to neural networks primarily for robustness certification against adversarial perturbations [ 18 , 19 ]. Reluplex [ 20 ] and its successors verify properties of ReLU networks by encoding network behavior as SMT constraints. α,β-CROWN [ 21 ] provides efficient bound propagation for verification. These approaches verify properties of the model itself rather than properties of individual outputs. Recent neurosymbolic systems integrate neural generation with symbolic verification at the output level. The ARc framework demonstrates high soundness rates in natural language formalization through SMT cross-validation [ 22 ]. AWS Automated Reasoning checks provide verification for cloud configuration compliance at production scale [ 23 ]. DeepSeek-Prover-V2 demonstrates strong pass rates on formal theorem proving benchmarks including MiniF2F [ 24 ]. Our work synthesizes these advances into a unified data-driven verification framework emphasizing cyber resilience and post-quantum security for safety-critical domains. 2.3 Adversarial Machine Learning and AI Security Adversarial attacks exploit vulnerabilities in neural networks to cause misclassification or generation of harmful outputs [ 6 , 25 ]. Defense strategies include adversarial training [ 26 ], certified robustness [ 27 ], and input preprocessing [ 28 ]. However, most defenses focus on perceptual adversarial examples (pixel-level perturbations) rather than semantic adversarial attacks that preserve surface plausibility while violating domain constraints. Guardrail systems including LlamaGuard [ 29 ], R²-Guard [ 30 ], and GuardReasoner [ 31 ] provide content filtering for language models. R²-Guard employs knowledge-enhanced logical reasoning with Markov logic networks for improved defense against jailbreak attacks [ 30 ]. GuardReasoner guides guard models to learn explicit reasoning, with the GuardReasoner 8B model surpassing GPT-4o with chain-of-thought by 5.74% and LLaMA Guard 3 8B by 20.84% average F1 score across 13 benchmarks [ 31 ]. However, these systems operate probabilistically, creating residual risk of adversarial bypass. Our constraint-based verification approach provides deterministic guarantees for encodable constraints, complementing probabilistic defenses with mathematical completeness. 2.4 Post-Quantum Intelligence and Cryptographic Security Quantum computers pose existential threats to widely deployed cryptographic schemes including RSA and elliptic curve cryptography [ 32 ]. Post-quantum cryptography encompasses algorithms believed resistant to quantum attack, including lattice-based, hash-based, and code-based schemes [ 33 ]. NIST has standardized several post-quantum algorithms including ML-KEM (FIPS 203) for key encapsulation and ML-DSA (FIPS 204) for digital signatures [ 34 ]. The intersection of post-quantum security and AI verification has received limited attention. Long-lived verification records—audit trails, compliance documentation, liability evidence in healthcare and critical infrastructure—must remain tamper-evident for years or decades, potentially spanning the advent of cryptographically relevant quantum computers. Our work addresses this gap by proposing post-quantum attestation mechanisms for FDT integrity, contributing to the emerging field of post-quantum intelligence: the design of AI systems whose security guarantees remain valid in a post-quantum computational landscape. 3 Formal Decision Trace Framework 3.1 System Architecture The FDT framework interposes an SMT verification layer between neural generation and output delivery. Let G denote a neural generator (e.g., a large language model), V denote an SMT verifier, and Φ denote a constraint specification encoding domain requirements. For input query x, the framework computes: 1. Generation: y ← G(x) produces candidate output 2. Encoding: ŷ ← E(y) translates output to formal representation 3. Verification: (r, π) ← V(ŷ, Φ) checks constraints and produces proof 4. Decision: If r = SAT, return (y, FDT(Φ, ŷ, r, π)); else regenerate or reject The key innovation is that successful verification produces not merely a binary accept/reject decision but a structured proof artifact—the Formal Decision Trace—that can be independently verified, stored for audit, and cryptographically attested. This constitutes a data-driven verification approach: each AI output is verified against formally specified constraints using the actual data produced by the model, rather than verifying abstract model properties. 3.2 FDT Structure Definition 1 (Formal Decision Trace). A Formal Decision Trace is a tuple FDT = (C, O, R, P, A, M) where: C (Constraint Specification): SMT-LIB 2.6 encoding of policy constraints Φ, enabling solver-agnostic verification O (Output Encoding): Formal representation ŷ of verified output with domain-specific variable bindings R (Verification Result): SAT or UNSAT with satisfying assignment or unsatisfiable core P (Proof Certificate): Machine-checkable proof from SMT solver with per-constraint satisfaction status A (Attestation): Cryptographic signature over H(C ‖ O ‖ R ‖ P ‖ M) for tamper detection M (Metadata): Timestamp, solver version, verification duration, cross-validation status, system identifier 3.3 Comparison with Traditional Explainable Analytics Table 1. Comparison of Formal Decision Traces with Traditional Explainable Analytics Methods Dimension Attention [15] SHAP/LIME [12, 13] Counterfactual [16] FDT (Ours) Output type Visualization Feature scores Alternatives Proof certificate Guarantee level None Statistical None Mathematical (SMT) Verifiability Subjective Approximate Subjective Machine-checkable Tamper evidence None None None Cryptographic (SHA-256/ML-DSA) Reproducibility Model-dependent Stochastic Search-dependent Deterministic Adversarial resilience Vulnerable Vulnerable Vulnerable Complete for encoded Φ The fundamental distinction is epistemological: traditional XAI methods describe model behavior, while FDTs prove constraint satisfaction. This distinction is particularly consequential in cyber-physical systems where adversaries may craft inputs specifically to exploit the gap between explanation and guarantee. 4 Adversarial Robustness Analysis 4.1 Threat Model We consider adversaries targeting AI systems in safety-critical cyber-physical environments who seek to cause constraint-violating outputs while evading detection. The adversary may: (1) craft inputs designed to trigger constraint-violating outputs from the neural generator; (2) manipulate intermediate representations or model weights in compromised deployments; or (3) attempt to forge or modify verification artifacts post-generation. We assume the SMT solver and cryptographic primitives are correctly implemented—standard assumptions in formal verification and security research respectively. 4.2 Formal Robustness Properties Theorem 1 (Constraint Satisfaction Guarantee). For any input x and constraint specification Φ, if the FDT framework returns output y with verification result SAT, then the formal encoding ŷ of y satisfies Φ, assuming correct solver implementation. Proof By construction, the verification step computes (r, π) ← V(ŷ, Φ). When r = SAT, the SMT solver has determined that there exists an assignment to all variables in ŷ such that all constraints in Φ evaluate to true. The proof certificate π provides machine-checkable evidence of this satisfiability determination. By the soundness property of SMT solving [ 9 ], if a solver returns SAT, then the formula is indeed satisfiable. Therefore, ŷ ⪇ Φ. □ Theorem 2 (Tamper Detection). Any modification to an attested FDT = (C, O, R, P, A, M) is detectable with probability 1 − ε, where ε is the signature scheme’s forgery probability (negligible for secure schemes, e.g., ε < 2⁻¹²⁸ for 128-bit security). Proof The attestation A = Sign(sk, H(C ‖ O ‖ R ‖ P ‖ M)) is computed over the concatenation of all FDT components. By the EUF-CMA security of the signature scheme [ 35 ], an adversary without the signing key cannot produce a valid signature on any message not previously signed, except with negligible probability ε. Therefore, any modification to any component of an attested FDT produces a verification failure. □ Corollary 1 (Defense-in-Depth). The FDT framework provides three independent and complementary layers of cyber resilience: (1) generation-time defense, where constraint violations are detected and rejected before output delivery; (2) storage-time defense, where attestations detect tampering with verification records; and (3) audit-time defense, where proof certificates enable independent re-verification of historical claims without trusting the original verifier. 4.3 Comparison with Probabilistic Guardrails Table 2 Security Properties: Constraint-Based Verification vs. Probabilistic Guardrails Property Probabilistic Guardrails [ 29 – 31 ] FDT Verification (Ours) Completeness Partial (learned patterns) Complete for encoded Φ False negatives Possible (novel attacks) None for encoded constraints Transparency Limited (model-dependent) Full (machine-checkable proof) Adversarial robustness Degraded under attack Invariant (constraint-based) Auditability Non-reproducible Deterministic, cryptographically attested FDT verification is complete for encoded constraints: any output violating an encoded constraint is rejected. The complementary limitation is that constraints must be explicitly encoded; unanticipated violations not captured in Φ are not detected. Defense-in-depth combining FDTs with probabilistic guardrails addresses both dimensions of the AI security challenge. 5 Post-Quantum Security Considerations 5.1 Quantum Threat to Verification Infrastructure Cryptographically relevant quantum computers (CRQCs) threaten the long-term integrity of verification records in safety-critical domains. Shor’s algorithm [ 32 ] enables quantum computers to efficiently break RSA and elliptic curve cryptography. Consider a healthcare AI system generating diagnostic recommendations with 20-year liability exposure. Verification records created today using ECDSA signatures could be forged by a CRQC operational within that period, undermining the evidentiary value of the entire audit trail. This “harvest-now, decrypt-later” threat is particularly acute for FDTs, where the integrity of historical verification records may be critical for liability, compliance, and forensic analysis. 5.2 Post-Quantum Attestation Design We propose lattice-based signatures for FDT attestation, specifically ML-DSA (Module-Lattice-Based Digital Signature Algorithm) as standardized by NIST in FIPS 204 [ 34 ]. ML-DSA provides quantum resistance based on the Module Learning With Errors (MLWE) problem, FIPS 204 standardization ensuring regulatory acceptance, and practical performance suitable for real-time verification applications. Definition 2 (Post-Quantum FDT Attestation). A post-quantum attested FDT replaces the classical attestation A with A_PQ = ML-DSA.Sign(sk, H(C ‖ O ‖ R ‖ P ‖ M)), where sk is the signer’s ML-DSA private key and H is a collision-resistant hash function (SHA-3 recommended for quantum resistance margin). 5.3 Hybrid Attestation for Transition Period During the transition to post-quantum cryptography, we recommend hybrid attestation combining classical and post-quantum signatures: A_hybrid = (ECDSA.Sign(sk_c, H(C ‖ O ‖ R ‖ P ‖ M)), ML-DSA.Sign(sk_pq, H(C ‖ O ‖ R ‖ P ‖ M))). This provides backward compatibility with classical-only verifiers, forward security against quantum attacks, and defense against potential weaknesses in post-quantum schemes. 5.4 Performance Characteristics Table 3 ML-DSA Signature Scheme Parameters (from NIST FIPS 204 [ 34 ]) Scheme Private Key (bytes) Public Key (bytes) Signature (bytes) NIST Category ML-DSA-44 2,560 1,312 2,420 Category 2 ML-DSA-65 4,032 1,952 3,309 Category 3 ML-DSA-87 4,896 2,592 4,627 Category 5 ECDSA P-256 32 64 64 Classical ~ 128-bit The increased signature size for post-quantum schemes (2.4–4.6 KB vs. 64 bytes for ECDSA) is negligible relative to typical FDT sizes, which include constraint specifications and proof certificates ranging from tens to hundreds of kilobytes. 6 Empirical Evaluation 6.1 Published Verification Benchmarks To contextualize our empirical results, Table 4 summarizes published benchmarks from production and research neurosymbolic verification systems. Table 4 Published Neurosymbolic Verification Benchmarks System Domain Reported Result Reference ARc NL formalization SMT cross-validation for soundness [ 22 ] AWS AR Checks Cloud configuration Production deployment at scale [ 23 ] GuardReasoner 8B Safety guardrails + 20.84% F1 vs LlamaGuard 3 8B [ 31 ] 6.2 Proof-of-Concept Implementation To validate the FDT pipeline architecture and characterize its performance empirically, we implemented a proof-of-concept in Python (approximately 300 lines) using the Z3 SMT solver [ 36 ] with Python boolean cross-validation. The implementation executes the complete generate–encode–verify–attest pipeline described in Section 3.1 across three safety-critical domains: healthcare medication safety (QF_LIA logic: dosage range constraints, frequency bounds, renal-dose interaction implications, contraindication checks), critical infrastructure SCADA access control (QF_LIA logic: role authorization, clearance thresholds, shift verification, dual-authorization requirements), and autonomous vehicle safety (QF_LRA logic: speed limit compliance, following distance requirements, obstacle-brake implications, lane position validity). Constraint specifications are encoded in SMT-LIB 2.6 standard format [ 37 ] and verified through the Z3 Python API. The proof-of-concept uses simulated generator outputs (deterministic dictionaries) rather than a live neural model, deliberately isolating the verification and attestation components for performance characterization. SHA-256 content hashing serves as a structural placeholder for ML-DSA attestation, preserving the attestation architecture described in Section 5 while deferring post-quantum cryptographic integration to future work. This experimental design enables precise measurement of verification latency without confounding factors from neural model inference time or output parsing. Four experiments evaluate: (1) end-to-end pipeline performance with Z3 verification, (2) constraint violation detection with dual-channel cross-validation, (3) attestation tamper detection, and (4) Z3 solver scalability. 6.3 Experiment 1: Pipeline Performance (Table 5 ) Table 5 reports end-to-end pipeline performance, averaged over 100 independent trials per domain. Verify time measures the complete Z3 verification step: solver instantiation, variable declaration with type coercion, constraint assertion, solver.check() invocation, and Python boolean cross-validation. Total time additionally includes output encoding and SHA-256 attestation. Table 5 End-to-End FDT Pipeline Performance with Z3 SMT Solver (N = 100 trials per domain) Domain Result N(c) Verify (ms) Total (ms) Healthcare (Medication Safety) SAT 4 3.67 ± 0.67 3.83 ± 0.70 Critical Infrastructure (SCADA) SAT 4 2.87 ± 0.40 3.00 ± 0.41 Autonomous Vehicle (Safety) SAT 4 2.28 ± 0.58 2.42 ± 0.60 Z3 verification completes in 2–4 ms across all domains, with total pipeline latency under 4 ms. Healthcare verification is slowest (3.67 ms) due to the implication constraint encoding renal-dose interaction (eGFR < 30 → dosage ≤ 1000 mg), which requires additional solver reasoning over integer arithmetic. Autonomous vehicle verification is fastest (2.28 ms) despite using real-valued arithmetic (QF_LRA), likely due to simpler constraint structure. These empirical results confirm that SMT verification adds acceptable overhead for real-time AI pipeline integration in cyber-physical systems. 6.4 Experiment 2: Violation Detection with Cross-Validation (Table 6 ) Table 6 reports constraint violation detection across 21 test cases: 8 compliant scenarios (including 4 boundary conditions testing constraint edges) and 13 violation scenarios spanning all three domains. Each test case is verified through dual-channel cross-validation: the Z3 SMT solver and an independent Python boolean evaluation must produce identical results, or execution halts with a RuntimeError. This cross-validation mechanism is specifically designed to detect constraint encoding errors—discrepancies between the Z3 constraint formulation and the intended domain semantics. Table 6 Constraint Violation Detection with Z3/Python Cross-Validation (21 test cases) Category Domain Cases Z3 Result Python Result Agreement Compliant (incl. boundary) Healthcare 4 4 SAT 4 SAT 4/4 Compliant (incl. boundary) Infrastructure 2 2 SAT 2 SAT 2/2 Compliant (incl. boundary) Autonomous 2 2 SAT 2 SAT 2/2 Violation Healthcare 4 4 UNSAT 4 UNSAT 4/4 Violation Infrastructure 4 4 UNSAT 4 UNSAT 4/4 Violation Autonomous 5 5 UNSAT 5 UNSAT 5/5 Total All domains 21 21/21 21/21 21/21 (100%) The Z3 solver and Python boolean evaluation agree on all 21 cases. The substantive empirical finding is this dual-channel agreement: it validates that the Z3 constraint encodings constructed via the Z3 Python API are faithful translations of the SMT-LIB 2.6 specifications and the domain-specific safety requirements. A disagreement would indicate a constraint encoding error—the cross-validation mechanism is designed to detect exactly such errors. We note that 100% agreement is expected for deterministic constraint evaluation over designed test cases; this result validates implementation correctness and constraint encoding fidelity, not generalization to arbitrary unseen inputs. 6.5 Experiment 3: Tamper Detection (Table 7 ) Table 7 evaluates the attestation integrity mechanism (Theorem 2 ) across six scenarios, each targeting a different FDT component. An unmodified control FDT is created, then five independent tampering attacks each modify a single component: the verification result (R), the output data (O), the constraint specification (C), the proof certificate (P), and the attestation hash itself (A). Tamper detection recomputes the SHA-256 content hash and compares it to the stored attestation. Table 7 Attestation Tamper Detection: Component-Level Attack Results Attack Scenario Targeted Component Detection Result Unmodified FDT (control) None Verified ✓ Result tampered: SAT → UNSAT R (Verification Result) Detected ✓ Output tampered: dosage 500 → 5000 O (Output Encoding) Detected ✓ Constraint tampered: threshold 250 → 0 C (Constraint Spec) Detected ✓ Proof tampered: satisfied → false P (Proof Certificate) Detected ✓ Hash bit flip (single character) A (Attestation) Detected ✓ All five tampering attacks are detected, and the unmodified control case correctly verifies. This empirically validates the attestation mechanism from Theorem 2 functioning end-to-end within the FDT structure. The result follows from the collision resistance of SHA-256: any modification to any FDT component produces a different content hash that no longer matches the stored attestation. In production deployment, ML-DSA signatures (Section 5 ) would provide the same integrity guarantee with additional non-repudiation and quantum resistance properties. 6.6 Experiment 4: Z3 Solver Scalability (Table 8 ) Table 8 isolates Z3 solver decision time from construction overhead to characterize how verification scales with constraint complexity. For each constraint level, Boolean variables are declared and asserted prior to timing; only the solver.check() call is measured. This differs from Table 5 , where verify time includes solver instantiation, variable declaration, and constraint assertion—explaining why Table 5 reports 2–4 ms for 4 domain-specific constraints while Table 8 reports 0.42 ms for 5 propositional constraints. The difference (approximately 2–3 ms) represents Z3 construction overhead, which is approximately constant regardless of constraint count. Table 8 Z3 SMT Solver Scalability: Decision Time vs. Constraint Count (N = 100 trials per level) Constraints Mean (ms) Std (ms) Min (ms) Max (ms) 5 0.42 0.15 0.33 1.40 10 0.45 0.12 0.34 1.11 25 0.57 0.16 0.43 1.36 50 0.68 0.13 0.55 1.26 100 0.82 0.12 0.70 1.37 200 0.97 0.15 0.85 1.76 500 1.42 0.21 1.27 2.55 Z3 decision time scales approximately linearly from 0.42 ms at 5 constraints to 1.42 ms at 500 constraints, remaining under 2 ms throughout. Combined with the approximately 2–3 ms construction overhead observed in Table 5 , total verification time for 500 propositional constraints would be approximately 4–5 ms. At 100 constraints—a realistic scale for domain-specific safety specifications in cyber-physical systems—decision time is 0.82 ms. These measurements use propositional Boolean constraints; the domain-specific constraints in Table 5 use richer theories (QF_LIA with implications, QF_LRA with real arithmetic) requiring additional solver reasoning. Performance with complex constraint interactions at higher scales remains to be characterized, though published Z3 benchmarks indicate sub-second performance for problems with thousands of variables in standard theories [ 36 ]. 6.7 Summary of Empirical Evidence Taken together, the four experiments provide empirical evidence supporting the following claims: (1) The FDT pipeline is implementable and performant, with Z3 verification adding 2–4 ms of latency across three distinct safety-critical domains (Table 5 ). (2) The dual-channel cross-validation mechanism confirms constraint encoding fidelity between Z3 and independent boolean evaluation across 21 test cases spanning compliant, boundary, and violation scenarios (Table 6 ). (3) The attestation mechanism from Theorem 2 functions correctly, detecting tampering at every FDT component level (Table 7 ). (4) Z3 solver decision time scales approximately linearly to 500 constraints at sub-2 ms, confirming that formal verification is computationally feasible for real-time cyber-physical system integration (Table 8 ). 7 Discussion 7.1 Limitations Constraint completeness. No finite constraint set captures all requirements for open-ended domains. FDTs verify encoded constraints, not unencodable requirements. This fundamental limitation mirrors the specification problem in formal methods generally. Defense-in-depth combining FDTs with probabilistic guardrails and human oversight addresses this limitation in practice. Encoding fidelity. Translation from natural language policies to formal constraints may introduce semantic gaps—a challenge identified broadly in the XAI literature [ 5 ]. The dual-channel cross-validation in our proof-of-concept demonstrates one approach to detecting encoding errors, but does not address the harder problem of ensuring constraints capture the intended policy completely. Proof-of-concept scope. The experimental evaluation uses simulated generator outputs with deterministic constraint specifications, deliberately isolating the verification pipeline for performance characterization. Production deployment would integrate live neural model outputs, introducing additional considerations including output parsing robustness, constraint evolution management, and solver timeout handling for complex constraint interactions. The scalability experiment uses propositional Boolean constraints; performance with richer SMT theories at scale remains to be characterized in deployment contexts. Post-quantum implementation. The proof-of-concept uses SHA-256 content hashing as a structural placeholder for ML-DSA attestation. Full post-quantum implementation requires integration with FIPS 204-compliant libraries, which is engineering work beyond the scope of this framework contribution. 7.2 Future Directions Future work encompasses several directions aligned with advancing cyber-resilient AI: integration with production neural models including large language models and deployment-scale evaluation with live outputs; development of domain-specific constraint libraries for healthcare, critical infrastructure, and autonomous systems based on existing regulatory requirements; differentiable verification integrating verification signals into neural network training loops; federated verification enabling cross-organizational audit and compliance in distributed cyber-physical environments; and empirical comparison with probabilistic guardrails in adversarial settings to quantify the complementary benefits of formal and statistical approaches. 8 Conclusion This paper presented Formal Decision Traces, a data-driven verification framework that provides cyber-resilient explainable analytics for safety-critical AI systems deployed in complex cyber-physical environments. Unlike traditional explanation methods that describe model behavior, FDTs prove constraint satisfaction through machine-checkable certificates with cryptographic attestation, addressing the fundamental gap between interpretability and guarantee that limits current approaches to trustworthy AI. Four contributions advance both theoretical understanding and practical implementation: formal definition of FDTs as structured verification artifacts, adversarial robustness analysis with completeness guarantees for encoded constraints, post-quantum security design using NIST-standardized ML-DSA attestation, and empirical validation through a Z3-based proof-of-concept demonstrating 2–4 ms verification latency across three safety-critical domains with sub-2 ms solver scalability to 500 constraints. As AI systems assume increasing responsibility in healthcare, critical infrastructure, and autonomous systems, formal verification offers a principled path toward systems that are both capable and provably trustworthy—contributing to the broader goal of building secure, interpretable, and resilient intelligent ecosystems. Declarations Funding This research received no external funding. Competing Interests The author declares no competing interests. Ethics Approval Not applicable. This research did not involve human participants or animals. Consent to Participate Not applicable. This research did not involve human participants. Consent to Publish Not applicable. This research did not involve human participants. Data Availability The experimental data reported in Tables 5–8 were generated by executing the proof-of-concept implementation provided as supplementary material (Online Resource 1: fdt_proof_of_concept.py, approximately 300 lines of Python, requiring Python 3.8+ with z3-solver). Raw experimental data are provided as supplementary CSV files (Online Resource 2: table5_pipeline.csv, table6_violations.csv, table7_tamper.csv, table8_scalability.csv). All results are independently reproducible by executing the provided code. The published benchmark results in Table 4 are available from the original sources. The ML-DSA parameters in Table 3 are from NIST FIPS 204, Table 2 [34]. Code Availability The proof-of-concept Python implementation is provided as Online Resource 1. It requires Python 3.8+ with z3-solver and can be executed with: python fdt_proof_of_concept.py. The implementation uses the Z3 SMT solver with Python boolean cross-validation for dual-channel verification. The code is available from the corresponding author upon request and will be deposited in a public repository upon acceptance. Use of AI Writing Assistance The author used Claude (Anthropic), a large language model, to assist with literature synthesis, manuscript drafting, and formatting during the preparation of this work. The author reviewed, edited, and verified all content and takes full responsibility for the integrity and accuracy of the work, including all factual claims, theoretical contributions, and cited sources. All numerical claims were independently verified against primary sources including NIST FIPS 204 and original research publications. All experimental results were generated by executing the proof-of-concept implementation and are independently reproducible. Author Contributions T.A.C. conceived the framework, conducted the literature synthesis, developed the theoretical analysis, implemented the proof-of-concept, designed and executed the experiments, and wrote the manuscript. References Amodei D, Olah C, Steinhardt J et al. (2016) Concrete problems in AI safety. arXiv:1606.06565. Brundage M, Avin S, Clark J et al. (2018) The malicious use of artificial intelligence. arXiv:1802.07228. Arrieta AB, Díaz-Rodríguez N, Del Ser J, et al. Explainable Artificial Intelligence (XAI): concepts, taxonomies, opportunities and challenges toward responsible AI. Inf Fusion. 2020;58:82–115. https://doi.org/10.1016/j.inffus.2019.12.012 . Molnar C. (2022) Interpretable Machine Learning, 2nd edn. https://christophm.github.io/interpretable-ml-book/ Sadeghi Z, Alizadehsani R, Cifci MA, et al. A review of Explainable Artificial Intelligence in healthcare. Comput Electr Eng. 2024;118:109370. https://doi.org/10.1016/j.compeleceng.2024.109370 . Goodfellow IJ, Shlens J, Szegedy C. Explaining and harnessing adversarial examples. In: Proc ICLR; 2015. Carlini N, Wagner D. (2017) Towards evaluating the robustness of neural networks. In: Proc IEEE S&P, pp 39–57. d’Avila Garcez A, Lamb LC. Neurosymbolic AI: the 3rd wave. Artif Intell Rev. 2023;56:12387–406. https://doi.org/10.1007/s10462-023-10448-w . Barrett C, Tinelli C. Satisfiability modulo theories. Handbook of Model Checking. Springer; 2018. pp. 305–43. Marcus G. (2020) The next decade in AI: four steps towards robust artificial intelligence. arXiv:2002.06177. Mao J, Gan C, Kohli P, Tenenbaum JB, Wu J. The neuro-symbolic concept learner: interpreting scenes, words, and sentences from natural supervision. In: Proc ICLR; 2019. Ribeiro MT, Singh S, Guestrin C. (2016) Why should I trust you? explaining the predictions of any classifier. In: Proc KDD, pp 1135–1144. Lundberg SM, Lee SI. (2017) A unified approach to interpreting model predictions. In: Proc NeurIPS, pp 4765–4774. Sundararajan M, Taly A, Yan Q. (2017) Axiomatic attribution for deep networks. In: Proc ICML, pp 3319–3328. Vaswani A, Shazeer N, Parmar N et al. (2017) Attention is all you need. In: Proc NeurIPS, pp 5998–6008. Wachter S, Mittelstadt B, Russell C. Counterfactual explanations without opening the black box. Harv JL Tech. 2018;31:841. Rudin C. Stop explaining black box machine learning models for high stakes decisions and use interpretable models instead. Nat Mach Intell. 2019;1:206–15. https://doi.org/10.1038/s42256-019-0048-x . Liu C, Arnon T, Lazarus C, et al. Algorithms for verifying deep neural networks. Found Trends Optim. 2021;4(3–4):244–404. Huang X, Kwiatkowska M, Wang S, Wu M. (2017) Safety verification of deep neural networks. In: Proc CAV, pp 3–29. Katz G, Barrett C, Dill DL et al. (2017) Reluplex: an efficient SMT solver for verifying deep neural networks. In: Proc CAV, pp 97–117. Wang S, Pei K, Whitehouse J et al. (2018) Efficient formal safety analysis of neural networks. In: Proc NeurIPS, pp 6367–6377. Bayless S et al. (2025) ARc: a neurosymbolic approach to natural language formalization and verification. arXiv:2511.09008. Amazon Web Services. Automated Reasoning checks—a new class of responsible AI capability. AWS Machine Learning Blog; 2025. DeepSeek-AI. (2025) DeepSeek-Prover-V2: advancing formal mathematical reasoning. arXiv. Biggio B, Roli F. Wild patterns: ten years after the rise of adversarial machine learning. Pattern Recognit. 2018;84:317–31. Madry A, Makelov A, Schmidt L, et al. Towards deep learning models resistant to adversarial attacks. In: Proc ICLR; 2018. Cohen J, Rosenfeld E, Kolter Z. (2019) Certified adversarial robustness via randomized smoothing. In: Proc ICML, pp 1310–1320. Guo C, Rana M, Cisse M, van der Maaten L. Countering adversarial images using input transformations. In: Proc ICLR; 2018. Inan H, Upasani K, Chi J et al. (2023) Llama Guard: LLM-based input-output safeguard for human-AI conversations. arXiv:2312.06674. Yuan M, Kang M, Li B. (2025) R²-Guard: robust reasoning enabled LLM guardrail via knowledge-enhanced logical reasoning. In: Proc ICLR. arXiv:2407.05557. Liu Y, Gao H, Zhai S et al. (2025) GuardReasoner: towards reasoning-based LLM safeguards. arXiv:2501.18492. Shor PW. (1994) Algorithms for quantum computation: discrete logarithms and factoring. In: Proc FOCS, pp 124–134. Bernstein DJ, Lange T. Post-quantum cryptography. Nature. 2017;549:188–94. https://doi.org/10.1038/nature23461 . National Institute of Standards and Technology. (2024) Module-Lattice-Based Digital Signature Standard. FIPS 204. https://doi.org/10.6028/NIST.FIPS.204 Goldwasser S, Micali S, Rivest RL. A digital signature scheme secure against adaptive chosen-message attacks. SIAM J Comput. 1988;17(2):281–308. de Moura L, Bjørner N. (2008) Z3: an efficient SMT solver. In: Proc TACAS, pp 337–340. https://doi.org/10.1007/978-3-540-78800-3_24 Barrett C, Fontaine P, Tinelli C. (2021) The SMT-LIB standard: version 2.6. https://smt-lib.org/ Barbosa H et al. (2022) cvc5: a versatile and industrial-strength SMT solver. In: Proc TACAS, pp 415–442. Cimatti A, Griggio A, Schaafsma BJ, Sebastiani R. (2013) The MathSAT5 SMT solver. In: Proc TACAS, pp 93–107. Ducas L, Kiltz E, Lepoint T, et al. CRYSTALS-Dilithium: a lattice-based digital signature scheme. IACR Trans CHES. 2018;2018(1):238–68. Perez F, Ribeiro I. (2023) Ignore this title and HackAPrompt: exposing systemic vulnerabilities of LLMs. In: Proc EMNLP, pp 4945–4977. Additional Declarations No competing interests reported. Supplementary Files table6violations3.csv table7tamper3.csv table8scalability3.csv READMESupplementary2.md table5pipeline3.csv Cite Share Download PDF Status: Posted Version 1 posted You are reading this latest preprint version Research Square lets you share your work early, gain feedback from the community, and start making changes to your manuscript prior to peer review in a journal. As a division of Research Square Company, we’re committed to making research communication faster, fairer, and more useful. We do this by developing innovative software and high quality services for the global research community. Our growing team is made up of researchers and industry professionals working together to solve the most critical problems facing scientific publishing. Also discoverable on Platform About Our Team In Review Editorial Policies Advisory Board Help Center Resources Author Services Accessibility API Access RSS feed Manage Cookie Preferences © Research Square 2026 | ISSN 2693-5015 (online) Privacy Policy Terms of Service Do Not Sell My Personal Information {"props":{"pageProps":{"initialData":{"identity":"rs-8736256","acceptedTermsAndConditions":true,"allowDirectSubmit":true,"archivedVersions":[],"articleType":"Method Article","associatedPublications":[],"authors":[{"id":588973601,"identity":"8c391d4f-1a15-47ed-bd9c-68c11e9f768a","order_by":0,"name":"Tiffany A. Ceasor","email":"data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAZAAAAAyAQMAAABI0h/eAAAABlBMVEX///8AAABVwtN+AAAACXBIWXMAAA7EAAAOxAGVKw4bAAAA3klEQVRIiWNgGAWjYDACZsYHH4CUHIMEsTp4mJkNZwBpYx4JBsYG4rQwQLQk9hCtxZ6dmbHh547D6fulm48//FFzj4Ff+vgFQg5jbOw9czi3R+ZYYjPPsWIGyb6cAgJa+I8/4G0DapHIMWxmYEtgMDjDk0DYlr9th9N5JPI/Nv74R6SWZqAtCTwSOYwNvG0gLewH8Gs5DNQi25Zu2HMjzXA2b18Cj2QPD14dDOz9hxkb37ZZy7PPSH7w8ce3BDl+HvYH+PVAQDPCWiAyIEZLHYrNRNkyCkbBKBgFIwcAAARFQjmit/gfAAAAAElFTkSuQmCC","orcid":"","institution":"Technological Society of Applied Research (TSAR)","correspondingAuthor":true,"prefix":"","firstName":"Tiffany","middleName":"A.","lastName":"Ceasor","suffix":""}],"badges":[],"createdAt":"2026-01-30 02:38:28","currentVersionCode":1,"declarations":"","doi":"10.21203/rs.3.rs-8736256/v1","doiUrl":"https://doi.org/10.21203/rs.3.rs-8736256/v1","draftVersion":[],"editorialEvents":[],"editorialNote":"","failedWorkflow":false,"files":[{"id":108806566,"identity":"86eff938-ede4-40a2-872c-4bfed9490f9e","added_by":"auto","created_at":"2026-05-08 15:28:56","extension":"pdf","order_by":0,"title":"","display":"","copyAsset":false,"role":"manuscript-pdf","size":399405,"visible":true,"origin":"","legend":"","description":"","filename":"manuscript.pdf","url":"https://assets-eu.researchsquare.com/files/rs-8736256/v1/4dec4248-24e7-4551-95b7-c28ee32937a1.pdf"},{"id":102397776,"identity":"9c735e37-98ab-4e76-a276-643eb2b40049","added_by":"auto","created_at":"2026-02-11 10:19:43","extension":"csv","order_by":2,"title":"","display":"","copyAsset":false,"role":"supplement","size":1496,"visible":true,"origin":"","legend":"","description":"","filename":"table6violations3.csv","url":"https://assets-eu.researchsquare.com/files/rs-8736256/v1/41e5caae7c9f7a07893623a0.csv"},{"id":102382445,"identity":"71951f1d-7c18-4815-869f-60546589dcf1","added_by":"auto","created_at":"2026-02-11 07:07:45","extension":"csv","order_by":3,"title":"","display":"","copyAsset":false,"role":"supplement","size":325,"visible":true,"origin":"","legend":"","description":"","filename":"table7tamper3.csv","url":"https://assets-eu.researchsquare.com/files/rs-8736256/v1/41c782cefc3053a66700204e.csv"},{"id":102382443,"identity":"5211c3ba-1376-441a-b4af-72540233ea2b","added_by":"auto","created_at":"2026-02-11 07:07:45","extension":"csv","order_by":4,"title":"","display":"","copyAsset":false,"role":"supplement","size":302,"visible":true,"origin":"","legend":"","description":"","filename":"table8scalability3.csv","url":"https://assets-eu.researchsquare.com/files/rs-8736256/v1/7837066fc6d944ae7672a5c3.csv"},{"id":102398424,"identity":"687f0f90-2c28-400c-9b24-13f659724847","added_by":"auto","created_at":"2026-02-11 10:22:36","extension":"md","order_by":5,"title":"","display":"","copyAsset":false,"role":"supplement","size":1846,"visible":true,"origin":"","legend":"","description":"","filename":"READMESupplementary2.md","url":"https://assets-eu.researchsquare.com/files/rs-8736256/v1/9bffb8b5be49720e69b17470.md"},{"id":102397768,"identity":"7b0ba08a-b00f-48cd-b0db-9ee4ad16ed0d","added_by":"auto","created_at":"2026-02-11 10:19:41","extension":"csv","order_by":5,"title":"","display":"","copyAsset":false,"role":"supplement","size":297,"visible":true,"origin":"","legend":"","description":"","filename":"table5pipeline3.csv","url":"https://assets-eu.researchsquare.com/files/rs-8736256/v1/7f5c0973bf04f394e3eb932b.csv"}],"financialInterests":"No competing interests reported.","formattedTitle":"Formal Decision Traces for Data-Driven Verification and Post- Quantum Attestation in Cyber-Resilient Explainable AI Systems","fulltext":[{"header":"1 Introduction","content":"\u003cp\u003eThe deployment of artificial intelligence in complex, interconnected cyber-physical environments has created unprecedented demand for systems that are simultaneously capable, explainable, and resilient to adversarial manipulation [1, 2]. As AI assumes decision-making responsibility in healthcare diagnostics, critical infrastructure management, and autonomous transportation, stakeholders require assurances that go beyond understanding\u0026mdash;they require proof that system outputs satisfy domain-specific safety constraints. Traditional approaches to AI trustworthiness have emphasized post-hoc explainability: techniques such as attention visualization, SHAP values, and counterfactual explanations that describe why a model produced a particular output [3, 4]. Sadeghi et al. [5] provide a comprehensive review of explainable AI methods in healthcare, categorizing approaches into feature-oriented, global, concept, surrogate, local pixel-based, and human-centric methods, and emphasize that model explainability and interpretability are vital for the successful deployment of AI in safety-critical clinical practice. However, these methods share a fundamental limitation: they are descriptive rather than normative, explaining what happened without guaranteeing that outputs satisfy specified constraints.\u003c/p\u003e\n\u003cp\u003eThis explanatory gap has practical consequences for cyber-resilient systems. Adversarial attacks on neural networks have demonstrated that models can be manipulated to produce incorrect outputs while maintaining plausible explanations [6, 7]. In safety-critical domains, a healthcare AI that explains its diagnostic reasoning may still hallucinate critical findings; an infrastructure management system that visualizes its attention patterns may still recommend actions violating safety constraints. As AI systems are increasingly deployed in interconnected environments where trust, transparency, and resilience are critical, the research community requires methodological innovations that integrate formal verification with machine learning to build secure, interpretable, and sustainable intelligent ecosystems [8].\u003c/p\u003e\n\u003cp\u003eSatisfiability Modulo Theories (SMT) verification offers a principled foundation for addressing this challenge. SMT solvers determine whether logical formulas are satisfiable under rich background theories including arithmetic, strings, and arrays [9]. When integrated with neural generation, SMT verification provides mathematical guarantees that outputs satisfy encoded constraints, producing machine-checkable proof certificates rather than interpretive explanations [10, 11]. This integration represents a form of data-driven verification: the verification system operates on the actual data produced by AI models, checking each output against formally specified constraints in real time.\u003c/p\u003e\n\u003cp\u003eThis paper introduces Formal Decision Traces (FDTs), a verification framework for cyber-resilient explainable AI in safety-critical systems. Unlike traditional explanations, FDTs provide cryptographically attested proof certificates demonstrating constraint satisfaction, enabling distributed verification, tamper detection, and audit trails suitable for high-assurance environments. We further address the implications of quantum computing for verification infrastructure, proposing post-quantum secure attestation mechanisms using NIST-standardized lattice-based signatures to ensure long-term integrity of verification records.\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003eContributions.\u0026nbsp;\u003c/strong\u003eThis paper makes four primary contributions:\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003e1. Theoretical Framework and Formal Specification:\u0026nbsp;\u003c/strong\u003eWe present a theoretical framework for verified explainability and formally define FDTs as structured verification artifacts comprising constraint specifications in SMT-LIB 2.6 format, output encodings, proof certificates, and cryptographic attestations, establishing their theoretical advantages over traditional XAI methods for cyber-resilient applications.\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003e2. Adversarial Robustness Analysis:\u0026nbsp;\u003c/strong\u003eWe analyze the security properties of SMT-verified outputs against semantic adversarial attacks, providing formal guarantees (Theorems 1\u0026ndash;2) that constraint-based verification detects any encodable constraint violation, complementing probabilistic guardrail approaches with mathematical completeness.\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003e3. Post-Quantum Security Framework:\u0026nbsp;\u003c/strong\u003eWe examine cryptographic requirements for long-term FDT integrity and propose lattice-based signature schemes (ML-DSA, FIPS 204) for verification attestation that remain secure against quantum adversaries, with hybrid attestation strategies for the classical-to-quantum transition period.\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003e4. Architecture Validation and Performance Characterization:\u0026nbsp;\u003c/strong\u003eWe validate the framework through a proof-of-concept implementation using the Z3 SMT solver with dual-channel cross-validation, characterizing verification performance across three safety-critical domains (healthcare, SCADA, autonomous vehicles) and providing empirical evidence that formal verification adds acceptable latency (2\u0026ndash;4 ms) for real-time integration in cyber-physical systems.\u003c/p\u003e\n\u003cp\u003eThe remainder of this paper is organized as follows. Section 2 reviews related work in explainable analytics, formal verification, and AI security. Section 3 presents the FDT framework architecture. Section 4 analyzes adversarial robustness properties. Section 5 addresses post-quantum security considerations. Section 6 presents empirical evaluation results. Section 7 discusses limitations and future directions. Section 8 concludes.\u003c/p\u003e"},{"header":"2 Related Work","content":"\u003cdiv id=\"Sec3\" class=\"Section2\"\u003e \u003ch2\u003e2.1 Explainable Analytics for Safety-Critical AI\u003c/h2\u003e \u003cp\u003eExplainable AI (XAI) encompasses techniques for making machine learning models interpretable to human users [\u003cspan citationid=\"CR3\" class=\"CitationRef\"\u003e3\u003c/span\u003e]. Feature attribution methods including LIME [\u003cspan citationid=\"CR12\" class=\"CitationRef\"\u003e12\u003c/span\u003e], SHAP [\u003cspan citationid=\"CR13\" class=\"CitationRef\"\u003e13\u003c/span\u003e], and Integrated Gradients [\u003cspan citationid=\"CR14\" class=\"CitationRef\"\u003e14\u003c/span\u003e] identify input features most influential to predictions. Attention visualization reveals which input tokens neural networks attend to during processing [\u003cspan citationid=\"CR15\" class=\"CitationRef\"\u003e15\u003c/span\u003e]. Counterfactual explanations describe minimal input changes that would alter predictions [\u003cspan citationid=\"CR16\" class=\"CitationRef\"\u003e16\u003c/span\u003e]. Sadeghi et al. [\u003cspan citationid=\"CR5\" class=\"CitationRef\"\u003e5\u003c/span\u003e] provide an extensive systematic review of XAI in healthcare, identifying six methodological categories and emphasizing that black-box AI applications in high-stakes decision-making situations have increased the demand for transparency and explainability since wrong predictions may have severe consequences. Their analysis demonstrates that while XAI methods have advanced significantly, current approaches remain fundamentally post-hoc descriptions of model behavior. Rudin [\u003cspan citationid=\"CR17\" class=\"CitationRef\"\u003e17\u003c/span\u003e] argues that explanations of black-box models are fundamentally unreliable and advocates for inherently interpretable models. Our work takes a complementary approach: rather than replacing neural models with interpretable alternatives, we augment neural generation with formal verification that proves constraint satisfaction regardless of model interpretability, providing a form of data-driven verification that operates directly on model outputs.\u003c/p\u003e \u003c/div\u003e \u003cdiv id=\"Sec4\" class=\"Section2\"\u003e \u003ch2\u003e2.2 Formal Verification for Machine Learning\u003c/h2\u003e \u003cp\u003eFormal verification techniques have been applied to neural networks primarily for robustness certification against adversarial perturbations [\u003cspan citationid=\"CR18\" class=\"CitationRef\"\u003e18\u003c/span\u003e, \u003cspan citationid=\"CR19\" class=\"CitationRef\"\u003e19\u003c/span\u003e]. Reluplex [\u003cspan citationid=\"CR20\" class=\"CitationRef\"\u003e20\u003c/span\u003e] and its successors verify properties of ReLU networks by encoding network behavior as SMT constraints. α,β-CROWN [\u003cspan citationid=\"CR21\" class=\"CitationRef\"\u003e21\u003c/span\u003e] provides efficient bound propagation for verification. These approaches verify properties of the model itself rather than properties of individual outputs. Recent neurosymbolic systems integrate neural generation with symbolic verification at the output level. The ARc framework demonstrates high soundness rates in natural language formalization through SMT cross-validation [\u003cspan citationid=\"CR22\" class=\"CitationRef\"\u003e22\u003c/span\u003e]. AWS Automated Reasoning checks provide verification for cloud configuration compliance at production scale [\u003cspan citationid=\"CR23\" class=\"CitationRef\"\u003e23\u003c/span\u003e]. DeepSeek-Prover-V2 demonstrates strong pass rates on formal theorem proving benchmarks including MiniF2F [\u003cspan citationid=\"CR24\" class=\"CitationRef\"\u003e24\u003c/span\u003e]. Our work synthesizes these advances into a unified data-driven verification framework emphasizing cyber resilience and post-quantum security for safety-critical domains.\u003c/p\u003e \u003c/div\u003e \u003cdiv id=\"Sec5\" class=\"Section2\"\u003e \u003ch2\u003e2.3 Adversarial Machine Learning and AI Security\u003c/h2\u003e \u003cp\u003eAdversarial attacks exploit vulnerabilities in neural networks to cause misclassification or generation of harmful outputs [\u003cspan citationid=\"CR6\" class=\"CitationRef\"\u003e6\u003c/span\u003e, \u003cspan citationid=\"CR25\" class=\"CitationRef\"\u003e25\u003c/span\u003e]. Defense strategies include adversarial training [\u003cspan citationid=\"CR26\" class=\"CitationRef\"\u003e26\u003c/span\u003e], certified robustness [\u003cspan citationid=\"CR27\" class=\"CitationRef\"\u003e27\u003c/span\u003e], and input preprocessing [\u003cspan citationid=\"CR28\" class=\"CitationRef\"\u003e28\u003c/span\u003e]. However, most defenses focus on perceptual adversarial examples (pixel-level perturbations) rather than semantic adversarial attacks that preserve surface plausibility while violating domain constraints. Guardrail systems including LlamaGuard [\u003cspan citationid=\"CR29\" class=\"CitationRef\"\u003e29\u003c/span\u003e], R\u0026sup2;-Guard [\u003cspan citationid=\"CR30\" class=\"CitationRef\"\u003e30\u003c/span\u003e], and GuardReasoner [\u003cspan citationid=\"CR31\" class=\"CitationRef\"\u003e31\u003c/span\u003e] provide content filtering for language models. R\u0026sup2;-Guard employs knowledge-enhanced logical reasoning with Markov logic networks for improved defense against jailbreak attacks [\u003cspan citationid=\"CR30\" class=\"CitationRef\"\u003e30\u003c/span\u003e]. GuardReasoner guides guard models to learn explicit reasoning, with the GuardReasoner 8B model surpassing GPT-4o with chain-of-thought by 5.74% and LLaMA Guard 3 8B by 20.84% average F1 score across 13 benchmarks [\u003cspan citationid=\"CR31\" class=\"CitationRef\"\u003e31\u003c/span\u003e]. However, these systems operate probabilistically, creating residual risk of adversarial bypass. Our constraint-based verification approach provides deterministic guarantees for encodable constraints, complementing probabilistic defenses with mathematical completeness.\u003c/p\u003e \u003c/div\u003e \u003cdiv id=\"Sec6\" class=\"Section2\"\u003e \u003ch2\u003e2.4 Post-Quantum Intelligence and Cryptographic Security\u003c/h2\u003e \u003cp\u003eQuantum computers pose existential threats to widely deployed cryptographic schemes including RSA and elliptic curve cryptography [\u003cspan citationid=\"CR32\" class=\"CitationRef\"\u003e32\u003c/span\u003e]. Post-quantum cryptography encompasses algorithms believed resistant to quantum attack, including lattice-based, hash-based, and code-based schemes [\u003cspan citationid=\"CR33\" class=\"CitationRef\"\u003e33\u003c/span\u003e]. NIST has standardized several post-quantum algorithms including ML-KEM (FIPS 203) for key encapsulation and ML-DSA (FIPS 204) for digital signatures [\u003cspan citationid=\"CR34\" class=\"CitationRef\"\u003e34\u003c/span\u003e]. The intersection of post-quantum security and AI verification has received limited attention. Long-lived verification records\u0026mdash;audit trails, compliance documentation, liability evidence in healthcare and critical infrastructure\u0026mdash;must remain tamper-evident for years or decades, potentially spanning the advent of cryptographically relevant quantum computers. Our work addresses this gap by proposing post-quantum attestation mechanisms for FDT integrity, contributing to the emerging field of post-quantum intelligence: the design of AI systems whose security guarantees remain valid in a post-quantum computational landscape.\u003c/p\u003e \u003c/div\u003e"},{"header":"3 Formal Decision Trace Framework","content":"\u003cp\u003e\u003cstrong\u003e3.1 System Architecture\u003c/strong\u003e\u003c/p\u003e\n\u003cp\u003eThe FDT framework interposes an SMT verification layer between neural generation and output delivery. Let G denote a neural generator (e.g., a large language model), V denote an SMT verifier, and \u0026Phi; denote a constraint specification encoding domain requirements. For input query x, the framework computes:\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003e1. Generation:\u0026nbsp;\u003c/strong\u003ey \u0026larr; G(x) produces candidate output\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003e2. Encoding:\u0026nbsp;\u003c/strong\u003eŷ \u0026larr; E(y) translates output to formal representation\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003e3. Verification:\u0026nbsp;\u003c/strong\u003e(r, \u0026pi;) \u0026larr; V(ŷ, \u0026Phi;) checks constraints and produces proof\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003e4. Decision:\u0026nbsp;\u003c/strong\u003eIf r = SAT, return (y, FDT(\u0026Phi;, ŷ, r, \u0026pi;)); else regenerate or reject\u003c/p\u003e\n\u003cp\u003eThe key innovation is that successful verification produces not merely a binary accept/reject decision but a structured proof artifact\u0026mdash;the Formal Decision Trace\u0026mdash;that can be independently verified, stored for audit, and cryptographically attested. This constitutes a data-driven verification approach: each AI output is verified against formally specified constraints using the actual data produced by the model, rather than verifying abstract model properties.\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003e3.2 FDT Structure\u003c/strong\u003e\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003e\u003cem\u003eDefinition 1 (Formal Decision Trace).\u0026nbsp;\u003c/em\u003e\u003c/strong\u003eA Formal Decision Trace is a tuple FDT = (C, O, R, P, A, M) where:\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003eC\u0026nbsp;\u003c/strong\u003e(Constraint Specification): SMT-LIB 2.6 encoding of policy constraints \u0026Phi;, enabling solver-agnostic verification\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003eO\u0026nbsp;\u003c/strong\u003e(Output Encoding): Formal representation ŷ of verified output with domain-specific variable bindings\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003eR\u0026nbsp;\u003c/strong\u003e(Verification Result): SAT or UNSAT with satisfying assignment or unsatisfiable core\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003eP\u0026nbsp;\u003c/strong\u003e(Proof Certificate): Machine-checkable proof from SMT solver with per-constraint satisfaction status\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003eA\u0026nbsp;\u003c/strong\u003e(Attestation): Cryptographic signature over H(C ‖ O ‖ R ‖ P ‖ M) for tamper detection\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003eM\u0026nbsp;\u003c/strong\u003e(Metadata): Timestamp, solver version, verification duration, cross-validation status, system identifier\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003e3.3 Comparison with Traditional Explainable Analytics\u003c/strong\u003e\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003eTable 1.\u0026nbsp;\u003c/strong\u003eComparison of Formal Decision Traces with Traditional Explainable Analytics Methods\u003c/p\u003e\n\u003ctable border=\"1\" cellspacing=\"0\" cellpadding=\"0\" width=\"100%\"\u003e\n \u003ctbody\u003e\n \u003ctr\u003e\n \u003ctd valign=\"top\" style=\"width: 104px;\"\u003e\n \u003cp\u003e\u003cstrong\u003eDimension\u003c/strong\u003e\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 104px;\"\u003e\n \u003cp\u003e\u003cstrong\u003eAttention [15]\u003c/strong\u003e\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 125px;\"\u003e\n \u003cp\u003e\u003cstrong\u003eSHAP/LIME [12, 13]\u003c/strong\u003e\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 125px;\"\u003e\n \u003cp\u003e\u003cstrong\u003eCounterfactual [16]\u003c/strong\u003e\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 166px;\"\u003e\n \u003cp\u003e\u003cstrong\u003eFDT (Ours)\u003c/strong\u003e\u003c/p\u003e\n \u003c/td\u003e\n \u003c/tr\u003e\n \u003ctr\u003e\n \u003ctd valign=\"top\" style=\"width: 104px;\"\u003e\n \u003cp\u003eOutput type\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 104px;\"\u003e\n \u003cp\u003eVisualization\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 125px;\"\u003e\n \u003cp\u003eFeature scores\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 125px;\"\u003e\n \u003cp\u003eAlternatives\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 166px;\"\u003e\n \u003cp\u003eProof certificate\u003c/p\u003e\n \u003c/td\u003e\n \u003c/tr\u003e\n \u003ctr\u003e\n \u003ctd valign=\"top\" style=\"width: 104px;\"\u003e\n \u003cp\u003eGuarantee level\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 104px;\"\u003e\n \u003cp\u003eNone\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 125px;\"\u003e\n \u003cp\u003eStatistical\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 125px;\"\u003e\n \u003cp\u003eNone\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 166px;\"\u003e\n \u003cp\u003eMathematical (SMT)\u003c/p\u003e\n \u003c/td\u003e\n \u003c/tr\u003e\n \u003ctr\u003e\n \u003ctd valign=\"top\" style=\"width: 104px;\"\u003e\n \u003cp\u003eVerifiability\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 104px;\"\u003e\n \u003cp\u003eSubjective\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 125px;\"\u003e\n \u003cp\u003eApproximate\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 125px;\"\u003e\n \u003cp\u003eSubjective\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 166px;\"\u003e\n \u003cp\u003eMachine-checkable\u003c/p\u003e\n \u003c/td\u003e\n \u003c/tr\u003e\n \u003ctr\u003e\n \u003ctd valign=\"top\" style=\"width: 104px;\"\u003e\n \u003cp\u003eTamper evidence\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 104px;\"\u003e\n \u003cp\u003eNone\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 125px;\"\u003e\n \u003cp\u003eNone\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 125px;\"\u003e\n \u003cp\u003eNone\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 166px;\"\u003e\n \u003cp\u003eCryptographic (SHA-256/ML-DSA)\u003c/p\u003e\n \u003c/td\u003e\n \u003c/tr\u003e\n \u003ctr\u003e\n \u003ctd valign=\"top\" style=\"width: 104px;\"\u003e\n \u003cp\u003eReproducibility\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 104px;\"\u003e\n \u003cp\u003eModel-dependent\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 125px;\"\u003e\n \u003cp\u003eStochastic\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 125px;\"\u003e\n \u003cp\u003eSearch-dependent\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 166px;\"\u003e\n \u003cp\u003eDeterministic\u003c/p\u003e\n \u003c/td\u003e\n \u003c/tr\u003e\n \u003ctr\u003e\n \u003ctd valign=\"top\" style=\"width: 104px;\"\u003e\n \u003cp\u003eAdversarial resilience\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 104px;\"\u003e\n \u003cp\u003eVulnerable\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 125px;\"\u003e\n \u003cp\u003eVulnerable\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 125px;\"\u003e\n \u003cp\u003eVulnerable\u003c/p\u003e\n \u003c/td\u003e\n \u003ctd valign=\"top\" style=\"width: 166px;\"\u003e\n \u003cp\u003eComplete for encoded \u0026Phi;\u003c/p\u003e\n \u003c/td\u003e\n \u003c/tr\u003e\n \u003c/tbody\u003e\n\u003c/table\u003e\n\u003cp\u003eThe fundamental distinction is epistemological: traditional XAI methods describe model behavior, while FDTs prove constraint satisfaction. This distinction is particularly consequential in cyber-physical systems where adversaries may craft inputs specifically to exploit the gap between explanation and guarantee.\u003c/p\u003e"},{"header":"4 Adversarial Robustness Analysis","content":"\u003cdiv id=\"Sec12\" class=\"Section2\"\u003e \u003ch2\u003e4.1 Threat Model\u003c/h2\u003e \u003cp\u003eWe consider adversaries targeting AI systems in safety-critical cyber-physical environments who seek to cause constraint-violating outputs while evading detection. The adversary may: (1) craft inputs designed to trigger constraint-violating outputs from the neural generator; (2) manipulate intermediate representations or model weights in compromised deployments; or (3) attempt to forge or modify verification artifacts post-generation. We assume the SMT solver and cryptographic primitives are correctly implemented\u0026mdash;standard assumptions in formal verification and security research respectively.\u003c/p\u003e \u003c/div\u003e \u003cdiv id=\"Sec13\" class=\"Section2\"\u003e \u003ch2\u003e4.2 Formal Robustness Properties\u003c/h2\u003e \u003cp\u003e \u003cstrong\u003eTheorem 1\u003c/strong\u003e \u003cp\u003e \u003cb\u003e(Constraint Satisfaction Guarantee).\u003c/b\u003e For any input x and constraint specification Φ, if the FDT framework returns output y with verification result SAT, then the formal encoding ŷ of y satisfies Φ, assuming correct solver implementation.\u003c/p\u003e \u003c/p\u003e \u003cp\u003e \u003cstrong\u003eProof\u003c/strong\u003e \u003cp\u003eBy construction, the verification step computes (r, π) \u0026larr; V(ŷ, Φ). When r\u0026thinsp;=\u0026thinsp;SAT, the SMT solver has determined that there exists an assignment to all variables in ŷ such that all constraints in Φ evaluate to true. The proof certificate π provides machine-checkable evidence of this satisfiability determination. By the soundness property of SMT solving [\u003cspan citationid=\"CR9\" class=\"CitationRef\"\u003e9\u003c/span\u003e], if a solver returns SAT, then the formula is indeed satisfiable. Therefore, ŷ ⪇ Φ. □\u003c/p\u003e \u003c/p\u003e \u003cp\u003e \u003cstrong\u003eTheorem 2\u003c/strong\u003e \u003cp\u003e \u003cb\u003e(Tamper Detection).\u003c/b\u003e Any modification to an attested FDT = (C, O, R, P, A, M) is detectable with probability 1\u0026thinsp;\u0026minus;\u0026thinsp;ε, where ε is the signature scheme\u0026rsquo;s forgery probability (negligible for secure schemes, e.g., ε\u0026thinsp;\u0026lt;\u0026thinsp;2⁻\u0026sup1;\u0026sup2;⁸ for 128-bit security).\u003c/p\u003e \u003c/p\u003e \u003cp\u003e \u003cstrong\u003eProof\u003c/strong\u003e \u003cp\u003eThe attestation A\u0026thinsp;=\u0026thinsp;Sign(sk, H(C ‖ O ‖ R ‖ P ‖ M)) is computed over the concatenation of all FDT components. By the EUF-CMA security of the signature scheme [\u003cspan citationid=\"CR35\" class=\"CitationRef\"\u003e35\u003c/span\u003e], an adversary without the signing key cannot produce a valid signature on any message not previously signed, except with negligible probability ε. Therefore, any modification to any component of an attested FDT produces a verification failure. □\u003c/p\u003e \u003c/p\u003e \u003cp\u003e \u003cstrong\u003eCorollary 1\u003c/strong\u003e \u003cp\u003e \u003cb\u003e(Defense-in-Depth).\u003c/b\u003e The FDT framework provides three independent and complementary layers of cyber resilience: (1) generation-time defense, where constraint violations are detected and rejected before output delivery; (2) storage-time defense, where attestations detect tampering with verification records; and (3) audit-time defense, where proof certificates enable independent re-verification of historical claims without trusting the original verifier.\u003c/p\u003e \u003c/p\u003e \u003c/div\u003e \u003cdiv id=\"Sec14\" class=\"Section2\"\u003e \u003ch2\u003e4.3 Comparison with Probabilistic Guardrails\u003c/h2\u003e \u003cp\u003e \u003cdiv class=\"gridtable\"\u003e\u003ctable float=\"Yes\" id=\"Tab2\" border=\"1\"\u003e \u003ccaption language=\"En\"\u003e \u003cdiv class=\"CaptionNumber\"\u003eTable 2\u003c/div\u003e \u003cdiv class=\"CaptionContent\"\u003e \u003cp\u003eSecurity Properties: Constraint-Based Verification vs. Probabilistic Guardrails\u003c/p\u003e \u003c/div\u003e \u003c/caption\u003e \u003ccolgroup cols=\"3\"\u003e \u003cdiv align=\"left\" class=\"colspec\" colname=\"c1\" colnum=\"1\"\u003e\u003c/div\u003e \u003cdiv align=\"left\" class=\"colspec\" colname=\"c2\" colnum=\"2\"\u003e\u003c/div\u003e \u003cdiv align=\"left\" class=\"colspec\" colname=\"c3\" colnum=\"3\"\u003e\u003c/div\u003e \u003cthead\u003e \u003ctr\u003e \u003cth align=\"left\" colname=\"c1\"\u003e \u003cp\u003eProperty\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c2\"\u003e \u003cp\u003eProbabilistic Guardrails [\u003cspan additionalcitationids=\"CR30\" citationid=\"CR29\" class=\"CitationRef\"\u003e29\u003c/span\u003e\u0026ndash;\u003cspan citationid=\"CR31\" class=\"CitationRef\"\u003e31\u003c/span\u003e]\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c3\"\u003e \u003cp\u003eFDT Verification (Ours)\u003c/p\u003e \u003c/th\u003e \u003c/tr\u003e \u003c/thead\u003e \u003ctbody\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eCompleteness\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003ePartial (learned patterns)\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c3\"\u003e \u003cp\u003eComplete for encoded Φ\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eFalse negatives\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003ePossible (novel attacks)\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c3\"\u003e \u003cp\u003eNone for encoded constraints\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eTransparency\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eLimited (model-dependent)\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c3\"\u003e \u003cp\u003eFull (machine-checkable proof)\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eAdversarial robustness\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eDegraded under attack\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c3\"\u003e \u003cp\u003eInvariant (constraint-based)\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eAuditability\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eNon-reproducible\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c3\"\u003e \u003cp\u003eDeterministic, cryptographically attested\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003c/tbody\u003e \u003c/colgroup\u003e \u003c/table\u003e\u003c/div\u003e \u003c/p\u003e \u003cp\u003eFDT verification is complete for encoded constraints: any output violating an encoded constraint is rejected. The complementary limitation is that constraints must be explicitly encoded; unanticipated violations not captured in Φ are not detected. Defense-in-depth combining FDTs with probabilistic guardrails addresses both dimensions of the AI security challenge.\u003c/p\u003e \u003c/div\u003e"},{"header":"5 Post-Quantum Security Considerations","content":"\u003cdiv id=\"Sec16\" class=\"Section2\"\u003e \u003ch2\u003e5.1 Quantum Threat to Verification Infrastructure\u003c/h2\u003e \u003cp\u003eCryptographically relevant quantum computers (CRQCs) threaten the long-term integrity of verification records in safety-critical domains. Shor\u0026rsquo;s algorithm [\u003cspan citationid=\"CR32\" class=\"CitationRef\"\u003e32\u003c/span\u003e] enables quantum computers to efficiently break RSA and elliptic curve cryptography. Consider a healthcare AI system generating diagnostic recommendations with 20-year liability exposure. Verification records created today using ECDSA signatures could be forged by a CRQC operational within that period, undermining the evidentiary value of the entire audit trail. This \u0026ldquo;harvest-now, decrypt-later\u0026rdquo; threat is particularly acute for FDTs, where the integrity of historical verification records may be critical for liability, compliance, and forensic analysis.\u003c/p\u003e \u003c/div\u003e \u003cdiv id=\"Sec17\" class=\"Section2\"\u003e \u003ch2\u003e5.2 Post-Quantum Attestation Design\u003c/h2\u003e \u003cp\u003eWe propose lattice-based signatures for FDT attestation, specifically ML-DSA (Module-Lattice-Based Digital Signature Algorithm) as standardized by NIST in FIPS 204 [\u003cspan citationid=\"CR34\" class=\"CitationRef\"\u003e34\u003c/span\u003e]. ML-DSA provides quantum resistance based on the Module Learning With Errors (MLWE) problem, FIPS 204 standardization ensuring regulatory acceptance, and practical performance suitable for real-time verification applications.\u003c/p\u003e \u003cp\u003e \u003cstrong\u003eDefinition 2\u003c/strong\u003e \u003cp\u003e \u003cb\u003e(Post-Quantum FDT Attestation).\u003c/b\u003e A post-quantum attested FDT replaces the classical attestation A with A_PQ\u0026thinsp;=\u0026thinsp;ML-DSA.Sign(sk, H(C ‖ O ‖ R ‖ P ‖ M)), where sk is the signer\u0026rsquo;s ML-DSA private key and H is a collision-resistant hash function (SHA-3 recommended for quantum resistance margin).\u003c/p\u003e \u003c/p\u003e \u003c/div\u003e \u003cdiv id=\"Sec18\" class=\"Section2\"\u003e \u003ch2\u003e5.3 Hybrid Attestation for Transition Period\u003c/h2\u003e \u003cp\u003eDuring the transition to post-quantum cryptography, we recommend hybrid attestation combining classical and post-quantum signatures: A_hybrid = (ECDSA.Sign(sk_c, H(C ‖ O ‖ R ‖ P ‖ M)), ML-DSA.Sign(sk_pq, H(C ‖ O ‖ R ‖ P ‖ M))). This provides backward compatibility with classical-only verifiers, forward security against quantum attacks, and defense against potential weaknesses in post-quantum schemes.\u003c/p\u003e \u003c/div\u003e \u003cdiv id=\"Sec19\" class=\"Section2\"\u003e \u003ch2\u003e5.4 Performance Characteristics\u003c/h2\u003e \u003cp\u003e \u003cdiv class=\"gridtable\"\u003e\u003ctable float=\"Yes\" id=\"Tab3\" border=\"1\"\u003e \u003ccaption language=\"En\"\u003e \u003cdiv class=\"CaptionNumber\"\u003eTable 3\u003c/div\u003e \u003cdiv class=\"CaptionContent\"\u003e \u003cp\u003eML-DSA Signature Scheme Parameters (from NIST FIPS 204 [\u003cspan citationid=\"CR34\" class=\"CitationRef\"\u003e34\u003c/span\u003e])\u003c/p\u003e \u003c/div\u003e \u003c/caption\u003e \u003ccolgroup cols=\"5\"\u003e \u003cdiv align=\"left\" class=\"colspec\" colname=\"c1\" colnum=\"1\"\u003e\u003c/div\u003e \u003cdiv align=\"char\" char=\".\" class=\"colspec\" colname=\"c2\" colnum=\"2\"\u003e\u003c/div\u003e \u003cdiv align=\"char\" char=\".\" class=\"colspec\" colname=\"c3\" colnum=\"3\"\u003e\u003c/div\u003e \u003cdiv align=\"char\" char=\".\" class=\"colspec\" colname=\"c4\" colnum=\"4\"\u003e\u003c/div\u003e \u003cdiv align=\"left\" class=\"colspec\" colname=\"c5\" colnum=\"5\"\u003e\u003c/div\u003e \u003cthead\u003e \u003ctr\u003e \u003cth align=\"left\" colname=\"c1\"\u003e \u003cp\u003eScheme\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c2\"\u003e \u003cp\u003ePrivate Key (bytes)\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c3\"\u003e \u003cp\u003ePublic Key (bytes)\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c4\"\u003e \u003cp\u003eSignature (bytes)\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c5\"\u003e \u003cp\u003eNIST Category\u003c/p\u003e \u003c/th\u003e \u003c/tr\u003e \u003c/thead\u003e \u003ctbody\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eML-DSA-44\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c2\"\u003e \u003cp\u003e2,560\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c3\"\u003e \u003cp\u003e1,312\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c4\"\u003e \u003cp\u003e2,420\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c5\"\u003e \u003cp\u003eCategory 2\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eML-DSA-65\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c2\"\u003e \u003cp\u003e4,032\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c3\"\u003e \u003cp\u003e1,952\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c4\"\u003e \u003cp\u003e3,309\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c5\"\u003e \u003cp\u003eCategory 3\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eML-DSA-87\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c2\"\u003e \u003cp\u003e4,896\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c3\"\u003e \u003cp\u003e2,592\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c4\"\u003e \u003cp\u003e4,627\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c5\"\u003e \u003cp\u003eCategory 5\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eECDSA P-256\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c2\"\u003e \u003cp\u003e32\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c3\"\u003e \u003cp\u003e64\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c4\"\u003e \u003cp\u003e64\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c5\"\u003e \u003cp\u003eClassical\u0026thinsp;~\u0026thinsp;128-bit\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003c/tbody\u003e \u003c/colgroup\u003e \u003c/table\u003e\u003c/div\u003e \u003c/p\u003e \u003cp\u003eThe increased signature size for post-quantum schemes (2.4\u0026ndash;4.6 KB vs. 64 bytes for ECDSA) is negligible relative to typical FDT sizes, which include constraint specifications and proof certificates ranging from tens to hundreds of kilobytes.\u003c/p\u003e \u003c/div\u003e"},{"header":"6 Empirical Evaluation","content":"\u003cdiv id=\"Sec21\" class=\"Section2\"\u003e \u003ch2\u003e6.1 Published Verification Benchmarks\u003c/h2\u003e \u003cp\u003eTo contextualize our empirical results, Table\u0026nbsp;\u003cspan refid=\"Tab4\" class=\"InternalRef\"\u003e4\u003c/span\u003e summarizes published benchmarks from production and research neurosymbolic verification systems.\u003c/p\u003e \u003cp\u003e \u003cdiv class=\"gridtable\"\u003e\u003ctable float=\"Yes\" id=\"Tab4\" border=\"1\"\u003e \u003ccaption language=\"En\"\u003e \u003cdiv class=\"CaptionNumber\"\u003eTable 4\u003c/div\u003e \u003cdiv class=\"CaptionContent\"\u003e \u003cp\u003ePublished Neurosymbolic Verification Benchmarks\u003c/p\u003e \u003c/div\u003e \u003c/caption\u003e \u003ccolgroup cols=\"4\"\u003e \u003cdiv align=\"left\" class=\"colspec\" colname=\"c1\" colnum=\"1\"\u003e\u003c/div\u003e \u003cdiv align=\"left\" class=\"colspec\" colname=\"c2\" colnum=\"2\"\u003e\u003c/div\u003e \u003cdiv align=\"left\" class=\"colspec\" colname=\"c3\" colnum=\"3\"\u003e\u003c/div\u003e \u003cdiv align=\"left\" class=\"colspec\" colname=\"c4\" colnum=\"4\"\u003e\u003c/div\u003e \u003cthead\u003e \u003ctr\u003e \u003cth align=\"left\" colname=\"c1\"\u003e \u003cp\u003eSystem\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c2\"\u003e \u003cp\u003eDomain\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c3\"\u003e \u003cp\u003eReported Result\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c4\"\u003e \u003cp\u003eReference\u003c/p\u003e \u003c/th\u003e \u003c/tr\u003e \u003c/thead\u003e \u003ctbody\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eARc\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eNL formalization\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c3\"\u003e \u003cp\u003eSMT cross-validation for soundness\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c4\"\u003e \u003cp\u003e[\u003cspan citationid=\"CR22\" class=\"CitationRef\"\u003e22\u003c/span\u003e]\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eAWS AR Checks\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eCloud configuration\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c3\"\u003e \u003cp\u003eProduction deployment at scale\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c4\"\u003e \u003cp\u003e[\u003cspan citationid=\"CR23\" class=\"CitationRef\"\u003e23\u003c/span\u003e]\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eGuardReasoner 8B\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eSafety guardrails\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c3\"\u003e \u003cp\u003e+\u0026thinsp;20.84% F1 vs LlamaGuard 3 8B\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c4\"\u003e \u003cp\u003e[\u003cspan citationid=\"CR31\" class=\"CitationRef\"\u003e31\u003c/span\u003e]\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003c/tbody\u003e \u003c/colgroup\u003e \u003c/table\u003e\u003c/div\u003e \u003c/p\u003e \u003c/div\u003e \u003cdiv id=\"Sec22\" class=\"Section2\"\u003e \u003ch2\u003e6.2 Proof-of-Concept Implementation\u003c/h2\u003e \u003cp\u003eTo validate the FDT pipeline architecture and characterize its performance empirically, we implemented a proof-of-concept in Python (approximately 300 lines) using the Z3 SMT solver [\u003cspan citationid=\"CR36\" class=\"CitationRef\"\u003e36\u003c/span\u003e] with Python boolean cross-validation. The implementation executes the complete generate\u0026ndash;encode\u0026ndash;verify\u0026ndash;attest pipeline described in Section \u003cspan refid=\"Sec8\" class=\"InternalRef\"\u003e3.1\u003c/span\u003e across three safety-critical domains: healthcare medication safety (QF_LIA logic: dosage range constraints, frequency bounds, renal-dose interaction implications, contraindication checks), critical infrastructure SCADA access control (QF_LIA logic: role authorization, clearance thresholds, shift verification, dual-authorization requirements), and autonomous vehicle safety (QF_LRA logic: speed limit compliance, following distance requirements, obstacle-brake implications, lane position validity). Constraint specifications are encoded in SMT-LIB 2.6 standard format [\u003cspan citationid=\"CR37\" class=\"CitationRef\"\u003e37\u003c/span\u003e] and verified through the Z3 Python API.\u003c/p\u003e \u003cp\u003eThe proof-of-concept uses simulated generator outputs (deterministic dictionaries) rather than a live neural model, deliberately isolating the verification and attestation components for performance characterization. SHA-256 content hashing serves as a structural placeholder for ML-DSA attestation, preserving the attestation architecture described in Section \u003cspan refid=\"Sec15\" class=\"InternalRef\"\u003e5\u003c/span\u003e while deferring post-quantum cryptographic integration to future work. This experimental design enables precise measurement of verification latency without confounding factors from neural model inference time or output parsing. Four experiments evaluate: (1) end-to-end pipeline performance with Z3 verification, (2) constraint violation detection with dual-channel cross-validation, (3) attestation tamper detection, and (4) Z3 solver scalability.\u003c/p\u003e \u003c/div\u003e \u003cdiv id=\"Sec23\" class=\"Section2\"\u003e \u003ch2\u003e6.3 Experiment 1: Pipeline Performance (Table\u0026nbsp;\u003cspan refid=\"Tab5\" class=\"InternalRef\"\u003e5\u003c/span\u003e)\u003c/h2\u003e \u003cp\u003eTable\u0026nbsp;\u003cspan refid=\"Tab5\" class=\"InternalRef\"\u003e5\u003c/span\u003e reports end-to-end pipeline performance, averaged over 100 independent trials per domain. Verify time measures the complete Z3 verification step: solver instantiation, variable declaration with type coercion, constraint assertion, solver.check() invocation, and Python boolean cross-validation. Total time additionally includes output encoding and SHA-256 attestation.\u003c/p\u003e \u003cp\u003e \u003cdiv class=\"gridtable\"\u003e\u003ctable float=\"Yes\" id=\"Tab5\" border=\"1\"\u003e \u003ccaption language=\"En\"\u003e \u003cdiv class=\"CaptionNumber\"\u003eTable 5\u003c/div\u003e \u003cdiv class=\"CaptionContent\"\u003e \u003cp\u003eEnd-to-End FDT Pipeline Performance with Z3 SMT Solver (N\u0026thinsp;=\u0026thinsp;100 trials per domain)\u003c/p\u003e \u003c/div\u003e \u003c/caption\u003e \u003ccolgroup cols=\"5\"\u003e \u003cdiv align=\"left\" class=\"colspec\" colname=\"c1\" colnum=\"1\"\u003e\u003c/div\u003e \u003cdiv align=\"left\" class=\"colspec\" colname=\"c2\" colnum=\"2\"\u003e\u003c/div\u003e \u003cdiv align=\"char\" char=\".\" class=\"colspec\" colname=\"c3\" colnum=\"3\"\u003e\u003c/div\u003e \u003cdiv align=\"char\" char=\"\u0026plusmn;\" class=\"colspec\" colname=\"c4\" colnum=\"4\"\u003e\u003c/div\u003e \u003cdiv align=\"char\" char=\"\u0026plusmn;\" class=\"colspec\" colname=\"c5\" colnum=\"5\"\u003e\u003c/div\u003e \u003cthead\u003e \u003ctr\u003e \u003cth align=\"left\" colname=\"c1\"\u003e \u003cp\u003eDomain\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c2\"\u003e \u003cp\u003eResult\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c3\"\u003e \u003cp\u003eN(c)\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c4\"\u003e \u003cp\u003eVerify (ms)\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c5\"\u003e \u003cp\u003eTotal (ms)\u003c/p\u003e \u003c/th\u003e \u003c/tr\u003e \u003c/thead\u003e \u003ctbody\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eHealthcare (Medication Safety)\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eSAT\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c3\"\u003e \u003cp\u003e4\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\"\u0026plusmn;\" colname=\"c4\"\u003e \u003cp\u003e3.67\u0026thinsp;\u0026plusmn;\u0026thinsp;0.67\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\"\u0026plusmn;\" colname=\"c5\"\u003e \u003cp\u003e3.83\u0026thinsp;\u0026plusmn;\u0026thinsp;0.70\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eCritical Infrastructure (SCADA)\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eSAT\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c3\"\u003e \u003cp\u003e4\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\"\u0026plusmn;\" colname=\"c4\"\u003e \u003cp\u003e2.87\u0026thinsp;\u0026plusmn;\u0026thinsp;0.40\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\"\u0026plusmn;\" colname=\"c5\"\u003e \u003cp\u003e3.00\u0026thinsp;\u0026plusmn;\u0026thinsp;0.41\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eAutonomous Vehicle (Safety)\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eSAT\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c3\"\u003e \u003cp\u003e4\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\"\u0026plusmn;\" colname=\"c4\"\u003e \u003cp\u003e2.28\u0026thinsp;\u0026plusmn;\u0026thinsp;0.58\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\"\u0026plusmn;\" colname=\"c5\"\u003e \u003cp\u003e2.42\u0026thinsp;\u0026plusmn;\u0026thinsp;0.60\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003c/tbody\u003e \u003c/colgroup\u003e \u003c/table\u003e\u003c/div\u003e \u003c/p\u003e \u003cp\u003eZ3 verification completes in 2\u0026ndash;4 ms across all domains, with total pipeline latency under 4 ms. Healthcare verification is slowest (3.67 ms) due to the implication constraint encoding renal-dose interaction (eGFR\u0026thinsp;\u0026lt;\u0026thinsp;30 \u0026rarr; dosage\u0026thinsp;\u0026le;\u0026thinsp;1000 mg), which requires additional solver reasoning over integer arithmetic. Autonomous vehicle verification is fastest (2.28 ms) despite using real-valued arithmetic (QF_LRA), likely due to simpler constraint structure. These empirical results confirm that SMT verification adds acceptable overhead for real-time AI pipeline integration in cyber-physical systems.\u003c/p\u003e \u003c/div\u003e \u003cdiv id=\"Sec24\" class=\"Section2\"\u003e \u003ch2\u003e6.4 Experiment 2: Violation Detection with Cross-Validation (Table\u0026nbsp;\u003cspan refid=\"Tab6\" class=\"InternalRef\"\u003e6\u003c/span\u003e)\u003c/h2\u003e \u003cp\u003eTable\u0026nbsp;\u003cspan refid=\"Tab6\" class=\"InternalRef\"\u003e6\u003c/span\u003e reports constraint violation detection across 21 test cases: 8 compliant scenarios (including 4 boundary conditions testing constraint edges) and 13 violation scenarios spanning all three domains. Each test case is verified through dual-channel cross-validation: the Z3 SMT solver and an independent Python boolean evaluation must produce identical results, or execution halts with a RuntimeError. This cross-validation mechanism is specifically designed to detect constraint encoding errors\u0026mdash;discrepancies between the Z3 constraint formulation and the intended domain semantics.\u003c/p\u003e \u003cp\u003e \u003cdiv class=\"gridtable\"\u003e\u003ctable float=\"Yes\" id=\"Tab6\" border=\"1\"\u003e \u003ccaption language=\"En\"\u003e \u003cdiv class=\"CaptionNumber\"\u003eTable 6\u003c/div\u003e \u003cdiv class=\"CaptionContent\"\u003e \u003cp\u003eConstraint Violation Detection with Z3/Python Cross-Validation (21 test cases)\u003c/p\u003e \u003c/div\u003e \u003c/caption\u003e \u003ccolgroup cols=\"6\"\u003e \u003cdiv align=\"left\" class=\"colspec\" colname=\"c1\" colnum=\"1\"\u003e\u003c/div\u003e \u003cdiv align=\"left\" class=\"colspec\" colname=\"c2\" colnum=\"2\"\u003e\u003c/div\u003e \u003cdiv align=\"char\" char=\".\" class=\"colspec\" colname=\"c3\" colnum=\"3\"\u003e\u003c/div\u003e \u003cdiv align=\"left\" class=\"colspec\" colname=\"c4\" colnum=\"4\"\u003e\u003c/div\u003e \u003cdiv align=\"left\" class=\"colspec\" colname=\"c5\" colnum=\"5\"\u003e\u003c/div\u003e \u003cdiv align=\"left\" class=\"colspec\" colname=\"c6\" colnum=\"6\"\u003e\u003c/div\u003e \u003cthead\u003e \u003ctr\u003e \u003cth align=\"left\" colname=\"c1\"\u003e \u003cp\u003eCategory\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c2\"\u003e \u003cp\u003eDomain\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c3\"\u003e \u003cp\u003eCases\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c4\"\u003e \u003cp\u003eZ3 Result\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c5\"\u003e \u003cp\u003ePython Result\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c6\"\u003e \u003cp\u003eAgreement\u003c/p\u003e \u003c/th\u003e \u003c/tr\u003e \u003c/thead\u003e \u003ctbody\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eCompliant (incl. boundary)\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eHealthcare\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c3\"\u003e \u003cp\u003e4\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c4\"\u003e \u003cp\u003e4 SAT\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c5\"\u003e \u003cp\u003e4 SAT\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c6\"\u003e \u003cp\u003e4/4\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eCompliant (incl. boundary)\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eInfrastructure\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c3\"\u003e \u003cp\u003e2\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c4\"\u003e \u003cp\u003e2 SAT\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c5\"\u003e \u003cp\u003e2 SAT\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c6\"\u003e \u003cp\u003e2/2\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eCompliant (incl. boundary)\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eAutonomous\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c3\"\u003e \u003cp\u003e2\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c4\"\u003e \u003cp\u003e2 SAT\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c5\"\u003e \u003cp\u003e2 SAT\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c6\"\u003e \u003cp\u003e2/2\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eViolation\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eHealthcare\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c3\"\u003e \u003cp\u003e4\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c4\"\u003e \u003cp\u003e4 UNSAT\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c5\"\u003e \u003cp\u003e4 UNSAT\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c6\"\u003e \u003cp\u003e4/4\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eViolation\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eInfrastructure\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c3\"\u003e \u003cp\u003e4\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c4\"\u003e \u003cp\u003e4 UNSAT\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c5\"\u003e \u003cp\u003e4 UNSAT\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c6\"\u003e \u003cp\u003e4/4\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eViolation\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eAutonomous\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c3\"\u003e \u003cp\u003e5\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c4\"\u003e \u003cp\u003e5 UNSAT\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c5\"\u003e \u003cp\u003e5 UNSAT\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c6\"\u003e \u003cp\u003e5/5\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eTotal\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eAll domains\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c3\"\u003e \u003cp\u003e21\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c4\"\u003e \u003cp\u003e21/21\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c5\"\u003e \u003cp\u003e21/21\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c6\"\u003e \u003cp\u003e21/21 (100%)\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003c/tbody\u003e \u003c/colgroup\u003e \u003c/table\u003e\u003c/div\u003e \u003c/p\u003e \u003cp\u003eThe Z3 solver and Python boolean evaluation agree on all 21 cases. The substantive empirical finding is this dual-channel agreement: it validates that the Z3 constraint encodings constructed via the Z3 Python API are faithful translations of the SMT-LIB 2.6 specifications and the domain-specific safety requirements. A disagreement would indicate a constraint encoding error\u0026mdash;the cross-validation mechanism is designed to detect exactly such errors. We note that 100% agreement is expected for deterministic constraint evaluation over designed test cases; this result validates implementation correctness and constraint encoding fidelity, not generalization to arbitrary unseen inputs.\u003c/p\u003e \u003c/div\u003e \u003cdiv id=\"Sec25\" class=\"Section2\"\u003e \u003ch2\u003e6.5 Experiment 3: Tamper Detection (Table\u0026nbsp;\u003cspan refid=\"Tab7\" class=\"InternalRef\"\u003e7\u003c/span\u003e)\u003c/h2\u003e \u003cp\u003eTable\u0026nbsp;\u003cspan refid=\"Tab7\" class=\"InternalRef\"\u003e7\u003c/span\u003e evaluates the attestation integrity mechanism (Theorem \u003cspan refid=\"FPar4\" class=\"InternalRef\"\u003e2\u003c/span\u003e) across six scenarios, each targeting a different FDT component. An unmodified control FDT is created, then five independent tampering attacks each modify a single component: the verification result (R), the output data (O), the constraint specification (C), the proof certificate (P), and the attestation hash itself (A). Tamper detection recomputes the SHA-256 content hash and compares it to the stored attestation.\u003c/p\u003e \u003cp\u003e \u003cdiv class=\"gridtable\"\u003e\u003ctable float=\"Yes\" id=\"Tab7\" border=\"1\"\u003e \u003ccaption language=\"En\"\u003e \u003cdiv class=\"CaptionNumber\"\u003eTable 7\u003c/div\u003e \u003cdiv class=\"CaptionContent\"\u003e \u003cp\u003eAttestation Tamper Detection: Component-Level Attack Results\u003c/p\u003e \u003c/div\u003e \u003c/caption\u003e \u003ccolgroup cols=\"3\"\u003e \u003cdiv align=\"left\" class=\"colspec\" colname=\"c1\" colnum=\"1\"\u003e\u003c/div\u003e \u003cdiv align=\"left\" class=\"colspec\" colname=\"c2\" colnum=\"2\"\u003e\u003c/div\u003e \u003cdiv align=\"left\" class=\"colspec\" colname=\"c3\" colnum=\"3\"\u003e\u003c/div\u003e \u003cthead\u003e \u003ctr\u003e \u003cth align=\"left\" colname=\"c1\"\u003e \u003cp\u003eAttack Scenario\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c2\"\u003e \u003cp\u003eTargeted Component\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c3\"\u003e \u003cp\u003eDetection Result\u003c/p\u003e \u003c/th\u003e \u003c/tr\u003e \u003c/thead\u003e \u003ctbody\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eUnmodified FDT (control)\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eNone\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c3\"\u003e \u003cp\u003eVerified ✓\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eResult tampered: SAT \u0026rarr; UNSAT\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eR (Verification Result)\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c3\"\u003e \u003cp\u003eDetected ✓\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eOutput tampered: dosage 500 \u0026rarr; 5000\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eO (Output Encoding)\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c3\"\u003e \u003cp\u003eDetected ✓\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eConstraint tampered: threshold 250 \u0026rarr; 0\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eC (Constraint Spec)\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c3\"\u003e \u003cp\u003eDetected ✓\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eProof tampered: satisfied \u0026rarr; false\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eP (Proof Certificate)\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c3\"\u003e \u003cp\u003eDetected ✓\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003eHash bit flip (single character)\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c2\"\u003e \u003cp\u003eA (Attestation)\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"left\" colname=\"c3\"\u003e \u003cp\u003eDetected ✓\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003c/tbody\u003e \u003c/colgroup\u003e \u003c/table\u003e\u003c/div\u003e \u003c/p\u003e \u003cp\u003eAll five tampering attacks are detected, and the unmodified control case correctly verifies. This empirically validates the attestation mechanism from Theorem \u003cspan refid=\"FPar4\" class=\"InternalRef\"\u003e2\u003c/span\u003e functioning end-to-end within the FDT structure. The result follows from the collision resistance of SHA-256: any modification to any FDT component produces a different content hash that no longer matches the stored attestation. In production deployment, ML-DSA signatures (Section \u003cspan refid=\"Sec15\" class=\"InternalRef\"\u003e5\u003c/span\u003e) would provide the same integrity guarantee with additional non-repudiation and quantum resistance properties.\u003c/p\u003e \u003c/div\u003e \u003cdiv id=\"Sec26\" class=\"Section2\"\u003e \u003ch2\u003e6.6 Experiment 4: Z3 Solver Scalability (Table\u0026nbsp;\u003cspan refid=\"Tab8\" class=\"InternalRef\"\u003e8\u003c/span\u003e)\u003c/h2\u003e \u003cp\u003eTable\u0026nbsp;\u003cspan refid=\"Tab8\" class=\"InternalRef\"\u003e8\u003c/span\u003e isolates Z3 solver decision time from construction overhead to characterize how verification scales with constraint complexity. For each constraint level, Boolean variables are declared and asserted prior to timing; only the solver.check() call is measured. This differs from Table\u0026nbsp;\u003cspan refid=\"Tab5\" class=\"InternalRef\"\u003e5\u003c/span\u003e, where verify time includes solver instantiation, variable declaration, and constraint assertion\u0026mdash;explaining why Table\u0026nbsp;\u003cspan refid=\"Tab5\" class=\"InternalRef\"\u003e5\u003c/span\u003e reports 2\u0026ndash;4 ms for 4 domain-specific constraints while Table\u0026nbsp;\u003cspan refid=\"Tab8\" class=\"InternalRef\"\u003e8\u003c/span\u003e reports 0.42 ms for 5 propositional constraints. The difference (approximately 2\u0026ndash;3 ms) represents Z3 construction overhead, which is approximately constant regardless of constraint count.\u003c/p\u003e \u003cp\u003e \u003cdiv class=\"gridtable\"\u003e\u003ctable float=\"Yes\" id=\"Tab8\" border=\"1\"\u003e \u003ccaption language=\"En\"\u003e \u003cdiv class=\"CaptionNumber\"\u003eTable 8\u003c/div\u003e \u003cdiv class=\"CaptionContent\"\u003e \u003cp\u003eZ3 SMT Solver Scalability: Decision Time vs. Constraint Count (N\u0026thinsp;=\u0026thinsp;100 trials per level)\u003c/p\u003e \u003c/div\u003e \u003c/caption\u003e \u003ccolgroup cols=\"5\"\u003e \u003cdiv align=\"left\" class=\"colspec\" colname=\"c1\" colnum=\"1\"\u003e\u003c/div\u003e \u003cdiv align=\"char\" char=\".\" class=\"colspec\" colname=\"c2\" colnum=\"2\"\u003e\u003c/div\u003e \u003cdiv align=\"char\" char=\".\" class=\"colspec\" colname=\"c3\" colnum=\"3\"\u003e\u003c/div\u003e \u003cdiv align=\"char\" char=\".\" class=\"colspec\" colname=\"c4\" colnum=\"4\"\u003e\u003c/div\u003e \u003cdiv align=\"char\" char=\".\" class=\"colspec\" colname=\"c5\" colnum=\"5\"\u003e\u003c/div\u003e \u003cthead\u003e \u003ctr\u003e \u003cth align=\"left\" colname=\"c1\"\u003e \u003cp\u003eConstraints\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c2\"\u003e \u003cp\u003eMean (ms)\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c3\"\u003e \u003cp\u003eStd (ms)\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c4\"\u003e \u003cp\u003eMin (ms)\u003c/p\u003e \u003c/th\u003e \u003cth align=\"left\" colname=\"c5\"\u003e \u003cp\u003eMax (ms)\u003c/p\u003e \u003c/th\u003e \u003c/tr\u003e \u003c/thead\u003e \u003ctbody\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003e5\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c2\"\u003e \u003cp\u003e0.42\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c3\"\u003e \u003cp\u003e0.15\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c4\"\u003e \u003cp\u003e0.33\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c5\"\u003e \u003cp\u003e1.40\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003e10\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c2\"\u003e \u003cp\u003e0.45\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c3\"\u003e \u003cp\u003e0.12\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c4\"\u003e \u003cp\u003e0.34\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c5\"\u003e \u003cp\u003e1.11\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003e25\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c2\"\u003e \u003cp\u003e0.57\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c3\"\u003e \u003cp\u003e0.16\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c4\"\u003e \u003cp\u003e0.43\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c5\"\u003e \u003cp\u003e1.36\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003e50\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c2\"\u003e \u003cp\u003e0.68\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c3\"\u003e \u003cp\u003e0.13\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c4\"\u003e \u003cp\u003e0.55\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c5\"\u003e \u003cp\u003e1.26\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003e100\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c2\"\u003e \u003cp\u003e0.82\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c3\"\u003e \u003cp\u003e0.12\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c4\"\u003e \u003cp\u003e0.70\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c5\"\u003e \u003cp\u003e1.37\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003e200\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c2\"\u003e \u003cp\u003e0.97\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c3\"\u003e \u003cp\u003e0.15\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c4\"\u003e \u003cp\u003e0.85\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c5\"\u003e \u003cp\u003e1.76\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003ctr\u003e \u003ctd align=\"left\" colname=\"c1\"\u003e \u003cp\u003e500\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c2\"\u003e \u003cp\u003e1.42\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c3\"\u003e \u003cp\u003e0.21\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c4\"\u003e \u003cp\u003e1.27\u003c/p\u003e \u003c/td\u003e \u003ctd align=\"char\" char=\".\" colname=\"c5\"\u003e \u003cp\u003e2.55\u003c/p\u003e \u003c/td\u003e \u003c/tr\u003e \u003c/tbody\u003e \u003c/colgroup\u003e \u003c/table\u003e\u003c/div\u003e \u003c/p\u003e \u003cp\u003eZ3 decision time scales approximately linearly from 0.42 ms at 5 constraints to 1.42 ms at 500 constraints, remaining under 2 ms throughout. Combined with the approximately 2\u0026ndash;3 ms construction overhead observed in Table\u0026nbsp;\u003cspan refid=\"Tab5\" class=\"InternalRef\"\u003e5\u003c/span\u003e, total verification time for 500 propositional constraints would be approximately 4\u0026ndash;5 ms. At 100 constraints\u0026mdash;a realistic scale for domain-specific safety specifications in cyber-physical systems\u0026mdash;decision time is 0.82 ms. These measurements use propositional Boolean constraints; the domain-specific constraints in Table\u0026nbsp;\u003cspan refid=\"Tab5\" class=\"InternalRef\"\u003e5\u003c/span\u003e use richer theories (QF_LIA with implications, QF_LRA with real arithmetic) requiring additional solver reasoning. Performance with complex constraint interactions at higher scales remains to be characterized, though published Z3 benchmarks indicate sub-second performance for problems with thousands of variables in standard theories [\u003cspan citationid=\"CR36\" class=\"CitationRef\"\u003e36\u003c/span\u003e].\u003c/p\u003e \u003c/div\u003e \u003cdiv id=\"Sec27\" class=\"Section2\"\u003e \u003ch2\u003e6.7 Summary of Empirical Evidence\u003c/h2\u003e \u003cp\u003eTaken together, the four experiments provide empirical evidence supporting the following claims: (1) The FDT pipeline is implementable and performant, with Z3 verification adding 2\u0026ndash;4 ms of latency across three distinct safety-critical domains (Table\u0026nbsp;\u003cspan refid=\"Tab5\" class=\"InternalRef\"\u003e5\u003c/span\u003e). (2) The dual-channel cross-validation mechanism confirms constraint encoding fidelity between Z3 and independent boolean evaluation across 21 test cases spanning compliant, boundary, and violation scenarios (Table\u0026nbsp;\u003cspan refid=\"Tab6\" class=\"InternalRef\"\u003e6\u003c/span\u003e). (3) The attestation mechanism from Theorem \u003cspan refid=\"FPar4\" class=\"InternalRef\"\u003e2\u003c/span\u003e functions correctly, detecting tampering at every FDT component level (Table\u0026nbsp;\u003cspan refid=\"Tab7\" class=\"InternalRef\"\u003e7\u003c/span\u003e). (4) Z3 solver decision time scales approximately linearly to 500 constraints at sub-2 ms, confirming that formal verification is computationally feasible for real-time cyber-physical system integration (Table\u0026nbsp;\u003cspan refid=\"Tab8\" class=\"InternalRef\"\u003e8\u003c/span\u003e).\u003c/p\u003e \u003c/div\u003e"},{"header":"7 Discussion","content":"\u003cdiv id=\"Sec29\" class=\"Section2\"\u003e \u003ch2\u003e7.1 Limitations\u003c/h2\u003e \u003cp\u003e \u003cb\u003eConstraint completeness.\u003c/b\u003e No finite constraint set captures all requirements for open-ended domains. FDTs verify encoded constraints, not unencodable requirements. This fundamental limitation mirrors the specification problem in formal methods generally. Defense-in-depth combining FDTs with probabilistic guardrails and human oversight addresses this limitation in practice.\u003c/p\u003e \u003cp\u003e \u003cb\u003eEncoding fidelity.\u003c/b\u003e Translation from natural language policies to formal constraints may introduce semantic gaps\u0026mdash;a challenge identified broadly in the XAI literature [\u003cspan citationid=\"CR5\" class=\"CitationRef\"\u003e5\u003c/span\u003e]. The dual-channel cross-validation in our proof-of-concept demonstrates one approach to detecting encoding errors, but does not address the harder problem of ensuring constraints capture the intended policy completely.\u003c/p\u003e \u003cp\u003e \u003cb\u003eProof-of-concept scope.\u003c/b\u003e The experimental evaluation uses simulated generator outputs with deterministic constraint specifications, deliberately isolating the verification pipeline for performance characterization. Production deployment would integrate live neural model outputs, introducing additional considerations including output parsing robustness, constraint evolution management, and solver timeout handling for complex constraint interactions. The scalability experiment uses propositional Boolean constraints; performance with richer SMT theories at scale remains to be characterized in deployment contexts.\u003c/p\u003e \u003cp\u003e \u003cb\u003ePost-quantum implementation.\u003c/b\u003e The proof-of-concept uses SHA-256 content hashing as a structural placeholder for ML-DSA attestation. Full post-quantum implementation requires integration with FIPS 204-compliant libraries, which is engineering work beyond the scope of this framework contribution.\u003c/p\u003e \u003c/div\u003e \u003cdiv id=\"Sec30\" class=\"Section2\"\u003e \u003ch2\u003e7.2 Future Directions\u003c/h2\u003e \u003cp\u003eFuture work encompasses several directions aligned with advancing cyber-resilient AI: integration with production neural models including large language models and deployment-scale evaluation with live outputs; development of domain-specific constraint libraries for healthcare, critical infrastructure, and autonomous systems based on existing regulatory requirements; differentiable verification integrating verification signals into neural network training loops; federated verification enabling cross-organizational audit and compliance in distributed cyber-physical environments; and empirical comparison with probabilistic guardrails in adversarial settings to quantify the complementary benefits of formal and statistical approaches.\u003c/p\u003e \u003c/div\u003e"},{"header":"8 Conclusion","content":"\u003cp\u003eThis paper presented Formal Decision Traces, a data-driven verification framework that provides cyber-resilient explainable analytics for safety-critical AI systems deployed in complex cyber-physical environments. Unlike traditional explanation methods that describe model behavior, FDTs prove constraint satisfaction through machine-checkable certificates with cryptographic attestation, addressing the fundamental gap between interpretability and guarantee that limits current approaches to trustworthy AI. Four contributions advance both theoretical understanding and practical implementation: formal definition of FDTs as structured verification artifacts, adversarial robustness analysis with completeness guarantees for encoded constraints, post-quantum security design using NIST-standardized ML-DSA attestation, and empirical validation through a Z3-based proof-of-concept demonstrating 2\u0026ndash;4 ms verification latency across three safety-critical domains with sub-2 ms solver scalability to 500 constraints. As AI systems assume increasing responsibility in healthcare, critical infrastructure, and autonomous systems, formal verification offers a principled path toward systems that are both capable and provably trustworthy\u0026mdash;contributing to the broader goal of building secure, interpretable, and resilient intelligent ecosystems.\u003c/p\u003e"},{"header":"Declarations","content":"\u003cp\u003e\u003cstrong\u003eFunding\u0026nbsp;\u003c/strong\u003eThis research received no external funding.\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003eCompeting Interests\u0026nbsp;\u003c/strong\u003eThe author declares no competing interests.\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003eEthics Approval\u0026nbsp;\u003c/strong\u003eNot applicable. This research did not involve human participants or animals.\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003eConsent to Participate\u0026nbsp;\u003c/strong\u003eNot applicable. This research did not involve human participants.\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003eConsent to Publish\u0026nbsp;\u003c/strong\u003eNot applicable. This research did not involve human participants.\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003eData Availability\u0026nbsp;\u003c/strong\u003eThe experimental data reported in Tables 5\u0026ndash;8 were generated by executing the proof-of-concept implementation provided as supplementary material (Online Resource 1: fdt_proof_of_concept.py, approximately 300 lines of Python, requiring Python 3.8+ with z3-solver). Raw experimental data are provided as supplementary CSV files (Online Resource 2: table5_pipeline.csv, table6_violations.csv, table7_tamper.csv, table8_scalability.csv). All results are independently reproducible by executing the provided code. The published benchmark results in Table 4 are available from the original sources. The ML-DSA parameters in Table 3 are from NIST FIPS 204, Table 2 [34].\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003eCode Availability\u0026nbsp;\u003c/strong\u003eThe proof-of-concept Python implementation is provided as Online Resource 1. It requires Python 3.8+ with z3-solver and can be executed with: python fdt_proof_of_concept.py. The implementation uses the Z3 SMT solver with Python boolean cross-validation for dual-channel verification. The code is available from the corresponding author upon request and will be deposited in a public repository upon acceptance.\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003eUse of AI Writing Assistance\u0026nbsp;\u003c/strong\u003eThe author used Claude (Anthropic), a large language model, to assist with literature synthesis, manuscript drafting, and formatting during the preparation of this work. The author reviewed, edited, and verified all content and takes full responsibility for the integrity and accuracy of the work, including all factual claims, theoretical contributions, and cited sources. All numerical claims were independently verified against primary sources including NIST FIPS 204 and original research publications. All experimental results were generated by executing the proof-of-concept implementation and are independently reproducible.\u003c/p\u003e\n\u003cp\u003e\u003cstrong\u003eAuthor Contributions\u0026nbsp;\u003c/strong\u003eT.A.C. conceived the framework, conducted the literature synthesis, developed the theoretical analysis, implemented the proof-of-concept, designed and executed the experiments, and wrote the manuscript.\u003c/p\u003e"},{"header":"References","content":"\u003col\u003e\u003cli\u003e\u003cspan\u003eAmodei D, Olah C, Steinhardt J et al. (2016) Concrete problems in AI safety. arXiv:1606.06565.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eBrundage M, Avin S, Clark J et al. (2018) The malicious use of artificial intelligence. arXiv:1802.07228.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eArrieta AB, D\u0026iacute;az-Rodr\u0026iacute;guez N, Del Ser J, et al. Explainable Artificial Intelligence (XAI): concepts, taxonomies, opportunities and challenges toward responsible AI. Inf Fusion. 2020;58:82\u0026ndash;115. \u003cspan class=\"ExternalRef\"\u003e\u003cspan class=\"RefSource\"\u003ehttps://doi.org/10.1016/j.inffus.2019.12.012\u003c/span\u003e\u003cspan address=\"10.1016/j.inffus.2019.12.012\" targettype=\"DOI\" class=\"RefTarget\"\u003e\u003c/span\u003e\u003c/span\u003e.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eMolnar C. (2022) Interpretable Machine Learning, 2nd edn. \u003cspan class=\"ExternalRef\"\u003e\u003cspan class=\"RefSource\"\u003ehttps://christophm.github.io/interpretable-ml-book/\u003c/span\u003e\u003cspan address=\"https://christophm.github.io/interpretable-ml-book/\" targettype=\"URL\" class=\"RefTarget\"\u003e\u003c/span\u003e\u003c/span\u003e\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eSadeghi Z, Alizadehsani R, Cifci MA, et al. A review of Explainable Artificial Intelligence in healthcare. Comput Electr Eng. 2024;118:109370. \u003cspan class=\"ExternalRef\"\u003e\u003cspan class=\"RefSource\"\u003ehttps://doi.org/10.1016/j.compeleceng.2024.109370\u003c/span\u003e\u003cspan address=\"10.1016/j.compeleceng.2024.109370\" targettype=\"DOI\" class=\"RefTarget\"\u003e\u003c/span\u003e\u003c/span\u003e.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eGoodfellow IJ, Shlens J, Szegedy C. Explaining and harnessing adversarial examples. In: Proc ICLR; 2015.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eCarlini N, Wagner D. (2017) Towards evaluating the robustness of neural networks. In: Proc IEEE S\u0026amp;P, pp 39\u0026ndash;57.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003ed\u0026rsquo;Avila Garcez A, Lamb LC. Neurosymbolic AI: the 3rd wave. Artif Intell Rev. 2023;56:12387\u0026ndash;406. \u003cspan class=\"ExternalRef\"\u003e\u003cspan class=\"RefSource\"\u003ehttps://doi.org/10.1007/s10462-023-10448-w\u003c/span\u003e\u003cspan address=\"10.1007/s10462-023-10448-w\" targettype=\"DOI\" class=\"RefTarget\"\u003e\u003c/span\u003e\u003c/span\u003e.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eBarrett C, Tinelli C. Satisfiability modulo theories. Handbook of Model Checking. Springer; 2018. pp. 305\u0026ndash;43.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eMarcus G. (2020) The next decade in AI: four steps towards robust artificial intelligence. arXiv:2002.06177.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eMao J, Gan C, Kohli P, Tenenbaum JB, Wu J. The neuro-symbolic concept learner: interpreting scenes, words, and sentences from natural supervision. In: Proc ICLR; 2019.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eRibeiro MT, Singh S, Guestrin C. (2016) Why should I trust you? explaining the predictions of any classifier. In: Proc KDD, pp 1135\u0026ndash;1144.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eLundberg SM, Lee SI. (2017) A unified approach to interpreting model predictions. In: Proc NeurIPS, pp 4765\u0026ndash;4774.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eSundararajan M, Taly A, Yan Q. (2017) Axiomatic attribution for deep networks. In: Proc ICML, pp 3319\u0026ndash;3328.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eVaswani A, Shazeer N, Parmar N et al. (2017) Attention is all you need. In: Proc NeurIPS, pp 5998\u0026ndash;6008.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eWachter S, Mittelstadt B, Russell C. Counterfactual explanations without opening the black box. Harv JL Tech. 2018;31:841.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eRudin C. Stop explaining black box machine learning models for high stakes decisions and use interpretable models instead. Nat Mach Intell. 2019;1:206\u0026ndash;15. \u003cspan class=\"ExternalRef\"\u003e\u003cspan class=\"RefSource\"\u003ehttps://doi.org/10.1038/s42256-019-0048-x\u003c/span\u003e\u003cspan address=\"10.1038/s42256-019-0048-x\" targettype=\"DOI\" class=\"RefTarget\"\u003e\u003c/span\u003e\u003c/span\u003e.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eLiu C, Arnon T, Lazarus C, et al. Algorithms for verifying deep neural networks. Found Trends Optim. 2021;4(3\u0026ndash;4):244\u0026ndash;404.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eHuang X, Kwiatkowska M, Wang S, Wu M. (2017) Safety verification of deep neural networks. In: Proc CAV, pp 3\u0026ndash;29.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eKatz G, Barrett C, Dill DL et al. (2017) Reluplex: an efficient SMT solver for verifying deep neural networks. In: Proc CAV, pp 97\u0026ndash;117.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eWang S, Pei K, Whitehouse J et al. (2018) Efficient formal safety analysis of neural networks. In: Proc NeurIPS, pp 6367\u0026ndash;6377.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eBayless S et al. (2025) ARc: a neurosymbolic approach to natural language formalization and verification. arXiv:2511.09008.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eAmazon Web Services. Automated Reasoning checks\u0026mdash;a new class of responsible AI capability. AWS Machine Learning Blog; 2025.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eDeepSeek-AI. (2025) DeepSeek-Prover-V2: advancing formal mathematical reasoning. arXiv.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eBiggio B, Roli F. Wild patterns: ten years after the rise of adversarial machine learning. Pattern Recognit. 2018;84:317\u0026ndash;31.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eMadry A, Makelov A, Schmidt L, et al. Towards deep learning models resistant to adversarial attacks. In: Proc ICLR; 2018.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eCohen J, Rosenfeld E, Kolter Z. (2019) Certified adversarial robustness via randomized smoothing. In: Proc ICML, pp 1310\u0026ndash;1320.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eGuo C, Rana M, Cisse M, van der Maaten L. Countering adversarial images using input transformations. In: Proc ICLR; 2018.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eInan H, Upasani K, Chi J et al. (2023) Llama Guard: LLM-based input-output safeguard for human-AI conversations. arXiv:2312.06674.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eYuan M, Kang M, Li B. (2025) R\u0026sup2;-Guard: robust reasoning enabled LLM guardrail via knowledge-enhanced logical reasoning. In: Proc ICLR. arXiv:2407.05557.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eLiu Y, Gao H, Zhai S et al. (2025) GuardReasoner: towards reasoning-based LLM safeguards. arXiv:2501.18492.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eShor PW. (1994) Algorithms for quantum computation: discrete logarithms and factoring. In: Proc FOCS, pp 124\u0026ndash;134.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eBernstein DJ, Lange T. Post-quantum cryptography. Nature. 2017;549:188\u0026ndash;94. \u003cspan class=\"ExternalRef\"\u003e\u003cspan class=\"RefSource\"\u003ehttps://doi.org/10.1038/nature23461\u003c/span\u003e\u003cspan address=\"10.1038/nature23461\" targettype=\"DOI\" class=\"RefTarget\"\u003e\u003c/span\u003e\u003c/span\u003e.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eNational Institute of Standards and Technology. (2024) Module-Lattice-Based Digital Signature Standard. FIPS 204. \u003cspan class=\"ExternalRef\"\u003e\u003cspan class=\"RefSource\"\u003ehttps://doi.org/10.6028/NIST.FIPS.204\u003c/span\u003e\u003cspan address=\"10.6028/NIST.FIPS.204\" targettype=\"DOI\" class=\"RefTarget\"\u003e\u003c/span\u003e\u003c/span\u003e\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eGoldwasser S, Micali S, Rivest RL. A digital signature scheme secure against adaptive chosen-message attacks. SIAM J Comput. 1988;17(2):281\u0026ndash;308.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003ede Moura L, Bj\u0026oslash;rner N. (2008) Z3: an efficient SMT solver. In: Proc TACAS, pp 337\u0026ndash;340. \u003cspan class=\"ExternalRef\"\u003e\u003cspan class=\"RefSource\"\u003ehttps://doi.org/10.1007/978-3-540-78800-3_24\u003c/span\u003e\u003cspan address=\"10.1007/978-3-540-78800-3_24\" targettype=\"DOI\" class=\"RefTarget\"\u003e\u003c/span\u003e\u003c/span\u003e\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eBarrett C, Fontaine P, Tinelli C. (2021) The SMT-LIB standard: version 2.6. \u003cspan class=\"ExternalRef\"\u003e\u003cspan class=\"RefSource\"\u003ehttps://smt-lib.org/\u003c/span\u003e\u003cspan address=\"https://smt-lib.org/\" targettype=\"URL\" class=\"RefTarget\"\u003e\u003c/span\u003e\u003c/span\u003e\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eBarbosa H et al. (2022) cvc5: a versatile and industrial-strength SMT solver. In: Proc TACAS, pp 415\u0026ndash;442.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eCimatti A, Griggio A, Schaafsma BJ, Sebastiani R. (2013) The MathSAT5 SMT solver. In: Proc TACAS, pp 93\u0026ndash;107.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003eDucas L, Kiltz E, Lepoint T, et al. CRYSTALS-Dilithium: a lattice-based digital signature scheme. IACR Trans CHES. 2018;2018(1):238\u0026ndash;68.\u003c/span\u003e\u003c/li\u003e \u003cli\u003e\u003cspan\u003ePerez F, Ribeiro I. (2023) Ignore this title and HackAPrompt: exposing systemic vulnerabilities of LLMs. In: Proc EMNLP, pp 4945\u0026ndash;4977.\u003c/span\u003e\u003c/li\u003e\u003c/ol\u003e"}],"fulltextSource":"","fullText":"","funders":[],"hasAdminPriorityOnWorkflow":false,"hasManuscriptDocX":true,"hasOptedInToPreprint":true,"hasPassedJournalQc":"","hasAnyPriority":false,"hideJournal":true,"highlight":"","institution":"","isAcceptedByJournal":false,"isAuthorSuppliedPdf":false,"isDeskRejected":"","isHiddenFromSearch":false,"isInQc":false,"isInWorkflow":false,"isPdf":false,"isPdfUpToDate":true,"isWithdrawnOrRetracted":false,"journal":{"display":true,"email":"[email protected]","identity":"researchsquare","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":true,"externalIdentity":"","sideBox":"","snPcode":"","submissionUrl":"/submission","title":"Research Square","twitterHandle":"researchsquare","acdcEnabled":true,"dfaEnabled":false,"editorialSystem":"","reportingPortfolio":"","inReviewEnabled":false,"inReviewRevisionsEnabled":true},"keywords":"AI security, Explainable analytics, Post-quantum systems, Cyber resilience, Data-driven verification, Trustworthy AI, Formal verification, SMT solvers, Cyber-physical systems, Safety-critical AI, Neurosymbolic systems, Machine learning security","lastPublishedDoi":"10.21203/rs.3.rs-8736256/v1","lastPublishedDoiUrl":"https://doi.org/10.21203/rs.3.rs-8736256/v1","license":{"name":"CC BY 4.0","url":"https://creativecommons.org/licenses/by/4.0/"},"manuscriptAbstract":"\u003cp\u003eAs artificial intelligence systems are deployed in complex, interconnected cyber-physical environments\u0026mdash;spanning healthcare diagnostics, critical infrastructure management, and autonomous vehicle control\u0026mdash;the limitations of traditional explainability methods become increasingly consequential. Post-hoc explanation techniques such as SHAP and LIME describe model behavior but cannot guarantee constraint satisfaction, leaving safety-critical systems vulnerable to adversarial manipulation and providing insufficient assurance for trustworthy AI deployment. This paper presents a theoretical framework and architecture for Formal Decision Traces (FDTs), a data-driven verification approach that integrates Satisfiability Modulo Theories (SMT) solvers with neural language models to produce machine-checkable proof certificates for system outputs, bridging the gap between explainable analytics and formal AI security. We make four contributions: (1) We present a theoretical framework for verified explainability and formally define FDTs as structured verification artifacts, establishing their advantages over attention-based and feature attribution methods for cyber-resilient applications. (2) We analyze the adversarial robustness properties of SMT-verified outputs, providing formal guarantees that constraint-based verification detects any encodable violation\u0026mdash;a completeness property that probabilistic guardrails cannot achieve. (3) We propose post-quantum secure attestation using NIST FIPS 204 (ML-DSA) lattice-based signatures, addressing the quantum threat to long-lived verification records in safety-critical domains. (4) We validate the architecture through a proof-of-concept implementation using the Z3 SMT solver across three safety-critical domains (healthcare, SCADA, autonomous vehicles), characterizing verification performance at 2\u0026ndash;4 ms per query (N\u0026thinsp;=\u0026thinsp;100 trials), demonstrating dual-channel cross-validation agreement across 21 test cases, confirming tamper detection across all FDT components, and measuring solver scalability to 500 constraints at sub-2 ms. These results provide empirical evidence that the proposed architecture is computationally feasible for real-time cyber-physical system integration.\u003c/p\u003e","manuscriptTitle":"Formal Decision Traces for Data-Driven Verification and Post- Quantum Attestation in Cyber-Resilient Explainable AI Systems","msid":"","msnumber":"","nonDraftVersions":[{"code":1,"date":"2026-02-11 07:07:40","doi":"10.21203/rs.3.rs-8736256/v1","editorialEvents":[{"type":"communityComments","content":0}],"status":"published","journal":{"display":true,"email":"[email protected]","identity":"researchsquare","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":true,"externalIdentity":"","sideBox":"","snPcode":"","submissionUrl":"/submission","title":"Research Square","twitterHandle":"researchsquare","acdcEnabled":true,"dfaEnabled":false,"editorialSystem":"","reportingPortfolio":"","inReviewEnabled":false,"inReviewRevisionsEnabled":true}}],"origin":"","ownerIdentity":"4642c6c7-444e-4a10-ab82-609048819286","owner":[],"postedDate":"February 11th, 2026","published":true,"recentEditorialEvents":[],"rejectedJournal":[],"revision":"","amendment":"","status":"posted","subjectAreas":[],"tags":[],"updatedAt":"2026-05-08T03:25:16+00:00","versionOfRecord":[],"versionCreatedAt":"2026-02-11 07:07:40","video":"","vorDoi":"","vorDoiUrl":"","workflowStages":[]},"version":"v1","identity":"rs-8736256","journalConfig":"researchsquare"},"__N_SSP":true},"page":"/article/[identity]/[[...version]]","query":{"redirect":"/article/rs-8736256","identity":"rs-8736256","version":["v1"]},"buildId":"XKTyCvWXoU3ODBz1xrDgd","isFallback":false,"isExperimentalCompile":false,"dynamicIds":[84888],"gssp":true,"scriptLoader":[]}