From 944f60e8db3dd01e2c9a8209eabe8bd94f3ca9da Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 09:01:15 +0200
Subject: [PATCH 01/29] mobile(docs): tighten typography rhythm + reading-list
 layout
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Audit of every page at 390x844 surfaced a handful of subtle mobile
rough edges. This batch:

  * Reading-list rows on the homepage no longer orphan their →
    arrow to a new line. Grid is now 2 cols × 2 rows: title + arrow
    on row 1, note as a quieter second line.
  * Inline-code chips switch from `overflow-wrap: anywhere` to
    `break-word` so long paths like
    Compiler/Proofs/IRGeneration/Contract.lean break at natural
    boundaries (slash, dot, dash) rather than producing single-letter
    orphans on the next line.
  * Hero dek → CTA spacing tightened on phones (1rem / 1.5rem)
    instead of the previous 1.4 / 2.25rem rhythm — felt over-aired
    when the page is narrow.
  * Breadcrumb on doc pages drops to 0.7rem with looser tracking
    and lower opacity so it reads as a spine locator rather than a
    second label above the h1.
  * Phone-only h2 / h3 sizing tuned for legibility without
    competing with the hero-class h1: clamp(1.55, 6vw, 1.95rem) for
    h2 and 1.22rem for h3. Chip-style h3s (an inline-code
    identifier as the heading, as on the EDSL reference) get a
    capped 0.95em chip size so they don't overshoot the line-height.
  * Secondary hero links get a 1.85rem min-height so they're a
    comfortable tap target without changing weight.
---
 docs-site/app/verity-site.css | 76 +++++++++++++++++++++++++++++++----
 1 file changed, 69 insertions(+), 7 deletions(-)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index 9093271fd..b3a2e30af 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -869,9 +869,13 @@ code.nextra-code:not(pre code) {
   padding: 0.05em 0.36em !important;
   /* Allow line-break inside long inline-code identifiers so they
      don't push the surrounding paragraph past the gutter on narrow
-     viewports. */
+     viewports. `break-word` (without anywhere) breaks at natural
+     boundaries first — slashes, dots, dashes — and only resorts to
+     mid-character when nothing else fits, avoiding single-letter
+     orphans like ".lea / n". */
   word-break: break-word;
-  overflow-wrap: anywhere;
+  overflow-wrap: break-word;
+  hyphens: none;
 }
 
 .dark article :not(pre) > code,
@@ -1588,11 +1592,29 @@ input:focus-visible,
 }
 
 @media (max-width: 767px) {
+  /* On phones, lay the reading-list row as a single column. The title
+     goes on top with the arrow right-aligned next to it, and the note
+     drops below as a quiet second line. Previously the arrow was
+     orphaning to its own line because grid-row was constraining it. */
   .verity-reading-list__row {
-    grid-template-columns: 1fr auto;
+    grid-template-columns: 1fr auto !important;
+    grid-template-rows: auto auto;
+    gap: 0.15rem 0.6rem;
+    padding: 0.95rem 0.2rem !important;
+  }
+  .verity-reading-list__title {
+    grid-column: 1;
+    grid-row: 1;
+  }
+  .verity-reading-list__arrow {
+    grid-column: 2;
+    grid-row: 1;
+    align-self: center;
   }
   .verity-reading-list__note {
-    grid-column: 1 / -1;
+    grid-column: 1 / -1 !important;
+    grid-row: 2;
+    font-size: 0.92rem !important;
   }
 }
 
@@ -1672,7 +1694,25 @@ input:focus-visible,
 
   article main {
     font-size: 1rem !important;
-    line-height: 1.68 !important;
+    line-height: 1.7 !important;
+  }
+
+  article main h2 {
+    font-size: clamp(1.55rem, 6vw, 1.95rem) !important;
+    margin-top: 2.5rem !important;
+    padding-top: 1rem !important;
+  }
+
+  article main h3 {
+    font-size: 1.22rem !important;
+    margin-top: 1.85rem !important;
+  }
+
+  /* Allow chip-style h3s (an inline-code identifier as the heading) to
+     not blow up the line-height by capping their inline-code size on
+     phones. */
+  article main h3 :not(pre) > code {
+    font-size: 0.95em !important;
   }
 
   article main > :not(.verity-hero):not(.code-compare):not(.report-callout) {
@@ -1715,7 +1755,15 @@ input:focus-visible,
   .verity-hero {
     padding-top: 1.25rem;
     padding-bottom: 1.5rem;
-    gap: 1.75rem;
+    gap: 1.25rem;
+  }
+
+  .verity-hero__head > h1 + .verity-hero__dek {
+    margin-top: 1rem;
+  }
+
+  .verity-hero__head > .verity-hero__dek + .verity-hero__links {
+    margin-top: 1.5rem;
   }
 
   .verity-hero__head {
@@ -1748,7 +1796,21 @@ input:focus-visible,
 
   .verity-hero__more {
     flex-direction: column;
-    gap: 0.35rem;
+    gap: 0.45rem;
+  }
+
+  .verity-hero__more a {
+    /* Bigger tap target on phones without changing visual weight. */
+    padding: 0.2rem 0;
+    min-height: 1.85rem;
+  }
+
+  /* Quieter breadcrumb on doc pages so it reads as a small spine
+     locator rather than a competing label above the h1. */
+  .nextra-breadcrumb {
+    font-size: 0.7rem !important;
+    letter-spacing: 0.04em;
+    opacity: 0.85;
   }
 
   .code-compare {

From 96de6e8f3ebfa6c24566ac3c3c43f6ef2a98d347 Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 09:05:59 +0200
Subject: [PATCH 02/29] mobile(docs): right-edge fade on every overflowing code
 block

The previous pass only put a scroll-fade on the homepage's
CodeCompareSwitcher panels. On the rest of the docs (getting-started,
EDSL reference, examples, guides) shiki pre blocks were still
clipping their long lines at the chip border without any affordance.

Apply the same 1.5rem teal-to-transparent gradient to every
figure[data-rehype-pretty-code-figure] on phones, so the scroll
gesture is suggested everywhere code overflows.
---
 docs-site/app/verity-site.css | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index b3a2e30af..f5a7d793d 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -1844,18 +1844,22 @@ input:focus-visible,
   }
 
   /* Fade the right edge of horizontally-scrolling code so it reads as
-     scrollable rather than cut-off. */
-  .code-switcher__panels {
+     scrollable rather than cut-off. The same treatment applies to
+     stand-alone shiki figures (getting-started, EDSL reference, etc.)
+     where a long line otherwise just clips at the chip border. */
+  .code-switcher__panels,
+  figure[data-rehype-pretty-code-figure] {
     position: relative;
   }
 
-  .code-switcher__panels::after {
+  .code-switcher__panels::after,
+  figure[data-rehype-pretty-code-figure]::after {
     content: "";
     position: absolute;
-    top: 0;
-    right: 0;
-    bottom: 0;
-    width: 1.75rem;
+    top: 1px;
+    right: 1px;
+    bottom: 1px;
+    width: 1.5rem;
     pointer-events: none;
     background: linear-gradient(
       to right,

From f42f28700116ab571c884fce1246b920db0cc6e5 Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 09:08:47 +0200
Subject: [PATCH 03/29] mobile(docs): pagination tap, numbered-list polish,
 chip border weight
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Bottom-of-page next/prev pagination gets a 2.6rem min-height with
  vertical padding so a finger has a comfortable target without the
  chevron / label feeling disconnected.
- Ordered lists in the article body switch to tabular lining
  numerals (font-feature-settings: tnum, lnum) so "1." through
  "10." line up cleanly under each other in a numbered list — the
  same alignment a LaTeX enumerate environment gives by default.
  ::marker pseudo gets a muted color so the digits read as a
  numbering scheme rather than competing chrome.
- Inline-code chip border-color softened to ~45% rule on phones so
  dense paragraphs (research, EDSL reference) don't read as a wall
  of small boxes.
- Lead paragraph after h1 gains explicit lining-numeral typography
  so any digit in the abstract sits on the baseline instead of the
  Source Serif default old-style figures we use elsewhere.
---
 docs-site/app/verity-site.css | 39 ++++++++++++++++++++++++++++++++++-
 1 file changed, 38 insertions(+), 1 deletion(-)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index f5a7d793d..361234b20 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -569,7 +569,11 @@ article main h1 {
 }
 
 /* Lead paragraph — the first paragraph after the h1 — gets a touch more
-   air and a slightly lighter weight, like a preprint abstract opener. */
+   air and a slightly lighter weight, like a preprint abstract opener.
+   `font-feature-settings: "lnum"` enables lining numerals so any digit
+   in the abstract sits on the baseline like normal text rather than
+   defaulting to old-style figures the serif's onum feature applies
+   elsewhere in the article. */
 article main h1 + p {
   font-size: 1.18rem !important;
   line-height: 1.6 !important;
@@ -579,6 +583,7 @@ article main h1 + p {
   margin-top: 0.6rem !important;
   margin-bottom: 1.8rem !important;
   max-width: 44rem !important;
+  font-feature-settings: "kern", "liga", "calt", "lnum";
 }
 
 article main h2 {
@@ -1715,6 +1720,38 @@ input:focus-visible,
     font-size: 0.95em !important;
   }
 
+  /* Pagination row at the bottom of every doc page — wider tap area
+     plus a tiny extra height so a hurried finger can still hit
+     "Example Contracts" without zooming in. Also widen the visible
+     hit-state so both the chevron and label feel like one button. */
+  article > div:last-child > a[title] {
+    padding: 0.85rem 0 !important;
+    min-height: 2.6rem;
+    display: inline-flex;
+    align-items: center;
+  }
+
+  /* Numbered lists in articles (e.g. the "What to read next" list at
+     the bottom of getting-started) get monospace-figured numerals so
+     they line up cleanly under each other — small but very
+     research-paper. */
+  article main ol {
+    font-feature-settings: "tnum", "lnum";
+  }
+
+  article main ol > li::marker {
+    color: var(--verity-muted);
+    font-weight: 500;
+  }
+
+  /* Lighten the inline-code chip border on phones so dense
+     paragraphs (research / EDSL reference) don't read as a wall of
+     boxes. */
+  article :not(pre) > code,
+  code.nextra-code:not(pre code) {
+    border-color: color-mix(in srgb, var(--verity-rule) 45%, transparent) !important;
+  }
+
   article main > :not(.verity-hero):not(.code-compare):not(.report-callout) {
     max-width: 100%;
   }

From 3b76ebec9fe7ad2a80aba4d7a2ad22d7249af149 Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 09:13:40 +0200
Subject: [PATCH 04/29] mobile(docs): chip ellipsis instead of mid-word break
 on long paths
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Previously inline-code chips with paths longer than the article
column (e.g. Compiler/Proofs/IRGeneration/Contract.lean) wrapped via
overflow-wrap: break-word and dropped one orphan letter onto the next
line — "Contract.lea" / "n". This batch:

  * Chips are now inline-block + nowrap + overflow:hidden +
    text-overflow:ellipsis, so a path that doesn't fit gets a clean
    ellipsis at the end rather than a mid-word break.
  * Drops chip font-size to 0.8em on phones so most real paths in
    the docs (Verity/Specs/<Name>/Spec.lean, etc.) fit in the line
    without the ellipsis kicking in at all.
  * Chip-style h3 headings (getStorage / setStorage on the EDSL
    reference) opt out of overflow:hidden so the heading shows the
    whole identifier.
---
 docs-site/app/verity-site.css | 24 +++++++++++++++++++++++-
 1 file changed, 23 insertions(+), 1 deletion(-)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index 361234b20..8157f4937 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -1746,10 +1746,32 @@ input:focus-visible,
 
   /* Lighten the inline-code chip border on phones so dense
      paragraphs (research / EDSL reference) don't read as a wall of
-     boxes. */
+     boxes. And shrink the chip a hair so long file paths like
+     `Compiler/Proofs/IRGeneration/Contract.lean` fit on a single
+     line in the article column instead of orphaning a single letter
+     ("Contract.lea" + "n") to the next line. */
   article :not(pre) > code,
   code.nextra-code:not(pre code) {
     border-color: color-mix(in srgb, var(--verity-rule) 45%, transparent) !important;
+    font-size: 0.8em !important;
+    padding: 0.05em 0.32em !important;
+    /* Treat the chip as an atomic inline-block: it either fits on the
+       current line or wraps as a whole to a new line. This kills the
+       "one orphan letter" wrap that was happening when a path got
+       broken mid-word as a last resort. */
+    display: inline-block;
+    max-width: 100%;
+    white-space: nowrap;
+    overflow: hidden;
+    text-overflow: ellipsis;
+    vertical-align: baseline;
+  }
+
+  /* For chip-style h3 headings (e.g. `getStorage` / `setStorage`) we
+     still want the chip to wrap as a whole rather than be ellipsised. */
+  article main h3 :not(pre) > code {
+    text-overflow: clip !important;
+    overflow: visible !important;
   }
 
   article main > :not(.verity-hero):not(.code-compare):not(.report-callout) {

From 1d5cd3fddef463d0fd0a754a4386dfb8b7b0dd2e Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 09:16:21 +0200
Subject: [PATCH 05/29] mobile(docs): keep table cells uncut + tabular numerals
 on tables

- Chips inside <td>/<th> opt out of the article-column overflow
  ellipsis so the path stays readable in the cell when the user
  horizontally scrolls the table.
- Tables get tabular lining numerals so columns of digits (iteration
  #, line counts, theorem counts) align cleanly row-to-row.
- Native horizontal scrollbar inside tables picks up the same teal
  6px treatment we already use on code blocks.
---
 docs-site/app/verity-site.css | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index 8157f4937..252680520 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -1774,6 +1774,17 @@ input:focus-visible,
     overflow: visible !important;
   }
 
+  /* Inside table cells the article-column ellipsis doesn't help —
+     the table already provides horizontal scroll. Let chips show full
+     text there so a hurried reader sees the path without scrolling
+     past the chip ellipsis they couldn't tap on. */
+  article main td :not(pre) > code,
+  article main th :not(pre) > code {
+    overflow: visible !important;
+    text-overflow: clip !important;
+    white-space: nowrap !important;
+  }
+
   article main > :not(.verity-hero):not(.code-compare):not(.report-callout) {
     max-width: 100%;
   }
@@ -1931,6 +1942,20 @@ input:focus-visible,
     display: block;
     overflow-x: auto;
     -webkit-overflow-scrolling: touch;
+    /* Tabular numerals so columns of digits (Iteration #, etc.) stay
+       aligned across rows. */
+    font-feature-settings: "tnum", "lnum";
+    /* Thin teal scrollbar to match code blocks. */
+    scrollbar-width: thin;
+    scrollbar-color: color-mix(in srgb, var(--verity-accent) 30%, transparent) transparent;
+  }
+
+  article main table::-webkit-scrollbar {
+    height: 6px;
+  }
+
+  article main table::-webkit-scrollbar-thumb {
+    background: color-mix(in srgb, var(--verity-accent) 30%, transparent);
   }
 
   /* The serif body uses hyphenation; on narrow screens this can

From 62544e27b6df1cadd3d30d9154e2c757f3695f51 Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 09:17:28 +0200
Subject: [PATCH 06/29] ui(docs): scroll-margin on headings + reduced-motion
 respect

Two small accessibility wins that show up most clearly on mobile:

  * Every heading gets scroll-margin-top equal to the navbar height
    plus a 0.75rem breathing room, so jumping to a section via the
    TOC or an in-page #anchor link lands the heading visibly below
    the sticky navbar instead of behind it. Particularly visible on
    long reference pages (EDSL, verification) where readers
    pogo-stick between sections.
  * Smooth scrolling on the whole document for those anchor jumps,
    which is now actively useful instead of jarring.
  * Honour prefers-reduced-motion: snap-scroll instead of smooth,
    and cut transitions to ~0ms so users who opted out get a
    static-feeling site.
---
 docs-site/app/verity-site.css | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index 252680520..31da3d2c4 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -105,6 +105,24 @@ html[dir] {
   background: var(--verity-bg);
   font-family: var(--verity-font-prose);
   text-rendering: optimizeLegibility;
+  /* Smooth scrolling for TOC anchor jumps; in conjunction with the
+     scroll-margin-top on h2/h3 this means clicking a TOC entry slides
+     the section heading into view under the sticky navbar instead of
+     snapping abruptly behind it. */
+  scroll-behavior: smooth;
+}
+
+/* Honour user preference for reduced motion: turn off smooth scroll
+   and the slide-in transitions on CTAs / arrows / panels. */
+@media (prefers-reduced-motion: reduce) {
+  html, html:root, html[dir] {
+    scroll-behavior: auto;
+  }
+
+  *, *::before, *::after {
+    animation-duration: 0.01ms !important;
+    transition-duration: 0.01ms !important;
+  }
 }
 
 body {
@@ -559,6 +577,13 @@ article main h6 {
   line-height: 1.16 !important;
   text-wrap: balance;
   border: 0 !important;
+  /* Anchor links / TOC clicks jump to a section heading. Without
+     scroll-margin the heading lands flush against the top of the
+     viewport (and on doc pages it slides under the sticky navbar).
+     Push the scroll target down by the navbar height + a small
+     breathing-room offset so the heading reads as the top of its
+     section. */
+  scroll-margin-top: calc(var(--nextra-navbar-height, 64px) + 0.75rem);
 }
 
 article main h1 {

From c0a6dbcfbcac8e67d6d2315ab0119802fb71857b Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 09:18:44 +0200
Subject: [PATCH 07/29] typography(docs): text-wrap pretty, hairline link
 underlines, teal tap
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Body paragraphs opt into text-wrap: pretty so the last few lines
  balance instead of leaving a one-word widow at the end of a
  long-form section.
- Inline links use 1px text-decoration-thickness so the underline
  reads as a hairline rule instead of fighting the serif's stroke
  weight (the previous 2px default from the browser was just enough
  to make every link feel boxy on mobile).
- iOS Safari's grey tap-highlight rectangle is replaced with a faint
  teal that matches the palette — the tap feedback now reads as
  "selected" rather than "rendered with default chrome".
---
 docs-site/app/verity-site.css | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index 31da3d2c4..c4ec381b1 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -130,6 +130,9 @@ body {
   background: var(--verity-page);
   color: var(--verity-ink);
   font-family: var(--verity-font-prose);
+  /* iOS Safari's default tap highlight is a translucent grey rect;
+     replace with a faint teal that matches the palette. */
+  -webkit-tap-highlight-color: color-mix(in srgb, var(--verity-accent) 18%, transparent);
 }
 
 [class*="x:text-blue"],
@@ -561,6 +564,10 @@ article main p {
   font-size: 1.045rem !important;
   line-height: 1.72 !important;
   color: var(--verity-ink) !important;
+  /* Modern browsers: `text-wrap: pretty` lets the browser balance the
+     last few lines of a paragraph so we don't end on a single
+     "widow" word. Falls back gracefully on Safari. */
+  text-wrap: pretty;
 }
 
 article main h1,
@@ -685,6 +692,9 @@ article main a {
   font-weight: 600;
   text-decoration-color: color-mix(in srgb, var(--verity-accent) 45%, transparent) !important;
   text-underline-offset: 0.16em;
+  /* Finer hairline-style underline that doesn't fight the serif. */
+  text-decoration-thickness: 1px;
+  -webkit-tap-highlight-color: color-mix(in srgb, var(--verity-accent) 15%, transparent);
 }
 
 article a:hover,

From 481c55129d1251b82e1c4d33a73312cfb2fd6634 Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 09:22:31 +0200
Subject: [PATCH 08/29] ui(docs): tap feedback for hero CTAs + heading anchors
 polish
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Hero "Start with a contract" and "Read the paper" buttons get a
  visible :active state so a finger tap on a phone reads as
  "pressed" (1px Y translate + tinted background). Hover doesn't
  cover touch.
- The `#` subheading anchor (Nextra's per-heading link) fades in
  instead of snapping, and on phones (where there's no hover) we
  hide it entirely — it was reserving gutter space we couldn't use.
---
 docs-site/app/verity-site.css | 35 +++++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index c4ec381b1..3766827c8 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -707,6 +707,29 @@ article main a:hover,
 
 .subheading-anchor {
   color: var(--verity-muted) !important;
+  /* The Nextra subheading anchor is a `#` that appears beside a
+     heading on hover (desktop). Subtly fade it in so it doesn't
+     blink-attack the reader, and on mobile (where the heading is
+     never hovered) keep it hidden so we don't reserve gutter space
+     for it. */
+  opacity: 0;
+  transition: opacity 0.15s ease;
+}
+
+article main h1:hover .subheading-anchor,
+article main h2:hover .subheading-anchor,
+article main h3:hover .subheading-anchor,
+article main h4:hover .subheading-anchor,
+article main h5:hover .subheading-anchor,
+article main h6:hover .subheading-anchor,
+.subheading-anchor:focus-visible {
+  opacity: 1;
+}
+
+@media (max-width: 767px) {
+  .subheading-anchor {
+    display: none !important;
+  }
 }
 
 /* The right-rail "Question? Give us feedback / Edit this page" footer
@@ -1194,6 +1217,18 @@ input:focus-visible,
   transform: translateX(0.18rem);
 }
 
+/* Tap feedback on phones — :hover is unreliable on touch, so give
+   both buttons a visible :active state that reads as "pressed". */
+.verity-hero__cta:active {
+  transform: translateY(1px);
+  background: var(--verity-accent-strong, var(--verity-accent)) !important;
+}
+
+.verity-hero__paper:active {
+  transform: translateY(1px);
+  background: color-mix(in srgb, var(--verity-accent) 18%, transparent) !important;
+}
+
 .verity-hero__cta:focus-visible,
 .verity-hero__more a:focus-visible {
   outline: 2px solid var(--verity-accent);

From ab197fbab45d5abf284b34d635773299ba8ccaeb Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 09:26:30 +0200
Subject: [PATCH 09/29] mobile(docs): disable hyphenation inside table cells

Short table-cell labels like "property tests" or "Solidity testing
framework" were getting hyphenated as "prop-/erty" / "test-/ing" on
phones. Hyphenation makes sense in justified body prose but reads
as truncation on table-cell labels that have plenty of column width
to wrap whole-word. Force hyphens: manual on td/th in the mobile
media block so wraps land between words instead of inside them.
---
 docs-site/app/verity-site.css | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index 3766827c8..bfe687f74 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -2028,6 +2028,16 @@ input:focus-visible,
     background: color-mix(in srgb, var(--verity-accent) 30%, transparent);
   }
 
+  /* Don't hyphenate inside table cells on phones — wrapping a short
+     word like "property" as "prop-/erty" reads as truncated text on
+     a phone screen and the column has the width to wrap naturally
+     instead. */
+  article main td,
+  article main th {
+    hyphens: manual !important;
+    -webkit-hyphens: manual !important;
+  }
+
   /* The serif body uses hyphenation; on narrow screens this can
      hyphenate every other line. Loosen so words break only on the rare
      overflow case. */

From 5da380044594c8ec2b3029c5f0bb78cd2cb2fdb8 Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 09:31:16 +0200
Subject: [PATCH 10/29] typography(docs): paper-style hr ornament + en-dash
 list markers
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Two small typographic touches that pull the docs closer to a
printed-paper feel:

  * <hr> rules are no longer 1px hairlines but a centred three-dot
    asterism ("· · ·") at the muted rule color, like a section
    break in a published paper. The rule itself is suppressed so
    the dots stand alone.
  * Unordered-list bullets become quiet en-dashes (–) rendered via
    a ::before pseudo so the existing markup keeps working. Nested
    sub-lists get a smaller middle-dot (·) so the hierarchy still
    reads. Ordered lists keep their numerals (with tabular figures
    from the previous pass).
---
 docs-site/app/verity-site.css | 54 ++++++++++++++++++++++++++++++++++-
 1 file changed, 53 insertions(+), 1 deletion(-)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index bfe687f74..c19652a4b 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -829,7 +829,59 @@ article > div:last-child > a[title]:hover svg {
 }
 
 article main hr {
-  border-color: var(--verity-rule);
+  border: 0;
+  height: 0;
+  margin: 2.5rem auto;
+  /* A centred dingbat-style rule: three small teal asterisms, like
+     a section break in a printed paper. Uses ::before with a flexible
+     content string so we don't need extra markup. */
+  text-align: center;
+  overflow: visible;
+  color: var(--verity-muted);
+}
+
+article main hr::before {
+  content: "·   ·   ·";
+  display: inline-block;
+  letter-spacing: 0.3em;
+  font-size: 1.1rem;
+  color: var(--verity-rule);
+}
+
+.dark article main hr::before {
+  color: var(--verity-rule);
+}
+
+/* Unordered-list bullet styling — replace the default round bullet
+   with a quieter en-dash so paragraphs in bulleted lists read as
+   research-paper enumerations instead of generic UI lists. Leaving
+   it on `::marker` keeps the bullet inline with the first line
+   without affecting indent. */
+article main ul {
+  list-style: none;
+  padding-left: 1.4rem;
+}
+
+article main ul > li {
+  position: relative;
+}
+
+article main ul > li::before {
+  content: "–";
+  position: absolute;
+  left: -1.1rem;
+  color: var(--verity-muted);
+  font-weight: 500;
+}
+
+/* Don't touch the nested list markers — they're rare and the default
+   is fine. */
+article main ul ul > li::before,
+article main ol ul > li::before {
+  content: "·";
+  left: -1rem;
+  font-size: 1.2em;
+  line-height: 1;
 }
 
 article main table {

From 0c0a0dfe0e8c7af7c43c7e3a324c34f75c59243b Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 09:34:40 +0200
Subject: [PATCH 11/29] mobile(docs): bigger paper icon inside "Read the paper"
 CTA
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

At 14×14 the paper SVG read as a tiny outline next to the label on
a phone. Bumping to 16×20 (1rem×1.25rem) lets the rectangle and
fold corner actually read as a document, matching the visual
weight of the arrow on the primary CTA next to it.
---
 docs-site/app/verity-site.css | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index c19652a4b..c0ff874a2 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -1986,6 +1986,13 @@ input:focus-visible,
     min-height: 2.85rem;
   }
 
+  /* Slightly bigger paper icon on phones so the CTA reads as
+     "open this PDF" rather than "view a tiny outline of paper". */
+  .verity-hero__paper svg {
+    width: 1rem;
+    height: 1.25rem;
+  }
+
   .verity-hero__more {
     flex-direction: column;
     gap: 0.45rem;

From aab9d710d87a8330d9fb93f1064b1498bf7e4c62 Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 09:36:29 +0200
Subject: [PATCH 12/29] docs(site): style <details>/<summary> for future
 collapsible content
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Currently unused in content but content authors should be able to drop
in a <details><summary> block (FAQ, "Show proof", debugger output) and
get a paper-rule treatment for free: 1px rule top + bottom, a teal
triangle that rotates 90° on open, no native browser arrow.
---
 docs-site/app/verity-site.css | 51 +++++++++++++++++++++++++++++++++++
 1 file changed, 51 insertions(+)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index c0ff874a2..4e1424c85 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -828,6 +828,57 @@ article > div:last-child > a[title]:hover svg {
   transform: translateX(0.15rem);
 }
 
+/* Disclosure widgets — <details><summary> — render as quiet
+   research-paper "footnote" blocks: a 1px rule top + bottom, a
+   teal triangle marker, and content padded under the summary.
+   Currently unused in content but ready for FAQ-style or
+   "Show proof" expanders. */
+article main details {
+  margin: 1.25rem 0;
+  border-top: 1px solid var(--verity-rule);
+  border-bottom: 1px solid var(--verity-rule);
+  padding: 0.85rem 0;
+}
+
+article main details > summary {
+  cursor: pointer;
+  list-style: none;
+  display: flex;
+  align-items: baseline;
+  gap: 0.55rem;
+  font-family: var(--verity-font-display);
+  font-weight: 600;
+  color: var(--verity-heading);
+  font-size: 1.05rem;
+  letter-spacing: -0.005em;
+  position: relative;
+}
+
+article main details > summary::-webkit-details-marker {
+  display: none;
+}
+
+article main details > summary::before {
+  content: "▸";
+  color: var(--verity-accent);
+  font-size: 0.78em;
+  transition: transform 0.15s ease;
+  display: inline-block;
+  width: 1em;
+}
+
+article main details[open] > summary::before {
+  transform: rotate(90deg);
+}
+
+article main details > summary:focus-visible {
+  outline-offset: 4px;
+}
+
+article main details[open] > *:not(summary) {
+  margin-top: 0.7rem;
+}
+
 article main hr {
   border: 0;
   height: 0;

From 4965d0e7a1e5b4b823c1e59f09aa8bd01c042a1d Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 09:39:04 +0200
Subject: [PATCH 13/29] mobile(docs): tighter cell padding + smaller font in
 reference tables

Reference tables (getting-started prereqs, research iterations) keep
more horizontal space for content when each cell uses 0.55/0.6rem
padding and 0.92rem font instead of the desktop default 0.7/0.85rem
at 0.95rem. Combined with the earlier "no-hyphen in cells" change,
4-column tables now wrap each cell on natural word boundaries
inside a phone column without the previous "Solidity test-/ing"
hyphenation.
---
 docs-site/app/verity-site.css | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index 4e1424c85..bb9bbaa7a 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -1958,6 +1958,15 @@ input:focus-visible,
     white-space: nowrap !important;
   }
 
+  /* Tighter cell padding on phones so a 4-column reference table
+     keeps more horizontal space for actual content. */
+  article main th,
+  article main td {
+    padding: 0.55rem 0.6rem !important;
+    font-size: 0.92rem !important;
+    line-height: 1.45 !important;
+  }
+
   article main > :not(.verity-hero):not(.code-compare):not(.report-callout) {
     max-width: 100%;
   }

From dd09e688d26027ef9cc7e6d13fc9d2460dd82d56 Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 09:40:02 +0200
Subject: [PATCH 14/29] mobile(docs): tap-active feedback on
 CodeCompareSwitcher tabs
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Same idea as the hero CTAs — :hover is unreliable on touch. Tabs
now get an inverted teal-mix background while pressed so a phone
tap feels acknowledged instead of the active state appearing only
after the panel finishes its fade.
---
 docs-site/app/verity-site.css | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index bb9bbaa7a..9c1b43617 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -1578,6 +1578,10 @@ input:focus-visible,
   color: var(--verity-accent-ink);
 }
 
+.code-switcher__tabs button:active {
+  background: color-mix(in srgb, var(--verity-accent) 60%, var(--verity-surface));
+}
+
 .code-switcher__tabs button:focus-visible {
   outline: 2px solid var(--verity-accent);
   outline-offset: 2px;

From bbf8badac071b22d5a8c2f70ac81109d1ddf3851 Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 09:41:32 +0200
Subject: [PATCH 15/29] ui(docs): brand wordmark gets focus-visible + active
 states

The Verity navbar wordmark already had a teal :hover lift. Add the
mirror :focus-visible state for keyboard users and an :active dim
so a phone tap on the brand reads as pressed.
---
 docs-site/app/verity-site.css | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index 9c1b43617..2a91a5b28 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -210,10 +210,16 @@ header.nextra-navbar > div:first-child {
   font-feature-settings: "kern", "liga", "calt";
 }
 
-.verity-brand:hover {
+.verity-brand:hover,
+.verity-brand:focus-visible {
   color: var(--verity-accent);
 }
 
+.verity-brand:active {
+  color: var(--verity-accent-strong, var(--verity-accent));
+  opacity: 0.85;
+}
+
 .verity-brand img {
   width: 1.35rem;
   height: 1.35rem;

From 2d4bca83091e59215b36077095f121bbe24d6cfb Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 09:44:38 +0200
Subject: [PATCH 16/29] mobile(docs): compact Copy-page widget + kicker padding
 on small phones
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

On phones the Copy-page button drops to 0.78rem font + 0.35/0.55rem
padding so the widget itself is smaller. On the very narrowest
screens (≤360px, e.g. Galaxy Fold inner), the hero kicker drops
its clear-space from 8rem to 6rem so "LEAN 4 · FORMAL VERIFICATION
· EVM" doesn't have to stack into four lines.
---
 docs-site/app/verity-site.css | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index 2a91a5b28..8e08e93b8 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -1138,6 +1138,12 @@ input:focus-visible,
   .verity-hero .verity-kicker span {
     margin: 0 0.3em;
   }
+
+  /* On these very narrow screens the Copy-page widget can drop to
+     about 100px so the kicker doesn't stack into four lines. */
+  .verity-hero__head > .verity-kicker {
+    padding-right: 6rem;
+  }
 }
 
 .verity-hero {
@@ -2007,6 +2013,14 @@ input:focus-visible,
     margin: 0 !important;
   }
 
+  /* On the very narrowest viewports (fold-style phones, ~280-360px)
+     shrink the Copy-page widget so the kicker has enough horizontal
+     space to fit on two lines instead of four. */
+  article > [class*="x:rounded-md"]:has(> button) button {
+    font-size: 0.78rem !important;
+    padding: 0.35rem 0.55rem !important;
+  }
+
   /* The kicker is the only line that sits at the same Y as the widget
      and needs to keep clear of it. Pad its right side so its last item
      doesn't slide under the widget. */

From 8e545cd47c9ca84864532c8f5d6f0e902242c71b Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 10:09:01 +0200
Subject: [PATCH 17/29] ui(docs): dark-mode selection + <mark> styling

- ::selection picks up a slightly stronger teal mix and explicit
  color so highlighted text stays legible. Dark mode gets its own
  rule that mixes accent into the page bg instead of transparent so
  the highlight reads as a band rather than a barely-visible halo.
- Adds a forward-compatible <mark> style: a soft teal wash with the
  heading ink color. Currently unused in content but ready for
  authors to highlight a key term inline without breaking the cold
  palette.
---
 docs-site/app/verity-site.css | 21 ++++++++++++++++++++-
 1 file changed, 20 insertions(+), 1 deletion(-)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index 8e08e93b8..a69a520ae 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -170,7 +170,26 @@ body {
 }
 
 ::selection {
-  background: color-mix(in srgb, var(--verity-accent) 28%, transparent);
+  background: color-mix(in srgb, var(--verity-accent) 30%, transparent);
+  color: var(--verity-heading);
+}
+
+.dark ::selection {
+  /* On a deep slate background the 30% mix reads almost black; use a
+     stronger teal-on-ink combo so highlighted text remains legible. */
+  background: color-mix(in srgb, var(--verity-accent) 38%, var(--verity-bg));
+  color: var(--verity-heading);
+}
+
+/* <mark> — semantically-highlighted text inside the article body.
+   Currently unused but content authors might wrap a key term in a
+   <mark> and expect a subtle yellow-highlighter. Use our palette so
+   it reads as "emphasised" without breaking the cold theme. */
+article main mark,
+mark {
+  background: color-mix(in srgb, var(--verity-accent) 22%, transparent);
+  color: var(--verity-heading);
+  padding: 0 0.18em;
 }
 
 /* Navbar — warm middle-tone between page cream and sidebar tan so it

From da812c7329bb81006554283c865c4ea0e5fdf35a Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 10:23:19 +0200
Subject: [PATCH 18/29] dark(docs): retune Verity code panel for sustained-read
 comfort
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The dark-mode Verity panel "arrache un peu les yeux" — too many
tokens landed in the same bright phosphor-teal at once. This batch
introduces a real visual hierarchy:

  * Top-level declarations (verity_contract, def, theorem, external,
    modifier, function) stay bold bright mint — the only "hot" tokens.
  * Section markers (storage, event_defs, where, linked_externals)
    drop to regular-weight, slightly softer mint (#7CD4C0) — readable
    but no longer competing for visual weight.
  * Types (Address, Uint256, ContractState, Bool, etc.) move from
    bright cyan-teal #A3E1D4 to desaturated sage-cyan #9FBEB6 with
    regular weight.
  * Function and identifier names drop to cool body-ink #C7D5D1,
    regular weight, so the page has actual resting zones.
  * Strings move to muted #86A8A2, numbers to soft mint #86C5B6 —
    distinguishable but not bold.
  * Errors / guards keep their coral accent but at a desaturated
    #E5A18C so they signal without screaming.
  * Code surface lifts from #0A1311 to #0F1B17 (a hair lighter)
    so the contrast gap between bg and tokens narrows.
  * The Verity-active panel's left-edge accent wash drops from
    accent×8% to accent×4% — the "lifted" cue is still visible
    without compounding the teal-on-teal saturation.

Light mode is untouched; the readability complaint was specifically
about the dark Verity panel.
---
 docs-site/app/verity-code.css     | 11 +++--
 docs-site/app/verity-site.css     |  9 ++--
 docs-site/themes/verity-dark.json | 78 +++++++++++++++----------------
 3 files changed, 50 insertions(+), 48 deletions(-)

diff --git a/docs-site/app/verity-code.css b/docs-site/app/verity-code.css
index 3b416d981..425863c91 100644
--- a/docs-site/app/verity-code.css
+++ b/docs-site/app/verity-code.css
@@ -19,20 +19,21 @@ figure[data-rehype-pretty-code-figure] pre[data-language="verity"] {
 }
 
 /* Dark-theme syntax remap: the bundled shiki theme is warm-amber. Push
-   highlights to cool teal/cyan/slate so code reads cold like the rest of
-   the dark theme. */
+   highlights to cool slate-teal so code reads cold like the rest of
+   the dark theme, but kept desaturated so the panel doesn't feel
+   over-saturated when many tokens land on screen. */
 .dark figure[data-rehype-pretty-code-figure] span[style*="#D9B7FF"],
 .dark figure[data-rehype-pretty-code-figure] span[style*="#D5B3FF"] {
-  color: #7DD3C0 !important;
+  color: #9FBEB6 !important;
 }
 
 .dark figure[data-rehype-pretty-code-figure] span[style*="#91C9FF"],
 .dark figure[data-rehype-pretty-code-figure] span[style*="#86D6C8"] {
-  color: #A3E1D4 !important;
+  color: #A8BCB6 !important;
 }
 
 .dark figure[data-rehype-pretty-code-figure] span[style*="#A3E1D4"] {
-  color: #82E0CC !important;
+  color: #9FBEB6 !important;
 }
 
 .dark figure[data-rehype-pretty-code-figure] span[style*="#D7E4F2"] {
diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index a69a520ae..d5d816575 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -86,7 +86,7 @@
   --verity-rule: #1E2A26;
   --verity-rule-soft: #16241F;
   --verity-code-bg: #0B1614;
-  --verity-code-surface: #0A1311;
+  --verity-code-surface: #0F1B17;
   --verity-accent: #2DD4BF;
   --verity-accent-strong: #5EEAD4;
   --verity-accent-bright: #2DD4BF;
@@ -1704,12 +1704,13 @@ input:focus-visible,
 }
 
 /* Subtle accent wash on the Verity panel so the lift to a proof-carrying
-   surface reads visually as well as semantically. Apply to the visible pre
-   so the solid code-surface !important above doesn't obscure it. */
+   surface reads visually as well as semantically. The earlier 8% mix
+   compounded with the bright keyword tokens to make the dark panel feel
+   saturated; 4% reads as a hint without intensifying the teal-on-teal. */
 .code-switcher[data-active="verity"] .code-panel--verity .code-panel__pre,
 .code-switcher[data-active="verity"] .code-panel--verity .code-panel__pre > pre {
   background:
-    linear-gradient(90deg, color-mix(in srgb, var(--verity-accent) 8%, transparent), transparent 15rem),
+    linear-gradient(90deg, color-mix(in srgb, var(--verity-accent) 4%, transparent), transparent 15rem),
     var(--verity-code-surface) !important;
 }
 
diff --git a/docs-site/themes/verity-dark.json b/docs-site/themes/verity-dark.json
index c277a24a2..4daf24b5c 100644
--- a/docs-site/themes/verity-dark.json
+++ b/docs-site/themes/verity-dark.json
@@ -3,8 +3,8 @@
   "name": "Verity Dark",
   "type": "dark",
   "colors": {
-    "editor.background": "#0A1311",
-    "editor.foreground": "#DDE8E5",
+    "editor.background": "#0F1B17",
+    "editor.foreground": "#D2DDD8",
     "editorLineNumber.foreground": "#6B7B77",
     "editor.selectionBackground": "#1B3631",
     "editor.inactiveSelectionBackground": "#152825"
@@ -20,76 +20,74 @@
     {
       "scope": ["string", "string.quoted.double", "string.quoted.double.verity"],
       "settings": {
-        "foreground": "#A3E1D4"
+        "foreground": "#86A8A2"
       }
     },
     {
       "scope": ["constant.numeric", "constant.numeric.hex", "constant.numeric.decimal", "constant.numeric.storage-slot", "constant.language.boolean", "constant.language.boolean.verity"],
       "settings": {
-        "foreground": "#7DD3C0",
-        "fontStyle": "bold"
+        "foreground": "#86C5B6"
       }
     },
     {
-      "scope": ["keyword", "keyword.declaration.contract.verity", "keyword.declaration.function.verity", "keyword.declaration.modifier.verity", "keyword.declaration.external.verity", "keyword.other.section.verity", "keyword.other.section.linked-externals.verity", "keyword.declaration.lean.verity", "source.lean keyword"],
+      "scope": ["keyword.declaration.contract.verity", "keyword.declaration.function.verity", "keyword.declaration.modifier.verity", "keyword.declaration.external.verity", "keyword.declaration.lean.verity"],
       "settings": {
         "foreground": "#5EEAD4",
         "fontStyle": "bold"
       }
     },
+    {
+      "scope": ["keyword", "keyword.other.section.verity", "keyword.other.section.linked-externals.verity", "source.lean keyword"],
+      "settings": {
+        "foreground": "#7CD4C0"
+      }
+    },
     {
       "scope": ["keyword.control.modifier-clause.verity", "storage.modifier.verity", "storage.modifier.reentrancy.verity", "keyword.control.do.verity", "keyword.control.lean.verity", "keyword.operator.assignment.verity", "keyword.operator", "punctuation.definition.parameters", "punctuation.separator", "punctuation.accessor.verity"],
       "settings": {
-        "foreground": "#9BB0AC"
+        "foreground": "#8E9E99"
       }
     },
     {
       "scope": ["entity.name.type.contract.verity", "storage.type.verity", "support.type", "entity.name.type", "storage.type"],
       "settings": {
-        "foreground": "#A3E1D4",
-        "fontStyle": "bold"
+        "foreground": "#9FBEB6"
       }
     },
     {
       "scope": ["entity.name.function.verity", "source.lean entity.name.function", "support.function.tactic.verity", "support.function.storage.verity", "support.function.context.verity", "support.function.arithmetic.verity", "support.function.spec.verity"],
       "settings": {
-        "foreground": "#C2D5D0",
-        "fontStyle": "bold"
+        "foreground": "#C7D5D1"
       }
     },
     {
       "scope": ["entity.name.function.external.verity", "support.function.external-call.verity"],
       "settings": {
-        "foreground": "#7DD3C0",
-        "fontStyle": "bold"
+        "foreground": "#9FBEB6"
       }
     },
     {
       "scope": ["entity.name.function.event.verity", "support.function.event.verity"],
       "settings": {
-        "foreground": "#82E0CC",
-        "fontStyle": "bold"
+        "foreground": "#9FBEB6"
       }
     },
     {
       "scope": ["entity.name.function.modifier.verity", "variable.other.property.verity"],
       "settings": {
-        "foreground": "#A3E1D4",
-        "fontStyle": "bold"
+        "foreground": "#A8BCB6"
       }
     },
     {
       "scope": ["support.function.guard.verity", "entity.name.exception.custom-error.verity"],
       "settings": {
-        "foreground": "#F0A48F",
-        "fontStyle": "bold"
+        "foreground": "#E5A18C"
       }
     },
     {
       "scope": ["support.function.loop.verity", "support.function.abi.verity"],
       "settings": {
-        "foreground": "#9BB0AC",
-        "fontStyle": "bold"
+        "foreground": "#9BB0AC"
       }
     },
     {
@@ -118,7 +116,15 @@
         "storage.type.enum",
         "storage.type.error",
         "storage.type.mapping",
-        "storage.type.constructor",
+        "storage.type.constructor"
+      ],
+      "settings": {
+        "foreground": "#5EEAD4",
+        "fontStyle": "bold"
+      }
+    },
+    {
+      "scope": [
         "keyword.control",
         "keyword.control.flow",
         "keyword.control.import",
@@ -127,8 +133,7 @@
         "keyword.control.for"
       ],
       "settings": {
-        "foreground": "#5EEAD4",
-        "fontStyle": "bold"
+        "foreground": "#7CD4C0"
       }
     },
     {
@@ -140,8 +145,7 @@
         "storage.modifier.is"
       ],
       "settings": {
-        "foreground": "#A3E1D4",
-        "fontStyle": "bold"
+        "foreground": "#9FBEB6"
       }
     },
     {
@@ -149,8 +153,7 @@
         "support.type.primitive"
       ],
       "settings": {
-        "foreground": "#A3E1D4",
-        "fontStyle": "bold"
+        "foreground": "#9FBEB6"
       }
     },
     {
@@ -166,8 +169,7 @@
         "entity.name.type.userType"
       ],
       "settings": {
-        "foreground": "#7DD3C0",
-        "fontStyle": "bold"
+        "foreground": "#9FBEB6"
       }
     },
     {
@@ -176,7 +178,7 @@
         "entity.name.function.modifier"
       ],
       "settings": {
-        "foreground": "#86D6C8"
+        "foreground": "#C7D5D1"
       }
     },
     {
@@ -187,8 +189,7 @@
         "keyword.control.contract"
       ],
       "settings": {
-        "foreground": "#F0A48F",
-        "fontStyle": "bold"
+        "foreground": "#E5A18C"
       }
     },
     {
@@ -206,7 +207,7 @@
         "support.variable.property"
       ],
       "settings": {
-        "foreground": "#82E0CC"
+        "foreground": "#9FBEB6"
       }
     },
     {
@@ -218,8 +219,7 @@
         "variable.language.type"
       ],
       "settings": {
-        "foreground": "#A3E1D4",
-        "fontStyle": "bold"
+        "foreground": "#9FBEB6"
       }
     },
     {
@@ -232,7 +232,7 @@
         "constant.language.time"
       ],
       "settings": {
-        "foreground": "#82E0CC"
+        "foreground": "#86C5B6"
       }
     },
     {
@@ -241,7 +241,7 @@
         "string.quoted.single"
       ],
       "settings": {
-        "foreground": "#A3E1D4"
+        "foreground": "#86A8A2"
       }
     },
     {
@@ -253,7 +253,7 @@
         "keyword.operator.binary"
       ],
       "settings": {
-        "foreground": "#9BB0AC"
+        "foreground": "#8E9E99"
       }
     }
   ],

From b870e14fd698653593637daaa89515f68d3cde81 Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 10:28:53 +0200
Subject: [PATCH 19/29] ui(docs): inline-code chips lift on link hover/focus

When a chip sits inside a link, hovering the link now lifts the chip
to a teal-tinted background with a teal border + teal text so the
chip reads as part of the interactive element instead of decoration
floating next to it.
---
 docs-site/app/verity-site.css | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index d5d816575..7e98c4ba3 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -1076,6 +1076,18 @@ code.nextra-code:not(pre code) {
   color: var(--verity-heading) !important;
 }
 
+/* When an inline chip sits inside a link, hovering the link shows a
+   gentle teal-tinted chip background so the chip reads as "part of
+   the interactive element" instead of decoration that floats next
+   to it. */
+article main a:hover :not(pre) > code,
+article main a:focus-visible :not(pre) > code {
+  background: color-mix(in srgb, var(--verity-accent) 14%, var(--verity-surface)) !important;
+  border-color: color-mix(in srgb, var(--verity-accent) 35%, var(--verity-rule)) !important;
+  color: var(--verity-accent) !important;
+  transition: background-color 0.15s ease, color 0.15s ease, border-color 0.15s ease;
+}
+
 /* When an inline code chip sits in a heading or strong, drop the chip
    chrome so the heading keeps its serif rhythm. */
 article h1 :not(pre) > code,

From 9a11c3063a03c30953c44f5874b867994c136146 Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 10:29:39 +0200
Subject: [PATCH 20/29] docs(site): style sup/sub/abbr for paper-style
 typography
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Currently unused but content authors should be able to drop in:
  * <sup> for a superscripted footnote marker
  * <sub> for an index / subscript
  * <abbr title="..."> for an initialism with a tooltip expansion

…and get LaTeX-style typography for free. Tabular numerals on the
super/subscript so digit-only markers ("1", "2", "10") align cleanly,
and a quiet dotted underline on <abbr> so glossed terms read as such
without breaking the cold palette.
---
 docs-site/app/verity-site.css | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index 7e98c4ba3..37fcf4884 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -192,6 +192,36 @@ mark {
   padding: 0 0.18em;
 }
 
+/* Footnote / index typography. Currently unused in content but ready
+   for authors to drop in superscripted footnote markers or subscript
+   indices the way a LaTeX paper does. */
+article main sup,
+article main sub {
+  font-size: 0.72em;
+  line-height: 0;
+  vertical-align: baseline;
+  position: relative;
+  font-feature-settings: "tnum", "lnum";
+}
+
+article main sup {
+  top: -0.45em;
+}
+
+article main sub {
+  top: 0.25em;
+}
+
+/* <abbr> with a title gets a quiet dotted underline so initialisms
+   ("ABI", "EVM", "EDSL") that have author-supplied expansions read
+   as glossed terms. */
+article main abbr[title] {
+  text-decoration: underline dotted color-mix(in srgb, var(--verity-muted) 70%, transparent);
+  text-underline-offset: 0.22em;
+  text-decoration-thickness: 1px;
+  cursor: help;
+}
+
 /* Navbar — warm middle-tone between page cream and sidebar tan so it
    doesn't read as a stark white slab above the sidebar.
 

From e36dfd8084b455a1c49643e9d3a1e0bcce4771ea Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 10:31:42 +0200
Subject: [PATCH 21/29] docs(site): lift dingbat hr visibility in dark mode
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The asterism rule (· · ·) was rendering in --verity-rule (#1E2A26)
which is functionally invisible on the #07100E dark page. Push to
--verity-muted at 60% opacity so the section break is legible without
asserting itself.

Also: revert the in-flight skip-to-content link attempt — it pointed
at #main-content but Nextra doesn't expose an article id we can hook
to, and adding the wrapper would require modifying the theme. Will
revisit if/when a proper anchor surfaces.
---
 docs-site/app/verity-site.css | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index 37fcf4884..b29517b21 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -135,6 +135,7 @@ body {
   -webkit-tap-highlight-color: color-mix(in srgb, var(--verity-accent) 18%, transparent);
 }
 
+
 [class*="x:text-blue"],
 [class*="x:text-primary"] {
   color: var(--verity-accent) !important;
@@ -955,7 +956,11 @@ article main hr::before {
 }
 
 .dark article main hr::before {
-  color: var(--verity-rule);
+  /* The rule color (#1E2A26) is too dark for three small dots on a
+     deep-slate page; use the muted body color so the asterism is
+     legible as a section break without competing with the prose. */
+  color: var(--verity-muted);
+  opacity: 0.6;
 }
 
 /* Unordered-list bullet styling — replace the default round bullet

From d1a645907bd905275a3c84629ef1de0f2c93a804 Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 10:34:39 +0200
Subject: [PATCH 22/29] typography(docs): raise code-block line-height for
 sustained read
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Bumped from 1.62-1.65 to 1.72 — matches the body-text rhythm and
gives the eye more breathing room on long Lean / Verity blocks
where line density was contributing to the "arrache les yeux" feel
alongside the previous saturation.
---
 docs-site/app/verity-code.css | 2 +-
 docs-site/app/verity-site.css | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/docs-site/app/verity-code.css b/docs-site/app/verity-code.css
index 425863c91..307cc6d6c 100644
--- a/docs-site/app/verity-code.css
+++ b/docs-site/app/verity-code.css
@@ -41,7 +41,7 @@ figure[data-rehype-pretty-code-figure] pre[data-language="verity"] {
 }
 
 figure[data-rehype-pretty-code-figure] pre[data-language="verity"] code {
-  line-height: 1.62;
+  line-height: 1.72;
 }
 
 figure[data-rehype-pretty-code-figure] pre[data-language="verity"] code > span {
diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index b29517b21..dabe0a967 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -1712,7 +1712,7 @@ input:focus-visible,
   color: var(--verity-ink) !important;
   font-family: var(--verity-font-code);
   font-size: 0.85rem;
-  line-height: 1.65;
+  line-height: 1.72;
   tab-size: 2;
   white-space: pre;
   border: 0 !important;

From 5e90b6a0558bd7043a1f4e8338f6a3d44edeb750 Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 10:38:12 +0200
Subject: [PATCH 23/29] dark(docs): soften hero italic emphasis to match code
 section markers

"Prove them correct" was inheriting --verity-accent-strong (#5EEAD4),
the same bright phosphor used for code keywords. Two hot spots on the
hero (the Verity-dot logotype and the italic dek emphasis) ran the
same retina-bright color back-to-back. Drop the dek em to #7CD4C0
(the softened section-marker mint from the code retune) so the hero
feels inviting rather than electric while still emphasizing the value
prop.
---
 docs-site/app/verity-site.css | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index dabe0a967..541e41d6f 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -1304,6 +1304,15 @@ input:focus-visible,
   font-feature-settings: "kern", "liga", "calt", "ss01";
 }
 
+/* In dark mode the accent-strong is the same bright mint we use for
+   code keywords. The italic phrase reads as the same "hot" token in
+   the hero, which is fine — it's a single short phrase, not a wall
+   of code — but soften the saturation a touch so the hero feels
+   inviting rather than electric. */
+.dark .verity-hero__dek em {
+  color: #7CD4C0;
+}
+
 .verity-hero__links {
   display: flex;
   flex-direction: column;

From fa4cd8d13d1c2e8accd9630677a0c4f8259293df Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 10:46:35 +0200
Subject: [PATCH 24/29] dark(docs): soften code-switcher kicker +
 report-callout top rule
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Continuing the readability-comfort pass:

  * "VERITY" / "SOLIDITY" caption kicker in the CodeCompareSwitcher
    header drops to the softer section-marker mint (#7CD4C0) in dark
    mode. Previously rendered in the bright brand accent above an
    already-busy code panel, which read as a stop sign rather than
    a label.
  * Report-callout top rule ("Where the trust comes from") softens
    from 2px bright phosphor to 2px section-mint in dark, so the
    callout reads as a raised paper rather than a highlighter strip.

Light mode keeps the brighter accent — these only affect dark.
---
 docs-site/app/verity-site.css | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index 541e41d6f..800db0d07 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -1619,6 +1619,13 @@ input:focus-visible,
   text-transform: uppercase;
 }
 
+/* In dark the bright phosphor accent felt loud above an already-busy
+   code panel; drop to the softer section-marker mint so the kicker
+   reads as a label rather than a stop sign. */
+.dark .code-switcher__caption span {
+  color: #7CD4C0;
+}
+
 .code-switcher__caption strong {
   color: var(--verity-heading);
   font-size: 0.92rem;
@@ -1895,6 +1902,13 @@ input:focus-visible,
   background: color-mix(in srgb, var(--verity-surface) 70%, transparent);
 }
 
+/* The 2px bright phosphor top rule felt like a highlighter strip in
+   dark mode. Soften to the section-marker mint so the callout reads
+   as "raised paper" not "alarm bar". */
+.dark .report-callout {
+  border-top-color: #7CD4C0;
+}
+
 .report-callout strong {
   display: block;
   color: var(--verity-heading);

From c61bd51660a7fbb0a507fc504939ee9b499618b1 Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 10:48:22 +0200
Subject: [PATCH 25/29] dark(docs): soften callout left bar to match rest of
 dark palette

The 0.22rem accent left bar on <blockquote>/<Callout> was the last
bright phosphor element still showing on dark pages alongside CTAs
and brand marks. Drop to the softer section-marker mint (#7CD4C0)
so a tip-callout in the middle of an article doesn't compete with
the actual call-to-action buttons.
---
 docs-site/app/verity-site.css | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index 800db0d07..377ba5581 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -1146,6 +1146,13 @@ article main blockquote,
   box-shadow: none !important;
 }
 
+/* Dark mode: drop the left bar to the softer section-marker mint so
+   the callout aligns with the rest of the eased dark palette. */
+.dark article main blockquote,
+.dark .nextra-callout {
+  border-left-color: #7CD4C0 !important;
+}
+
 button,
 .nextra-button,
 a[role="button"] {

From 994de3ee6a38d38c36dcd517d6741ffc496df04c Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 10:52:51 +0200
Subject: [PATCH 26/29] ui(docs): style visited links inside the article body

Browsers default :visited to purple, which looked out of place
amid the teal palette on dense reference pages (EDSL API, research
log). Mix the accent with the muted color (75/25) so visited links
stay in our palette but read as visibly visited on long pages.
---
 docs-site/app/verity-site.css | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index 377ba5581..18108111e 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -753,6 +753,14 @@ article main a {
   -webkit-tap-highlight-color: color-mix(in srgb, var(--verity-accent) 15%, transparent);
 }
 
+/* Override the browser default :visited (often purple) — visited
+   links stay in our palette but pick up a touch of muted weight so
+   you can still tell them apart on long reference pages. */
+article a:visited,
+article main a:visited {
+  color: color-mix(in srgb, var(--verity-accent) 75%, var(--verity-muted)) !important;
+}
+
 article a:hover,
 article main a:hover,
 .nextra-breadcrumb a:hover,

From 3ff0b9bb4e546664281c671874d3cb6eedec017b Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 10:55:08 +0200
Subject: [PATCH 27/29] mobile(docs): tighter asterism hr vertical margin on
 phones

2.5rem above + below felt loose on a narrow phone column. Drop to
2rem on mobile so a section break still reads as a break without
pushing two long sections too far apart.
---
 docs-site/app/verity-site.css | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index 18108111e..96e4116c4 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -2286,6 +2286,12 @@ input:focus-visible,
     -webkit-hyphens: manual !important;
   }
 
+  /* Asterism hr — tighter vertical margin on phones so the section
+     break doesn't push two long sections too far apart. */
+  article main hr {
+    margin: 2rem auto !important;
+  }
+
   /* The serif body uses hyphenation; on narrow screens this can
      hyphenate every other line. Loosen so words break only on the rare
      overflow case. */

From 1ad78a4e0db85dd4236cb1a95fa3f15f62c092f2 Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 10:57:02 +0200
Subject: [PATCH 28/29] ui(docs): refine visited-link underline + accent mix

Tweak the :visited mix from 75/25 to 78/22 (touch more accent
remaining so visited links don't read as fully muted) and dim
their underline to 30% accent so the visual weight of a visited
link sits between fresh-link and plain body text.
---
 docs-site/app/verity-site.css | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index 96e4116c4..9e785b6d6 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -758,7 +758,8 @@ article main a {
    you can still tell them apart on long reference pages. */
 article a:visited,
 article main a:visited {
-  color: color-mix(in srgb, var(--verity-accent) 75%, var(--verity-muted)) !important;
+  color: color-mix(in srgb, var(--verity-accent) 78%, var(--verity-muted)) !important;
+  text-decoration-color: color-mix(in srgb, var(--verity-accent) 30%, transparent) !important;
 }
 
 article a:hover,

From 3aadf5109d4a657723d11fce8c1193e829b8dd97 Mon Sep 17 00:00:00 2001
From: Claude Bot <bot@anthropic.com>
Date: Tue, 19 May 2026 11:42:52 +0200
Subject: [PATCH 29/29] fix(docs): address Bugbot review on PR #1908
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Six concrete issues plus one no-op already-fixed item:

  1. .code-switcher__tabs button:active was overriding the
     [data-active="true"] background when the user pressed the
     already-active tab, causing a brief contrast dip
     (full --verity-accent → 60% mix with surface, but text stays
     light). Scope :active to non-active tabs:
       button:not([data-active="true"]):active { ... }
  2. (no-op) .dark hr::before redundant rule — an earlier commit had
     already replaced the redundant --verity-rule color with
     --verity-muted + 0.6 opacity for proper visibility.
  3. Hero kicker padding-right was 6rem under @media (max-width:360px)
     but 8rem under @media (max-width:767px), and the later media
     query won by source order. Add !important to the 360px override
     so fold-style phones actually get the tighter clear-space.
  4. Mobile inline-code chips were truncating long paths with a
     text-overflow: ellipsis that had no tap affordance, hiding the
     rest of the path permanently. Switch to overflow-x:auto so the
     chip becomes a swipeable horizontal-scroll surface; the
     scrollbar itself is hidden (scrollbar-width:none) so the chip
     stays visually clean. Heading chips (h3) keep overflow:visible.
  5. The unordered-list ::before en-dash collided with GFM
     task-list checkboxes ("- [x] Done"), producing a "– ☐ Done"
     double-bullet. Suppress ::before on li.task-list-item /
     li:has(> input[type="checkbox"]) and zero out the bullet-clear
     padding so the checkbox sits where the en-dash was. Checkbox
     accent-color picks up --verity-accent.
  6. Chip-in-link transition was declared only on the :hover state,
     causing a snap-back on hover-out. Move transition to the base
     state (article main a > code, article main a > :not(pre) > code)
     so the fade is symmetric. Also corrected the descendant
     selector since Nextra renders <a><code> directly without any
     intermediate element — the previous `a :not(pre) > code` rule
     never actually matched the rendered DOM.
  7. Standalone figure[data-rehype-pretty-code-figure] pre was
     using --verity-code-bg (#0B1614) in dark while the mobile
     right-edge fade ended at --verity-code-surface (#0F1B17),
     creating a seam where the fade met the panel bg. Unify by
     using --verity-code-surface for the dark figure pre as well.
---
 docs-site/app/verity-code.css |  5 ++-
 docs-site/app/verity-site.css | 82 ++++++++++++++++++++++++++++++-----
 2 files changed, 74 insertions(+), 13 deletions(-)

diff --git a/docs-site/app/verity-code.css b/docs-site/app/verity-code.css
index 307cc6d6c..8a2b2ae28 100644
--- a/docs-site/app/verity-code.css
+++ b/docs-site/app/verity-code.css
@@ -9,7 +9,10 @@ figure[data-rehype-pretty-code-figure] pre[data-language="verity"] {
 }
 
 .dark figure[data-rehype-pretty-code-figure] pre {
-  background: var(--verity-code-bg) !important;
+  /* Match the standalone-figure surface to the same --verity-code-surface
+     the rest of the site uses (and that the mobile right-edge fade ends
+     at), so there's no seam where the gradient meets the panel bg. */
+  background: var(--verity-code-surface) !important;
   border: 1px solid var(--verity-rule) !important;
   color: var(--verity-ink) !important;
 }
diff --git a/docs-site/app/verity-site.css b/docs-site/app/verity-site.css
index 9e785b6d6..8fcf08e60 100644
--- a/docs-site/app/verity-site.css
+++ b/docs-site/app/verity-site.css
@@ -1004,6 +1004,35 @@ article main ol ul > li::before {
   line-height: 1;
 }
 
+/* GFM task-list items ("- [x] Done") render as <li class="task-list-item">
+   with an <input type="checkbox"> child. Our en-dash ::before marker
+   would collide with the checkbox, producing a "– ☐ Done" visual
+   double-bullet. Suppress the marker on task-list rows and let the
+   checkbox itself be the marker; also remove the bullet-clearing
+   left padding so the checkbox sits at the same x as the en-dash
+   markers on regular bullets. */
+article main ul > li.task-list-item::before,
+article main ul > li:has(> input[type="checkbox"])::before {
+  content: none;
+}
+
+article main ul:has(> li.task-list-item),
+article main ul:has(> li > input[type="checkbox"]) {
+  padding-left: 0;
+  list-style: none;
+}
+
+article main ul > li.task-list-item,
+article main ul > li:has(> input[type="checkbox"]) {
+  padding-left: 0;
+}
+
+article main ul > li > input[type="checkbox"] {
+  accent-color: var(--verity-accent);
+  margin-right: 0.45em;
+  vertical-align: -0.08em;
+}
+
 article main table {
   display: table;
   width: 100%;
@@ -1123,13 +1152,24 @@ code.nextra-code:not(pre code) {
 /* When an inline chip sits inside a link, hovering the link shows a
    gentle teal-tinted chip background so the chip reads as "part of
    the interactive element" instead of decoration that floats next
-   to it. */
-article main a:hover :not(pre) > code,
-article main a:focus-visible :not(pre) > code {
+   to it. The transition is declared on the chip-in-link base state
+   (not just the :hover override) so the fade is symmetric — hover-in
+   and hover-out both animate.
+
+   Nextra renders chip-in-link as <a><code>...</code></a> directly,
+   so the selector targets <code> as a direct child of <a>. */
+article main a > code,
+article main a > :not(pre) > code {
+  transition: background-color 0.15s ease, color 0.15s ease, border-color 0.15s ease;
+}
+
+article main a:hover > code,
+article main a:focus-visible > code,
+article main a:hover > :not(pre) > code,
+article main a:focus-visible > :not(pre) > code {
   background: color-mix(in srgb, var(--verity-accent) 14%, var(--verity-surface)) !important;
   border-color: color-mix(in srgb, var(--verity-accent) 35%, var(--verity-rule)) !important;
   color: var(--verity-accent) !important;
-  transition: background-color 0.15s ease, color 0.15s ease, border-color 0.15s ease;
 }
 
 /* When an inline code chip sits in a heading or strong, drop the chip
@@ -1222,9 +1262,13 @@ input:focus-visible,
   }
 
   /* On these very narrow screens the Copy-page widget can drop to
-     about 100px so the kicker doesn't stack into four lines. */
+     about 100px so the kicker doesn't stack into four lines. The
+     !important is necessary because the broader (max-width: 767px)
+     media query later in the file targets the same selector with
+     equal specificity, and the later-source rule would otherwise
+     win at ≤360px. */
   .verity-hero__head > .verity-kicker {
-    padding-right: 6rem;
+    padding-right: 6rem !important;
   }
 }
 
@@ -1688,7 +1732,11 @@ input:focus-visible,
   color: var(--verity-accent-ink);
 }
 
-.code-switcher__tabs button:active {
+/* Only apply the :active press background to tabs that are NOT the
+   currently-selected tab — otherwise it overrides the full-accent
+   active-tab background with a 60% mix, causing a visible contrast
+   dip when the user taps the already-active tab. */
+.code-switcher__tabs button:not([data-active="true"]):active {
   background: color-mix(in srgb, var(--verity-accent) 60%, var(--verity-surface));
 }
 
@@ -2053,19 +2101,29 @@ input:focus-visible,
     /* Treat the chip as an atomic inline-block: it either fits on the
        current line or wraps as a whole to a new line. This kills the
        "one orphan letter" wrap that was happening when a path got
-       broken mid-word as a last resort. */
+       broken mid-word as a last resort. When the chip is still too
+       long for one line (rare — only on very long paths), the chip
+       becomes horizontally scrollable so the user can swipe to read
+       the rest, instead of clipping content with an ellipsis that
+       has no tap affordance. */
     display: inline-block;
     max-width: 100%;
     white-space: nowrap;
-    overflow: hidden;
-    text-overflow: ellipsis;
+    overflow-x: auto;
+    overflow-y: hidden;
     vertical-align: baseline;
+    /* Hide the inline-scrollbar — the swipe affordance is enough. */
+    scrollbar-width: none;
+  }
+
+  article :not(pre) > code::-webkit-scrollbar,
+  code.nextra-code:not(pre code)::-webkit-scrollbar {
+    display: none;
   }
 
   /* For chip-style h3 headings (e.g. `getStorage` / `setStorage`) we
-     still want the chip to wrap as a whole rather than be ellipsised. */
+     still want the chip to be fully visible rather than scrollable. */
   article main h3 :not(pre) > code {
-    text-overflow: clip !important;
     overflow: visible !important;
   }