phases.md

Implementation Phases

Phase 1: Core DSL + Single-Machine Verification ✅

Delivered:

• machine() builder with full fluent API
• Guards and actions as constrained JS functions
• TypeScript generics for type-safe context
• AST/IR representation (MachineAST)
• JS → TLA+ compiler (tokenizer, parser, code generator)
• TLA+ spec generation from MachineAST
• TLC integration with auto-download
• Structured VerifyResult with violation traces
• 74 unit tests

Phase 2: Concurrent Composition ✅

Delivered:

• concurrent() builder with .instances(), .shared(), .interaction()
• Multi-process TLA+ generation with indexed variables
• Fairness conditions (weak/strong)
• Tests with worker pool spec

Phase 3: Trace-Driven Test Generation ✅

Delivered:

• BFS-based coverage strategy (covers all transitions)
• Violation strategy (extracts TLC counterexamples)
• JSON trace serialization/deserialization
• Targeted path finding for hard-to-reach transitions

Phase 4: Vitest Plugin + CLI ✅

Delivered:

• stateproof() Vitest plugin
• stateproof CLI with check, generate, mermaid, diff subcommands
• CI-friendly output

Phase 5: Advanced ✅

Delivered:

• generateRuntimeCode() — standalone TypeScript from specs
• createRuntime() — executable state machines
• diffSpecs() — spec comparison
• toMermaidStateDiagram() — state diagrams
• violationToMermaidSequence() — counterexample diagrams
• traceToMermaidSequence() — trace diagrams

Self-Verification ✅

The compilation pipeline is specified using stateproof itself:

• CompilationPipeline spec with 7 states, 8 transitions, 2 invariants
• Tests verify the spec, TLA+ generation, runtime, and test generation