Lightkone pilot¶

The first spec pack built from a real product: lightkone, a static web app for keeping a personal library of research papers. The pack lives in packs/kausalflow/lightkone/.

What the pack covers¶

symbolon pack validate packs/kausalflow/lightkone/versions/1 reports 63 obligations (all decided) and 4 assumptions, and every one of the components' 337 checks traces to an obligation.

Results (milestone 2)¶

Five more contracts: citation-key, pdf-filing, library-merge, tidy, and library-file, the data contract for library.json itself (how lightkone reads it and writes it back, byte for byte, with library.bib). Contracts can now share sample data in fixtures/, including raw text files with {"$text": ...}; library-file ships three sample libraries.

How it went:

1. Second build, second language. A fresh Claude Code session (Claude Opus 5.5, the same model as the Python build, with no access to it) got only versions/1/ and built all eight components in Go (standard library only), with lightkone, the oracle and the Python rebuild moved off the machine. It passed all eight contracts and all eight holdouts.
2. Passing is not agreeing. oracle/differential.py sends the same generated inputs to lightkone and the Go build and reports every disagreement on inputs the contract accepts. On about 5,000 inputs, six contracts agreed completely. bibtex-import and search-query showed five real gaps that both the spec and the holdout had missed:
3. a malformed BibTeX field skipped to a } ends the entry, but one skipped to a comma does not (the contract said the rest was always lost);
4. "whitespace" means JavaScript's \s, including no-break space and U+2028;
5. the arXiv URL match ignores case, so V3 and .PDF are stripped;
6. year: terms that are not numbers do not count, and do not replace an earlier one;
7. title sort is Unicode collation (localeCompare), not code-point order.
8. Tightened and rebuilt. The contracts now state each rule, with 18 new examples recorded from lightkone. The Go builder revised from the new text alone (adding golang.org/x/text for collation) and passes. The differential test then found no disagreement on search-query within scope, and 11 in 2,000 heavily mutated BibTeX files, all deliberately broken input (unbalanced braces, a value starting with #); those are left for a later version.
9. Evidence. Runner A attested lightkone and the Go build on all eight contracts; runner B re-ran all sixteen in fresh containers with identical outcomes. The Python build's milestone 1 attestations are kept: they are for the earlier digests of search-query and bibtex-import.

The pack now has 63 obligations, all decided. Four defaults that were lightkone bugs are fixed and decided: papers in the trash are left out of library.bib, and top-level keys of library.json that lightkone does not use are kept on save (lightkone#51); a user folder named in capitals (ML, 2019) is no longer taken for a Paperpile author folder unless it is an author's surname, and blank DOIs no longer match each other in tidy (lightkone#52). On 2026-10-24 kausalflow settled the last five: an empty journal no longer hides the booktitle as the venue, and a library.json saved by a newer lightkone is refused rather than read as version 1 (lightkone#53); a mistyped year: filter still filters nothing, title sort keeps Unicode collation, and import keeps JavaScript's whitespace set.

Two Symbolon bugs turned up and are fixed: examples containing U+2028 were split into two lines, and the container sandbox removed the execute bit, so no compiled implementation could run.

Results (milestone 1)¶

1. Oracle check. Examples were recorded by running lightkone's own code through the command protocol. The properties were written from the description, and lightkone passed all of them.
2. Replication. An AI builder got only versions/1/, with lightkone's source and the oracle moved off the machine. It passed all three contracts, then passed the holdout: a different property seed, 5× the generated cases, and 18 examples it never saw.
3. Divergence found. Comparing the two builds on the builder's listed ambiguities found one real gap in how repeated year: filters combine. The contract now states the rule, with a property and two examples for it, and both builds pass it.
4. Reproduction. A second runner key re-ran all six attestations in a fresh container, and every check had the same outcome.
5. Kill rate. Plausible wrong versions of the rebuild live in examples/mutants/lightkone/, outside the pack so the component digests stay put. search-query rejects 8 of 9; the one survivor ignores a malformed year: term, which is exactly what the open obligation search.year-malformed leaves to the builder. bibtex-export rejects 7 of 7. bibtex-import rejects 7 of 8; the survivor reads a two-digit year like 99 as a number, which the description rules out but no check covers, so it is a gap for the next pack version.

Measuring the remaining ambiguity¶

symbolon diff turns the milestone 2 differential test into a command that works on any number of builds (see Measuring ambiguity). Run on search-query with lightkone as the reference and both rebuilds, it puts the Go build at distance 0 from lightkone. It finds the two rules milestone 2 tightened, search.year-malformed and search.title-sort-other, as the splits between the milestone 1 Python build and the other two. On bibtex-import, after the importer fix in kausalflow/lightkone#50, it finds no disagreement between lightkone and the Go build.

Re-running the evidence¶

cd packs/kausalflow/lightkone
symbolon pack validate 1
symbolon verify attestations/search-query.go-1.json --trust attestations/runner-a.pub \
  --contract versions/1/components/search-query/versions/1 --impl rebuilds/go-1/search-query --rerun

The pack's own README.md has the full notes, including the three importer bugs the contracts found, now fixed in lightkone#50.