Emergent Formal Verification: How an Autonomous AI Ecosystem Independently Discovered SMT-Based Safety Across Six Domains

• URL: http://arxiv.org/abs/2603.21149v1
• Date: Sun, 22 Mar 2026 10:02:16 GMT
• Title: Emergent Formal Verification: How an Autonomous AI Ecosystem Independently Discovered SMT-Based Safety Across Six Domains
• Abstract summary: We propose a unified framework that applies Z3-based verification across all six output classes through a common API.<n>We evaluate it on 181 test cases across five implemented domains, achieving 100% classification accuracy with zero false positives and zero false negatives.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: An autonomous AI ecosystem (SUBSTRATE S3), generating product specifications without explicit instructions about formal methods, independently proposed the use of Z3 SMT solver across six distinct domains of AI safety: verification of LLM-generated code, tool API safety for AI agents, post-distillation reasoning correctness, CLI command validation, hardware assembly verification, and smart contract safety. These convergent discoveries, occurring across 8 products over 13 days with Jaccard similarity below 15% between variants, suggest that formal verification is not merely a useful technique for AI safety but an emergent property of any sufficiently complex system reasoning about its own safety. We propose a unified framework (substrate-guard) that applies Z3-based verification across all six output classes through a common API, and evaluate it on 181 test cases across five implemented domains, achieving 100% classification accuracy with zero false positives and zero false negatives. Our framework detected real bugs that empirical testing would miss, including an INT_MIN overflow in branchless RISC-V assembly and mathematically proved that unconstrained string parameters in tool APIs are formally unverifiable.

Related papers

• Non-Degenerate Risk Certification for Automated Security Decisions: A Decision-Contract Theory with ATT\&CK-Aligned Triage as a Worked Instance [1.4915002678801434]
  An unconditional risk bound on automated decisions can be satisfied without automating anything, since a selector that never acts drives the bound to zero.<n>We show this is structural: any risk certificate is defined over a decision contract, the inputs a system acts on plus the semantic relation under which an output counts correct.<n>We develop a decision-contract theory: an error-conservation law showing error is only reassigned among harmful automation, human deferral, and semantic masking.
  arXiv  Detail & Related papers  (2026-08-12T16:59:19Z)
• VATS: Exploiting Implicit Authority in Error-Path Injection via Systematic Mutation [0.3222802562733787]
  We introduce VATS (Vulnerability Analysis of Tool Streams), a mutation-driven framework that evolves adversarial payloads across seven structural and linguistic dimensions.<n>Our evaluation across four frontier models, Gemini 3.1 Pro, GPT-5.5, GLM-5.1, and Qwen3-Coder, demonstrates that error-path injection triples the success rate of standard indirect prompt injection.
  arXiv  Detail & Related papers  (2026-06-06T06:07:52Z)
• Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems [100.24694338574402]
  We present Inductive Deductive Synthesis (IDS), which jointly and incrementally synthesizes implementation and proof.<n>IDS achieves 7/7 in about 6.8 hours and $106 per spec on average, roughly 200x faster than expert effort and 17% cheaper than SOTA agents.<n>IDS further incorporates performance feedback into the same loop, yielding implementations up to 3x faster than published verified systems.
  arXiv  Detail & Related papers  (2026-05-22T00:05:36Z)
• Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline [0.0]
  We present a formally verified framework for patent analysis as a hybrid AI + Lean 4 pipeline.<n>The DAG-coverage core (Algorithm 1b) is fully machine-verified once bounded match scores are fixed.<n>Claims are encoded as DAGs in Lean 4, match strengths as elements of a verified complete lattice, and confidence scores propagate through dependencies via proven-correct monotone functions.
  arXiv  Detail & Related papers  (2026-04-20T22:02:57Z)
• Broken by Default: A Formal Verification Study of Security Vulnerabilities in AI-Generated Code [0.0]
  Broken by Default is a formal verification study of 3,500 code artifacts generated by seven widely-deployed LLMs across 500 security-critical prompts.<n>Across all models, 55.8% of artifacts contain at least one COBALT-identified vulnerability; of these, 1,055 are formally proven via Z3 satisfiability witnesses.<n>GPT-4o leads at 62.4% (grade F); Gemini 2.5 Flash performs best at 48.4% (grade D)
  arXiv  Detail & Related papers  (2026-04-07T00:55:42Z)
• You Told Me to Do It: Measuring Instructional Text-induced Private Data Leakage in LLM Agents [9.719776777345364]
  High-privilege LLM agents that autonomously process external documentation are increasingly trusted to automate tasks.<n>These agents are granted terminal access, control, and outbound network connectivity with minimal security oversight.<n>We measure a fundamental vulnerability in this trust model, which we term the emphTrusted Executor Dilemma<n>This vulnerability is a structural consequence of the instruction-following design paradigm, not an implementation bug.
  arXiv  Detail & Related papers  (2026-03-12T12:35:46Z)
• Synthesizing the Kill Chain: A Zero-Shot Framework for Target Verification and Tactical Reasoning on the Edge [12.201060368447251]
  This paper introduces a hierarchical, zero-shot framework that cascades lightweight object detection with compact Vision-Language Models (VLMs)<n>We evaluate this pipeline on 55 high-fidelity synthetic videos from Battlefield 6 across three tasks: false-positive filtering (up to 100% accuracy), damage assessment (up to 97.5%), and fine-grained vehicle classification (55-90%)
  arXiv  Detail & Related papers  (2026-02-10T23:00:19Z)
• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in code generation, but their proficiency in producing secure code remains a critical, under-explored area.<n>We introduce RealSec-bench, a new benchmark for secure code generation meticulously constructed from real-world, high-risk Java repositories.
  arXiv  Detail & Related papers  (2026-01-30T08:29:01Z)
• ReasAlign: Reasoning Enhanced Safety Alignment against Prompt Injection Attack [52.17935054046577]
  We present ReasAlign, a model-level solution to improve safety alignment against indirect prompt injection attacks.<n>ReasAlign incorporates structured reasoning steps to analyze user queries, detect conflicting instructions, and preserve the continuity of the user's intended tasks.
  arXiv  Detail & Related papers  (2026-01-15T08:23:38Z)
• What Matters For Safety Alignment? [38.86339753409445]
  This paper presents a comprehensive empirical study on the safety alignment capabilities of AI systems.<n>We systematically investigate and compare the influence of six critical intrinsic model characteristics and three external attack techniques.<n>We identify the LRMs GPT-OSS-20B, Qwen3-Next-80B-A3B-Thinking, and GPT-OSS-120B as the top-three safest models.
  arXiv  Detail & Related papers  (2026-01-07T12:31:52Z)
• OmniSafeBench-MM: A Unified Benchmark and Toolbox for Multimodal Jailbreak Attack-Defense Evaluation [94.61617176929384]
  OmniSafeBench-MM is a comprehensive toolbox for multi-modal jailbreak attack-defense evaluation.<n>It integrates 13 representative attack methods, 15 defense strategies, and a diverse dataset spanning 9 major risk domains and 50 fine-grained categories.<n>By unifying data, methodology, and evaluation into an open-source, reproducible platform, OmniSafeBench-MM provides a standardized foundation for future research.
  arXiv  Detail & Related papers  (2025-12-06T22:56:29Z)
• Can AI Keep a Secret? Contextual Integrity Verification: A Provable Security Architecture for LLMs [0.0]
  We present Contextual Integrity Verification (CIV), a provenance-time security architecture that attaches cryptographic inferenceally signed labels to every token.<n>CIV provides provenance, per-token non-interference guarantees on frozen models.<n>We demonstrate drop-in protection for Llama-3-8B and Mistral-7B.
  arXiv  Detail & Related papers  (2025-08-12T18:47:30Z)
• SORRY-Bench: Systematically Evaluating Large Language Model Safety Refusal [64.9938658716425]
  SORRY-Bench is a proposed benchmark for evaluating large language models' (LLMs) ability to recognize and reject unsafe user requests.<n>First, existing methods often use coarse-grained taxonomy of unsafe topics, and are over-representing some fine-grained topics.<n>Second, linguistic characteristics and formatting of prompts are often overlooked, like different languages, dialects, and more -- which are only implicitly considered in many evaluations.
  arXiv  Detail & Related papers  (2024-06-20T17:56:07Z)
• ASSERT: Automated Safety Scenario Red Teaming for Evaluating the Robustness of Large Language Models [65.79770974145983]
  ASSERT, Automated Safety Scenario Red Teaming, consists of three methods -- semantically aligned augmentation, target bootstrapping, and adversarial knowledge injection. We partition our prompts into four safety domains for a fine-grained analysis of how the domain affects model performance. We find statistically significant performance differences of up to 11% in absolute classification accuracy among semantically related scenarios and error rates of up to 19% absolute error in zero-shot adversarial settings.
  arXiv  Detail & Related papers  (2023-10-14T17:10:28Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.