Introduction

Weltenwanderer is a compiler for formally verified Event Sourcing systems. It takes .ddd files — written in the language of domain experts — and verifies their internal consistency before producing executable code.

Domain language is specification. Everything else is infrastructure.

The Problem It Solves

Runtime frameworks catch errors at runtime or in tests. If your decide function misses a state transition, you discover that in production or when a test case covers it. Weltenwanderer catches those errors at compile time, before any code runs.

Domain models also drift from code over time. Comments go stale. Tests cover the happy path. The .ddd file is the single source of truth — the compiler and the generated code are both derived from it, so they cannot diverge.

A First Look at .ddd

This snippet from examples/minimal/registration.ddd shows the core constructs:

context Registration {

  type Email = String
  type DisplayName = String

  command Register {
    email: Email
    name: DisplayName
    validate email != ""
      else "Email must not be empty"
  }

  event Registered {
    email: Email
    name: DisplayName
  }

  decider User {
    commands: Register
    events: Registered
    state: Unregistered | Active(email: Email, name: DisplayName)
    initial: Unregistered

    decide(Register, Unregistered) -> [Registered { email, name }]
    decide(Register, Active) -> already "User is already registered"

    evolve(Unregistered, Registered) -> Active
    evolve(Active, Registered) -> Active
  }
}

command declares an intent with its fields. The validate clause specifies value-level constraints. event records a fact. decider ties commands, events, and state together: decide specifies which events each command produces in each state; evolve specifies how each event advances the state.

Four Constraint Layers

Every constraint in .ddd maps to one of four layers, each with a distinct scope and failure mode:

Layer	Keyword	Scope	On Failure
Type	: TypeName	Compile time	Compile error
Value	validate	Command construction	Err(ValidationError[]) — command not created
Business Rule	require	decide invocation	Err(RejectionError) — no events produced
Postcondition	ensure	After evolve	Compile error — derived from evolve definition

Type constraints are resolved statically. Value constraints become smart constructors — the command object cannot be created if the constraint fails. Business rules are state-dependent guards checked at decision time. Postconditions are verified by the compiler from the shape of the evolve function, not at runtime.

Three Computation Layers

The language partitions behavior into three layers with distinct decidability properties:

Layer	DSL Construct	Formal Class	Decidable?
Pure Projection	evolve	DynPROP (regular languages)	Yes, fully
Cross-Aggregate	projection with lookup	DynQF / DynFO	Yes, with constraints
Reactive Flows	flow (events → commands → events)	Turing-complete	Bounded cases only

The evolve function is a left-fold (catamorphism). When the state type is a finite algebraic data type, the projection is a finite automaton — all properties are decidable (Gelade, Marquardt, Schwentick 2012). The system becomes Turing-complete only through flow composition across deciders.

For the mathematical foundation, see Why Category Theory?.

What the Compiler Verifies

The compiler performs eight checks on every .ddd file:

Check	What It Catches
Exhaustiveness	Missing decide branches — command/state pairs with no handler
Evolve totality	Missing evolve branches — event/state pairs with no handler
Guard consistency	Contradictory require clauses that can never both be satisfied
Postcondition derivability	ensure postconditions that cannot be verified from the evolve definition
Dead code detection	Commands and events declared but not referenced by any decider
Terminal state enforcement	decide clauses that target a terminal state, or deciders with no non-terminal state
Positioned diagnostics	Every error includes file, line, column, and an actionable fix suggestion
Expression grammar	Operator-precedence grammar for validate and require expressions

All checks operate on the AST and are platform-independent. They apply regardless of the code generation target. If the compiler accepts a .ddd file, the stated properties hold. See Validation Reference for the full specification of each check.

What Gets Generated

From a validated .ddd file, the compiler generates TypeScript code targeting the Emmett framework: a decider class, smart constructors from validate constraints, event and state union types, and Emmett wiring. See Code Generation for details.

How It Differs from Frameworks

Aspect	Weltenwanderer	Runtime Frameworks
Verification	Static, at compile time	Dynamic, at runtime or in tests
Correctness	Proven by the compiler for all inputs	Tested by the developer for sampled inputs
Code generation	From a single verified source	Manual wiring of events, states, and handlers
Domain language	First-class DSL with compile-time semantics	Library conventions embedded in the host language

Where to Go Next

• Quick Start — write and validate a .ddd file
• Event Sourcing Primer — background on Event Sourcing and why formal verification applies
• Decider Reference — full syntax for commands, events, states, and transitions
• Validation Reference — detailed specification of all seven compiler checks
• Why Category Theory? — the theoretical foundation for decidability
• Roadmap — full feature status and planned phases