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

Implementation for reworking CATWD 2.0 semantics and calibrating K across domains to better understand its properties.

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

Offline training and reranking over exported Wonton Soup run traces.

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

Benchmark harness for Lean `sorry` tactic proposals, with split policy, scoring, and verification protocols.

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

WASM-first `egui` component library for dashboard-grade research visualization.

Reproducible benchmark design for LLM contribution quality on tinygrad and related codebases.

Typst template suite for Specter field manuals and public papers, with shared tokens and reproducible build routing.