2026-05-06 - 2026-11-06
Overview
46 issues closed from 3 users
Closed
#59 PROV-O / CycloneDX / SPDX artifacts are shallow — no per-event, per-constraint traceability
Closed
#58 Z3 generator produces invalid SMT-LIB2 for common constraint idioms
Closed
#60 Add protobuf backend — emit .proto from .speckdl so generated bindings replace handwritten APIs (zero glue)
Closed
#61 Parser drops field declarations in record-style interface blocks (only enum variants are captured)
Closed
#57 [parser] Multi-line input: { ... } and output: { ... } blocks parse as ident (no fields)
Closed
#55 [generator] LTL inner-expression identifiers not qualified with this. — input fields + action params out of scope in rewriteExpr
Closed
#42 [speckl#37.4] B3: Emit real TypeScript if/then/else in TS generator
Closed
#41 [speckl#37.3] B4: Add SpeckDL difference set operator to TS generator rewriteExpr
Closed
#54 [parser] Multi-line verify: bodies truncated in parseMember (parser.ts:422) — blocks B2 PR stack
Closed
#48 [speckl#37.10] B2.2: Implement verifyN() with runtime LTL evaluator (or Z3 call-out)
Closed
#53 [parser] Multi-line Map(K, { ... }) type misparsed line-by-line in parseStateBlock (parser.ts:538)
Closed
#52 [speckl#37.11] B1-redux: Delete preamble heuristic in TS generator emitAction (re-diagnosis)
Closed
#43 [speckl#37.5] B1: Stop silently inventing let/forall stubs in TS generator
Closed
#51 [CRITICAL — Re-apply lost work] B2.1 constraint forwarding (#47) + #49 multi-line input/output parser, working tree was reset without commit
Closed
#47 [speckl#37.9] B2.1: Forward constraint expressions through TS generator (rewriteExpr chain)
Closed
#45 [speckl#37.7] B2: Forward constraint/verify expressions through TS generator (or evaluate at runtime)
Closed
#49 Parser: parse input: { name: Type, ... } and output: { ... } record body into fields
Closed
#44 [speckl#37.6] B5: Fix parser init-block handling so generator emits init body
Closed
#46 [speckl#37.8] B6: Add readonly modifier + JSDoc on emitted state variables
Closed
#37 Unblock Speckl compiler: Fix TS generator bugs so all examples build clean
Closed
#39 [speckl#37.1] Triage TS generator bugs: enumerate specific bugs with file paths + repros
Closed
#40 [speckl#37.2] Fix top P0+P1 TS generator bugs from #37.1 triage
Closed
#38 [speckl#37.3] Verify all example specs compile clean + unblock #19-#36
Closed
#25 M2.1: Rust code generation backend
Closed
#26 M2.2: KRaft reference implementation in Rust
Closed
#27 M3.1: Blog post — "We Formally Verified Kafka's Consensus"
Closed
#23 M1.2: Verify KRaft invariants with Z3
Closed
#24 M1.3: Kafka producer acks and consumer group specs
Closed
#28 M3.2: Show HN launch
Closed
#29 M3.3: Consulting one-pager — "Prove Your Distributed System"
Closed
#31 M4.2: TigerBeetle deep verification
Closed
#32 M4.3: OAuth 2.0 / OIDC flow specification
Closed
#22 M1.1: Write KRaft consensus spec in SpeckDL
Closed
#30 M4.1: Full Raft specification (etcd/Consul)
Closed
#21 M0.3: Implement Z3 verification backend
Closed
#20 M0.2: Add typed IR between AST and generators
Closed
#35 DB.2: SQLitePager.speck — pager state machine spec
Closed
#36 DB.4: SQLiteWAL.speck — WAL concurrency spec
Closed
#18 M0.1: Fix TS generator bugs — clean build for all examples
Closed
#15 Feature: Sale/Price Tracking for WardrobeAI Recommendations
Closed
#33 DB.1: SQLite internals research (pager, WAL, VDBE, B-Tree)
Closed
#34 DB.6: Blog post — "Prove SQLite"
Closed
#12 Implement reference agent (TypeScript)
Closed
#19 M0.1: Delete WAT/WASM generator
Closed
#17 Prove Kafka — Project Plan
Closed
#9 Visually verify all SVG diagrams render correctly
45 issues created by 1 user
Opened
#17 Prove Kafka — Project Plan
Opened
#18 M0.1: Fix TS generator bugs — clean build for all examples
Opened
#19 M0.1: Delete WAT/WASM generator
Opened
#20 M0.2: Add typed IR between AST and generators
Opened
#21 M0.3: Implement Z3 verification backend
Opened
#22 M1.1: Write KRaft consensus spec in SpeckDL
Opened
#23 M1.2: Verify KRaft invariants with Z3
Opened
#24 M1.3: Kafka producer acks and consumer group specs
Opened
#25 M2.1: Rust code generation backend
Opened
#26 M2.2: KRaft reference implementation in Rust
Opened
#27 M3.1: Blog post — "We Formally Verified Kafka's Consensus"
Opened
#28 M3.2: Show HN launch
Opened
#29 M3.3: Consulting one-pager — "Prove Your Distributed System"
Opened
#30 M4.1: Full Raft specification (etcd/Consul)
Opened
#31 M4.2: TigerBeetle deep verification
Opened
#32 M4.3: OAuth 2.0 / OIDC flow specification
Opened
#33 DB.1: SQLite internals research (pager, WAL, VDBE, B-Tree)
Opened
#34 DB.6: Blog post — "Prove SQLite"
Opened
#35 DB.2: SQLitePager.speck — pager state machine spec
Opened
#36 DB.4: SQLiteWAL.speck — WAL concurrency spec
Opened
#37 Unblock Speckl compiler: Fix TS generator bugs so all examples build clean
Opened
#38 [speckl#37.3] Verify all example specs compile clean + unblock #19-#36
Opened
#39 [speckl#37.1] Triage TS generator bugs: enumerate specific bugs with file paths + repros
Opened
#40 [speckl#37.2] Fix top P0+P1 TS generator bugs from #37.1 triage
Opened
#41 [speckl#37.3] B4: Add SpeckDL difference set operator to TS generator rewriteExpr
Opened
#42 [speckl#37.4] B3: Emit real TypeScript if/then/else in TS generator
Opened
#43 [speckl#37.5] B1: Stop silently inventing let/forall stubs in TS generator
Opened
#44 [speckl#37.6] B5: Fix parser init-block handling so generator emits init body
Opened
#45 [speckl#37.7] B2: Forward constraint/verify expressions through TS generator (or evaluate at runtime)
Opened
#46 [speckl#37.8] B6: Add readonly modifier + JSDoc on emitted state variables
Opened
#47 [speckl#37.9] B2.1: Forward constraint expressions through TS generator (rewriteExpr chain)
Opened
#48 [speckl#37.10] B2.2: Implement verifyN() with runtime LTL evaluator (or Z3 call-out)
Opened
#49 Parser: parse input: { name: Type, ... } and output: { ... } record body into fields
Opened
#50 Generator: input/output fields not declared as class properties + bare helper calls + duration/implies literal rewriter gaps
Opened
#51 [CRITICAL — Re-apply lost work] B2.1 constraint forwarding (#47) + #49 multi-line input/output parser, working tree was reset without commit
Opened
#52 [speckl#37.11] B1-redux: Delete preamble heuristic in TS generator emitAction (re-diagnosis)
Opened
#53 [parser] Multi-line Map(K, { ... }) type misparsed line-by-line in parseStateBlock (parser.ts:538)
Opened
#54 [parser] Multi-line verify: bodies truncated in parseMember (parser.ts:422) — blocks B2 PR stack
Opened
#55 [generator] LTL inner-expression identifiers not qualified with this. — input fields + action params out of scope in rewriteExpr
Opened
#56 [wiki] Evidence-Generation page returns HTTP 500 (broken rendering)
Opened
#57 [parser] Multi-line input: { ... } and output: { ... } blocks parse as ident (no fields)
Opened
#58 Z3 generator produces invalid SMT-LIB2 for common constraint idioms
Opened
#59 PROV-O / CycloneDX / SPDX artifacts are shallow — no per-event, per-constraint traceability
Opened
#60 Add protobuf backend — emit .proto from .speckdl so generated bindings replace handwritten APIs (zero glue)
Opened
#61 Parser drops field declarations in record-style interface blocks (only enum variants are captured)