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

1. Problem Statement

As AI systems increasingly generate code, invoke tools, execute shell commands, and produce compressed models, ensuring the safety of these outputs is critical. Current safety verification methods are predominantly empirical (e.g., test suites, red-teaming, benchmarks), which only check specific inputs and cannot guarantee safety across the entire input space.
The paper argues that formal verification, which provides mathematical proofs of correctness, is necessary to offer stronger guarantees. However, existing research is siloed, addressing single output modalities (e.g., only code or only reasoning) without a unified framework. Furthermore, it is unclear whether the need for formal verification is an arbitrary human design choice or an emergent property of complex AI systems reasoning about their own safety.

2. Methodology

The paper employs a two-pronged methodology: Empirical Observation of an autonomous AI ecosystem and Experimental Validation via a newly developed framework.

A. Emergent Discovery Observation

The authors analyzed SUBSTRATE S3, an autonomous AI ecosystem comprising 73 agents that generates product specifications without explicit instructions on formal methods.

• Process: Over 24 days, S3 generated 215 unique MVP specifications across 39 product concepts.
• Analysis: The authors consolidated these specifications and identified 11 emergent safety principles.
• Key Finding: The principle of "Formal Verification" (Principle 1) emerged independently in six distinct domains across eight different products.
• Independence Verification: The discoveries were confirmed as independent because:
  • They occurred on different dates in response to different RSS feeds (healthcare, infrastructure, hardware, blockchain, etc.).
  • Jaccard similarity between the text of the specifications was below 15%.
  • The ecosystem never cross-referenced its own prior mentions of Z3, indicating no internal pattern matching.

B. Framework Development: substrate-guard

Motivated by the emergent discovery, the authors built substrate-guard, a unified verification framework.

• Core Engine: Uses the Z3 SMT (Satisfiability Modulo Theories) solver.
• Architecture: A unified API verify(artifact, spec, type) dispatches artifacts to domain-specific translators that convert them into Z3 constraints.
• Supported Domains:
  1. LLM-Generated Code: Translates Python functions to Z3 constraints using Static Single Assignment (SSA) form. Supports integers, floats, and booleans (loops and strings are unsupported).
  2. Tool API Safety: Models API parameters as Z3 variables to check if any combination triggers forbidden patterns (e.g., SQL injection).
  3. Post-Distillation Reasoning: Verifies mathematical reasoning traces by checking if step transformations hold as logical implications using SymPy and Z3.
  4. CLI Commands: Encodes dangerous command patterns as boolean variables to verify safety.
  5. Hardware Assembly: Performs symbolic execution of RISC-V RV32I assembly using 32-bit bitvectors to check register bounds and privilege escalation.

3. Key Contributions

1. Empirical Evidence of Emergence: The paper documents the first instance of an autonomous AI system independently discovering the necessity of formal verification across six diverse domains without human prompting, suggesting it is a fundamental requirement for complex safety reasoning.
2. Unified Verification Framework (substrate-guard): The first framework to unify Z3-based verification across multiple AI output modalities (Code, Tools, Reasoning, CLI, Hardware) via a common API.
3. Novel Applications:
   • First application of Z3 to Tool API safety for AI agents.
   • First application of Z3 to post-distillation reasoning verification.
   • Formal proof that unconstrained string parameters in tool APIs are mathematically unverifiable.
4. Bug Detection: Demonstrated the ability to catch real-world bugs (e.g., INT_MIN overflow) that empirical testing would miss due to the vastness of the input space.

4. Results

The framework was evaluated on 135 test cases across five implemented domains (Code, Tool APIs, CLI, Hardware, Distillation).

• Accuracy: 100% classification accuracy.
  • 0 False Positives: No correct artifacts were flagged as unsafe.
  • 0 False Negatives: No buggy artifacts passed verification.
• Performance:
  • Code: ~70ms average.
  • Tool APIs: ~15ms average.
  • CLI: <1ms average.
  • Hardware: ~5ms average.
  • Distillation: ~30ms average.
• Notable Discoveries:
  • INT_MIN Overflow: The hardware verifier detected that the standard branchless absolute value trick fails for INT_MIN (-2,147,483,648) in 32-bit arithmetic, a bug rarely caught by random testing.
  • Unverifiable Strings: Proved that any tool with an unconstrained string parameter cannot be formally certified as safe, as Z3 can instantly construct a string containing a forbidden pattern.
  • Compiler Equivalence: Formally proved that specific assembly optimizations preserve semantics for all possible inputs.

5. Significance and Implications

• Shift in AI Safety Paradigm: The results suggest that AI safety should not rely solely on empirical testing. Formal verification offers mathematical guarantees that are feasible, fast, and capable of finding edge-case bugs.
• Theoretical Insight: The "emergent discovery" implies that sufficiently complex AI systems reasoning about safety constraints may naturally converge on formal verification as a necessary mechanism. This hints at a form of "safety awareness" emerging from the system's internal logic rather than explicit programming.
• Future Directions: The paper calls for replication of these findings with other autonomous systems and the extension of the framework to additional modalities (e.g., natural language reasoning, full Python support).

Conclusion: The paper establishes that formal verification is not just a human-imposed constraint but an emergent property of complex AI safety reasoning. The substrate-guard framework validates this by successfully applying Z3 across multiple domains with perfect accuracy, providing a blueprint for mathematically guaranteeing the safety of autonomous AI outputs.