SpeckDL defines what a system does, not how. The compiler produces deterministic output: Z3 → Decision Structure → WASM. Same input, same output — every time.
+SpeckDL defines what a system does, not how. The compiler produces deterministic output: Z3 → Decision Structure → WASM. Same input, same output — every time. Every spec includes dark provenance: traceability to regulations, design decisions, and source conversations — embedded in the spec, not added later.
speck RetryHandler { input: { operation: Operation, maxRetries: Nat }