Where humans and AI collaborate in the same language.
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.
Compiles SpeckDL directly to Wasm through a deterministic pipeline — Z3 constraint solving, then code generation. No LLMs, no non-determinism. Same input, same output, every time.
Minimal implementations for SpeckDL parsing, Z3 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.
SpeckDL is the shared space humans and AI both work in — human-judgeable, AI-writable, and compiler-enforced to the binary.
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.