Abstract
<title>Abstract</title> <p>Applying Large Language Models (LLMs) to the autonomous remediation of cloud misconfigurations is complicated by model hallucination, as generated patches can be syntactically well-formed yet semantically insecure. We present Sentinel-Mesh, a neuro-symbolic framework that couples LLM-driven patch synthesis with an SMT-based Cloud Perimeter Model (CPM) to produce formal verification results over a compact three-variable abstraction of network exposure, encryption state, and data sensitivity. A Z3 theorem prover serves as a closed-loop verification oracle, requiring every proposed patch to satisfy CPM invariants before acceptance. The CPM adopts a bounded 12-point integer domain (Z × E × S), enabling exhaustive SMT reasoning over approximately 60 AWS resource types without requiring Terraform engine execution. Properties outside this abstraction, including full IAM policy semantics and multi-account configurations, are handled by heuristic dispatcher tiers and therefore carry no formal guarantee. We evaluate Sentinel-Mesh on CloudFix-Bench, comprising 105 hand-crafted AWS Terraform misconfigurations derived from documented patterns in the CSA Top Threats report and AWS Security Best Practices. The framework autonomously remediated 83.81% of cases (95% Wilson score confidence interval: 75.59%–89.64%) within the evaluated benchmark and CPM verification scope, blocked all 17 hallucinated patches before acceptance, achieving a 0% regression rate within the evaluated scope, and generated 29 formal proof certificates confirming CPM invariant satisfaction for accepted remediations. These results indicate that integrating symbolic verification with generative models can reduce the risk of unsafe autonomous cloud remediation within the bounds of the proposed CPM abstraction.</p>