HN, formally / loop

How HN, formally works

Every night a language model redesigns the front page from a design brief: sixteen candidates in parallel, each a new renderer and stylesheet. A candidate ships only if the Lean 4 kernel accepts its proof that, for every possible Hacker News API input, the bytes it emits encode a page with the right structure, the right data, and no injected content; that theorem, and nothing beyond it, is what "proven" means here. Each passer is then checked in a browser for contrast, reflow at 375px, HTML validity and accessibility violations (run per release, never proven), and a vision model ranks what is left on adherence to the brief, novelty against the live site, and craft. The winner ships without human review. Every generation is below, with its proof, screenshots, scores and cost; new ones appear in the Atom feed.

Releases
–
Runs
–
Spec version
–
Total spend
–

Current release

The build serving the site right now.

Loading…

Newest first. Every release passed tier 1 and tier 2; the judge only ranks.

Run history

Every redesign run, including the ones that produced nothing. Expand a run to see each candidate's last error.

Run Candidates Tier 1 Tier 2 Released Cost Stop reason

What is proven, what is checked, what is trusted

Static text, maintained by hand from DESIGN.md. It does not change when a release ships.

Tier 1 Proven in Lean 4

Checked by the Lean kernel. No native_decide, no axioms beyond propext, Classical.choice, Quot.sound; CI verifies the axiom set of render_ok on every build.

  • Structure: 30 items in API rank order; each item's title, url, domain, points, author, age and comments link; the "More" link.
  • The full comment tree at any depth, with parent/child nesting preserved.
  • Data fidelity to the API: every rendered value comes from the item it belongs to.
  • Landmark, heading and link-name structure.
  • No injection: the API's HTML fragments pass through a verified allowlist parser (p, a, i, code, pre, br, entities).
  • Content gate: every text node in the rendered tree is a substring of the API payload or a member of a fixed allowlist of nav/footer strings.
  • A proven DOM-to-HTML serializer, so the bytes on disk encode exactly the proven tree.
  • The Item type covers all five API types (job, story, comment, poll, pollopt) with optional fields; the theorem quantifies over all of them, including deleted and dead items.

Tier 2 Checked per release, in a browser

Run by the orchestrator with Playwright and Chromium on the rendered output. A release must pass all of them. Never called "proven".

  • Contrast: every text node's computed foreground/background ratio is at least 4.5:1 (3:1 at 24px and above).
  • Reflow: at a 375px viewport the document does not scroll horizontally.
  • HTML validity: vnu.jar reports zero errors on every page.
  • Accessibility: axe-core reports zero serious or critical violations on the front page and three item pages.
  • Content-Security-Policy simulation: no scripts, no inline styles, no external origins in the computed stylesheet.

Trusted Not proven, assumed correct

  • The Lean 4 kernel (checks the proof).
  • The Lean compiler and runtime (the proof is about the source; the compiled binary produces the bytes).
  • Lean's JSON decoder into the Item type.
  • The fetcher (HN Firebase API to data JSON).
  • GitHub Actions.
  • The operating system.

Everything else in the pipeline is covered by the theorem. The judge (a vision model scoring screenshots) ranks passers and never blocks a release.