Broken websites don't build.

NoGoals is a static site generator written in Lean 4. Types and proofs guarantee routes, output paths and bilingual completeness. An audit checks links, CSP, SEO and published URLs in the emitted files. If the audit fails, the output directory remains unchanged.

Theorem, sorry and build-gate counts

theorems
167
sorries
0
build gates
15

Theorems and sorries are counted by verify.sh, which fails on drift. The gate count is read from the code that built this page. All of these counts are generated automatically.

How it works

Most static site generators hold links and images as strings. A string can point anywhere, and nothing stops a typo.

NoGoals is written in Lean 4. Each site defines a closed type for its pages, and the scaffold includes one. Links name constructors of this type. A link to a nonexistent page causes a compile error.

During an audit, the link gate resolves every href in the emitted files, including hand-written HTML.

String-based references
href : String
-- "/about"
-- "/prodcuts"             a typo, and it ships
-- "javascript:alert(1)"   ships too
Typed values
target : PageId     -- a page that exists
src    : AssetPath  -- path syntax checked at the literal
title  : L          -- a Japanese AND an English field
date   : IsoDate    -- a real calendar date
-- a wrong value is a compile error, with a line number

Verification methods

  • Guarantees enforced by types

    The types prevent invalid states from being represented. A link names a constructor of the site's page type. Slugs, asset paths and dates are literals whose syntax is checked at compile time. Editorial text is a record with a Japanese and an English field, so neither can be left out.

  • Guarantees proved by theorems

    Lean's kernel checks the proofs. For every site the generator accepts, no two outputs share a path, every page is emitted, and every page exists in both languages. Inside the verified renderer, an emitted link resolves to an emitted file.

  • Build-time checks

    With --audit, a parser that follows browsers' HTML rules reads the emitted files. The audit checks that every link and asset reference resolves, that pages comply with the delivered CSP, and that canonical and hreflang match the routes. It also checks HTML validity and whether every published URL is still live or redirected. If any gate fails, no files are copied to the output directory.

The report says which tier each claim belongs to. A build without --audit runs no gates, and its report says so: a check that did not run is shown as skipped, never as passed.

See the full list of checks

When a build fails

Say a page's URL is changed and one hand-written link to the old URL is left behind.

Output of an audited build (example)
$ ./scripts/build.sh --audit
  …
  ✗ links: every internal reference on 12 pages resolves:
      pricing/index.html: <a href="/plans/">: no emitted file at plans/index.html
  ✓ seo: canonical/hreflang/og on 12 route pages
  …
  ✗ permalinks: all 31 obligations live or redirected (permalinks_sound applies); _redirects rendered from the same map:
      previously published URL would 404: plans/index.html (add a redirect or restore the page)

✗ AUDIT FAILED — violations above; the previous build stays in place.
  …
✗ BUILD REJECTED: a gate failed. build/ is UNTOUCHED (last green build).

The previous successful build remains in place. The failed candidate is kept separate, and its receipt records the gate that failed. The receipt is machine-readable, so a deployment script can reject any receipt that does not record a successful full audit.

This site's verification results

This site is built with NoGoals. The badge in the footer links to this build's verification page.

This build's verification pageevery guarantee, its tier, and the theorem behind it

Get started