SAT-Based Synthesis and DEVS Simulation from Partial Generative Specifications for Verifiable AI

Abstract

System models and artifacts continuously require validation and refinement to address imprecise specifications and early-stage requirements in order to derive executable simulations. We propose a multi-layer approach for the automated formalization and execution of partial generative specifications derived from high-level descriptions. The first layer processes model seeds—potentially produced by large language models—that capture coarse structural information such as node relations, ordering, and timing estimates. Rather than requiring fully specified executable models from generative sources, we restrict their role to producing partial specifications, which are then completed through formal synthesis. We implement a synthesis engine based on Boolean satisfiability that constructs executable control flow structures from these partial specifications while enforcing structural consistency and execution semantics. Satisfiability modulo theories are further used to verify temporal properties and establish simulation baselines. The resulting models are then transformed into a set-theoretic discrete event system specification, enabling executable simulation via generated code artifacts. This pipeline establishes a unified pathway from partial generative artifacts to formally validated and executable models. It enables reliable and interpretable exploration of design alternatives and experimentation under formally grounded structural and temporal constraints, while providing a foundation for integrating generative modeling with rigorous execution semantics.