Cloud providers rely on compliance controls to ensure that customer resources are configured according to security best practices — from encryption of storage to network isolation of compute instances. Today, these controls are typically written as general-purpose programs (e.g., in Python or Java), making them difficult to analyze, test exhaustively, and maintain. We present ControlsDSL, a domain-specific language for writing compliance controls. ControlsDSL's restricted semantics enables analysis based on Satisfiability Modulo Theories (SMT), generating test inputs automatically, verifying semantic equivalence between control versions, and supporting scenario generation. Given a control, ControlsDSL produces a set of human-readable scenarios that describe every possible execution path and its expected result. We prove that generated scenarios are sound (they accurately predict the control's behavior) and complete (every well-typed input is covered by at least one scenario). We evaluate ControlsDSL on 397 compliance controls deployed in production at Amazon Web Services (AWS), demonstrating its expressiveness, the effectiveness of scenario generation, and the practical value of SMT-based analysis for control development and migration. ControlsDSL controls serve over one billion daily compliance evaluations and are 3.3× more concise than their Python/Java counterparts. Scenario generation completes in under one second for the vast majority of controls, and SMT-based test generation achieves complete path coverage—completing in seconds for the median control, with a heavy tail (minutes) for the more complex controls.
