Canonical SPECTER design language specification and multi-target token generation.

Sub-10KB offline decision procedure for equational implication over magmas, distilled from the 4694-law implication graph.

Reworked CATWD 2.0 semantics and cross-domain calibration of K.

Typst template suite for Specter field manuals and public papers.

Lean-native extractor for deterministic theorem-item JSONL used in Wonton Soup corpus workflows.

Offline training and reranking over exported Wonton Soup run traces.

WASM-first egui component library for research dashboards.

Algebraic, round-trippable representations of Lean proof-state tactics.

History-mined benchmark harness for reproducible tinygrad contribution tasks.

Benchmark harness for scoring and verifying Lean sorry tactic proposals.

Deterministic ingestion pipeline for SorryDB-compatible snapshots and benchmark indexes.