Spec-first development with dark provenance.
Write what your system should do. Prove it. Ship with full traceability.
Speckl is an open standard for specification-first development with dark provenance. It defines how to write what a system should do — in a machine-verifiable format — before any code is written. Every behavior traces back to its source of intent.
Speckl is not a product or a platform. It is a methodology and language specification, published freely under MIT. The SpeckDL language, the Dark Provenance methodology, and the reference implementations define the standard. Products built on it — compilers, verification tools, compliance APIs — will come as the ecosystem grows.
A constraint-based specification language that defines what a system does, not how. Specs are small, stable, and machine-verifiable — the audit surface for regulated systems.
A methodology where every behavior traces back to its source — a regulation, a design decision, a conversation. The provenance graph is always present, materialized on demand for audits or debugging.
Minimal reference tools for SpeckDL parsing, Z3 constraint verification, and provenance graph generation. The building blocks for tooling, not a production system.
The standard is the foundation. Consulting, SaaS tooling, and compliance APIs will build on it — validated through real-world use before they ship.
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 provenance: traceability to regulations, design decisions, and source conversations — embedded in the spec, not added later.
speck RetryHandler { input: { operation: Operation, maxRetries: Nat } output: Result // Constraints the compiler proves via Z3 constraint: maxRetries <= 5 constraint: backoff(delay(n)) == delay(n-1) * 2 constraint: totalDelay < 30s // Always-verified properties verify: always(implies(attempt > 1, delay > 0)) // Dark provenance: where did this intent come from? provenance: { regulation: "DO-178C 6.4.2.2" } provenance: { design_decision: "ADR-0042" } source: conversation ref "slack://C123/456" review: manual }
Specs are orders of magnitude smaller than the code they generate. They change less often. The audit surface stays tractable.
If Speck→WASM compilation preserves semantics, human review at the spec boundary satisfies assurance requirements.
Agents generate code. Humans own specifications. The chain of custody for intent stays intact.
Open Standard: SpeckDL language, Dark Provenance methodology, reference implementations.
Consulting: Hands-on engagements with regulated-industry teams.
SaaS: Spec editor, live Z3 verification, provenance graph browser.
Compliance API: Audit reports, traceability matrices.