Research Motivation
Sentinel-Mesh started from an engineering observation, not a literature review. While building the 28K+ record AI enrichment pipeline at TechPotion, I noticed a recurring reliability limitation in the translation and enrichment stage. Most outputs succeeded, but some repeatedly failed and needed retries, and in some cases the model returned malformed JSON even though the task was tightly constrained. Roughly 2 in 10 outputs hit one of these problems. That was a rough observation from that pipeline, and it fluctuated with model and load. It is not a general AI failure rate.
Why Structured-Output Reliability Matters
In that pipeline, the fix was engineering discipline: schema-checked outputs, and status gates that keep a failed record visible and retryable instead of silently marking it done. A schema check can tell you an output is well-formed. It can't tell you the output is correct.
The Cloud-Security Question
That gap matters much more when the output is a change to cloud infrastructure. A Terraform patch can be syntactically valid and still leave a storage bucket public, drop encryption, or open a security group to the internet. The experience raised a broader question: if a model can't consistently produce valid structured output for a bounded task, how should AI-generated changes be trusted when the consequences involve cloud security?
Research Question
Can an LLM's proposed remediation for a Terraform misconfiguration be accepted only when a formal verifier shows it satisfies explicit security invariants, and does feeding the verifier's rejection back to the model improve repair rates?
Sentinel-Mesh explores that by combining three things: LLM remediation generation, Z3 SMT formal verification, and Terraform remediation, in a single closed loop.
Architecture
- Parsing. Terraform HCL is converted to a JSON structure with python-hcl2.
- Initial verification. A Z3-based verifier checks every resource. Per-resource security checks are encoded as Z3 queries over the Cloud Perimeter Model (CPM), which covers network isolation, encryption at rest and in transit, and defense in depth. Dedicated Z3 reachability checks look for IAM privilege-escalation paths and security groups that expose critical ports. A configuration that passes needs no patch.
- Patch generation. On a violation, an LLM agent receives the original configuration and the verifier's violation message, and proposes a remediated configuration.
- Patch verification. The HCL is extracted from the model response, re-parsed, and checked again by the full verifier. That re-check alone decides whether the patch passes.
- Feedback loop. A rejected patch's verdict becomes the context for the next attempt, for up to 5 attempts. A case with no verified patch after 5 attempts is recorded as a persistent failure.
- Proof certificate. For encryption and network-exposure violations, an accepted patch also goes through a dual-solver refinement proof over the CPM. The proof annotates the result; it never overrides the verifier's decision.
LLM Remediation Generation
Patch generation is zero-shot and multi-provider: the agent supports Cerebras, Gemini, and Groq backends, rotating across providers with cooldowns to handle rate limits. The model only proposes; it never decides whether its own patch is acceptable. Responses are normalized by extracting the fenced HCL block, so conversational text around the code can't reach the verifier.
Formal Verification with Z3 SMT
Security properties are encoded as Z3 constraints over the parsed configuration. When a configuration violates an invariant, the solver finds a satisfying assignment for the violation, a counterexample witness: for example, a concrete source address and port that reach a critical service, or a chain of IAM permissions that reaches administrator access. The verifier's verdict, built from that witness, is fed into the next prompt.
A candidate patch is accepted only if the full verifier passes it. For violations the CPM can model directly, encryption and network exposure, an accepted patch also gets a dual-solver refinement proof. Solver A checks completeness: that no counterexample exists, so the patched configuration satisfies the modeled invariants. Solver B checks non-regression: it uses the original configuration to confirm the violation was real, then shows that the patched configuration cannot retain that violation class. Passing both produces a formal proof certificate. Audit and policy properties, such as a missing WAF association or lifecycle policy, sit outside the CPM state space, so they are decided by the verifier alone.
Terraform Remediation
The unit of work is a real Terraform configuration: a main.tf per test case, covering resources across 8 infrastructure pillars (management, identity, database, networking, security, compute, analytics, and storage) and 60+ AWS service types. Patches are full, re-parseable configurations, not diff hints.
CloudFix-Bench
To evaluate the loop, I built CloudFix-Bench: 105 AWS Terraform misconfiguration patterns, each a self-contained Terraform case with a known violation. The benchmark is archived on Zenodo so the evaluation can be reproduced.
Evaluation
The evaluation compares the full loop against three references:
- Checkov baseline. A static linter run on the same cases.
- No-witness ablation. The same loop without Z3 counterexample feedback, to isolate what the witness contributes.
- External set. 12 Terraform misconfigurations from outside the benchmark, to test generalization.
Success rates are reported with 95% Wilson score confidence intervals. The reported results:
- Full Sentinel-Mesh remediation rate: 88/105 (83.81%), 95% interval 75.59% to 89.64%
- No-witness ablation: 68/105 (64.76%), 95% interval 55.25% to 73.23%
- Checkov baseline: 37/105 (35.24%), 95% interval 26.77% to 44.75%
- External set: 6/12 (50.00%), 95% interval 25.38% to 74.62%
- Security regression rate: 0.0%, 95% interval 0.00% to 3.45%
Of the 88 fixed cases, 75 were fixed on the first attempt. Formal proof certificates were issued for 29 of the 105 cases.
Findings
- Verification feedback helped. Removing the counterexample witness dropped the remediation rate from 83.81% to 64.76% on the same cases, which suggests the witness gives the model information a plain error message doesn't.
- Verified repair outperformed static linting on this benchmark. The full loop reached 83.81% against 35.24% for the Checkov baseline.
- No regressions were observed within the stated scope. The reported security regression rate was 0.0% (95% interval 0.00% to 3.45%), measured against the modeled invariants.
- Coverage varied by pillar. Management (7/7) and identity (9/9) cases were all fixed; compute (16/22), analytics (10/14), and storage (7/10) were the hardest.
Limitations
- Scope is the model. Verification is only as complete as the Cloud Perimeter Model. A pass means the patch satisfies the modeled invariants, not that the configuration is secure in every respect.
- Generalization is still open. The external set reached 6 of 12 cases (50%), with a wide confidence interval, so results on real-world configurations need a larger evaluation.
- 17 benchmark cases were not fixed within 5 attempts, concentrated in the compute, analytics, and storage pillars.
- Certificates cover a subset. Formal proof certificates were issued for 29 of 105 cases. The dual-solver proof only applies to encryption and network violations; other accepted patches rest on the verifier's checks alone.
- Status. The work is a Research Square preprint and the manuscript is under review; the results have not yet completed peer review.
Future Work
The limitations point to the next steps: a larger external evaluation on real-world Terraform, broader invariant coverage for the pillars with the lowest repair rates, and extending proof certificates beyond the current subset of policies.
Research Artifacts
The Research Square preprint, the CloudFix-Bench dataset on Zenodo, the source code, and a technical article are linked under public evidence below, and collected on the research page. I'm the lead author and developer; the preprint is co-authored, and lists the full author team.