diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml
index d027d3422d..c9edcfac05 100644
--- a/.pre-commit-config.yaml
+++ b/.pre-commit-config.yaml
@@ -61,6 +61,18 @@ repos:
         files: '^(docs/basedpython/.*\.md|zensical\.toml|scripts/check_docs_nav\.py)$'
         pass_filenames: false
         priority: 0
+
+      - id: check-by-lexer
+        name: check the basedpython pygments lexer
+        # `--no-project` avoids building ruff from source. the lexer goes in
+        # editable, because a plain `--with <path>` is served from uv's build
+        # cache and would check a stale copy of the very thing being edited
+        entry: uv run --no-project --python 3.13 --with pygments --with-editable
+          ./python/basedpython-pygments python scripts/check_by_lexer.py
+        language: system
+        files: '^(docs/basedpython/.*\.md|python/basedpython-pygments/.*|scripts/check_by_lexer\.py)$'
+        pass_filenames: false
+        priority: 0
   # Prettier
   - repo: https://github.com/rbubley/mirrors-prettier
     rev: 9337a74165b178ae2c766f60bee7252a0f06f3e8 # frozen: v3.9.5
diff --git a/README.md b/README.md
index 60dc233e31..1ca841708c 100644
--- a/README.md
+++ b/README.md
@@ -2,15 +2,25 @@
 
 a python type checker and a python-like language that transpiles to pure python
 
+- **a python type checker with framework support** — pydantic, sqlalchemy,
+    pytest and django are modelled directly, so the magic they do at runtime
+    checks like ordinary code
+- **basedpython, a python-like language that builds into python wheels**
+- **compiles into high performance python extension modules**
+- **a language server, formatter and linter** — `by server` drives the editor,
+    and `buff` is the basedpython build of ruff
+
 ```by
 enum class Shape:
     case Circle(radius: int)
     case Rect(width: int, height: int)
 
     def area(self) -> int:
-        match self:
-            case Shape.Circle(r): return 3 * r * r
-            case Shape.Rect(w, h): return w * h
+        return match self:
+            case Shape.Circle(r):
+                3 * r * r
+            case Shape.Rect(w, h):
+                w * h
 
 extension list[Element: Shape]:
     def first_circle(self) -> Shape.Circle?:
@@ -33,6 +43,7 @@ def main():
 
 ```sh
 uv add --dev basedpython
+echo 'print("hello")' > main.by
 by run main
 ```
 
@@ -42,7 +53,5 @@ by run main
 
 ## acknowledgements
 
-basedpython is a fork of [astral-sh/ruff](https://github.com/astral-sh/ruff) —
-it reuses ruff's parser, AST, and fix-application machinery, and the type
-checker is built on [ty](https://github.com/astral-sh/ty). none of this would
+basedpython is built on top of [astral-sh/ruff](https://github.com/astral-sh/ruff). none of this would
 exist without the work of the astral team and the wider ruff community
diff --git a/crates/by_transforms/src/reverse_transforms/identity_swap.rs b/crates/by_transforms/src/reverse_transforms/identity_swap.rs
index c3055726a9..d3616fec8c 100644
--- a/crates/by_transforms/src/reverse_transforms/identity_swap.rs
+++ b/crates/by_transforms/src/reverse_transforms/identity_swap.rs
@@ -1,19 +1,29 @@
 //! reverse of `crate::transforms::identity_swap`:
-//!   `x is y`            → `x === y`
-//!   `x is not y`        → `x === not y`  (not symmetric — see below)
-//!   `isinstance(x, y)`  → `x is y`
+//!   `x is y`                → `x === y`
+//!   `x is not y`            → `x !== y`
+//!   `isinstance(x, y)`      → `x is y`
+//!   `not isinstance(x, y)`  → `x is not y`
 //!
-//! basedpython's `is` is the instance check, so a Python `is` round-trips
-//! to `===` and an `isinstance` call round-trips to `is`. Note `is not`
-//! reverses incompletely — there's no concise basedpython spelling
+//! basedpython's `is` is the instance check, so a python identity comparison
+//! round-trips to `===` / `!==` and an `isinstance` call round-trips to `is`
+//!
+//! a literal right-hand side is left alone, mirroring the forward transform's
+//! own literal guard: `x is None` is identity in both languages, so rewriting
+//! it to `x === None` would churn idiomatic source for no change in meaning.
+//! this is why the operator must be rewritten rather than skipped — leaving a
+//! python `is not` in place re-reads it as `not isinstance(...)` on the way
+//! back out
 
 use ruff_diagnostics::{Edit, Fix};
 use ruff_python_ast::visitor::{Visitor, walk_expr, walk_stmt};
-use ruff_python_ast::{CmpOp, Expr, Stmt};
+use ruff_python_ast::{CmpOp, Expr, Stmt, UnaryOp};
 use ruff_text_size::{Ranged, TextRange, TextSize};
 
 pub(crate) struct IdentitySwapReverse<'src> {
     source: &'src str,
+    /// `isinstance` calls already folded into an enclosing `not`, so the call
+    /// itself must not also be rewritten into an overlapping edit
+    folded_into_not: Vec<TextRange>,
     pub(crate) edits: Vec<Fix>,
 }
 
@@ -21,6 +31,7 @@ impl<'src> IdentitySwapReverse<'src> {
     pub(crate) fn new(source: &'src str) -> Self {
         Self {
             source,
+            folded_into_not: Vec::new(),
             edits: Vec::new(),
         }
     }
@@ -34,36 +45,106 @@ impl<'src> IdentitySwapReverse<'src> {
         for (op, rhs) in c.ops.iter().zip(c.comparators.iter()) {
             let rhs_start = rhs.range().start();
             let between = &self.source[usize::from(lhs_end)..usize::from(rhs_start)];
-            if matches!(op, CmpOp::Is) && between.trim() == "is" {
-                if let Some(pos) = between.find("is") {
-                    let op_start = lhs_end + TextSize::try_from(pos).unwrap();
-                    let op_range = TextRange::new(op_start, op_start + TextSize::from(2u32));
-                    self.edits.push(Fix::safe_edit(Edit::range_replacement(
-                        "===".to_owned(),
-                        op_range,
-                    )));
+            // a literal rhs means identity in basedpython too, so the forward
+            // transform leaves it as `is` — mirror that and don't churn it
+            if !rhs.is_literal_expr() {
+                let words: &[&str] = match op {
+                    CmpOp::Is => &["is"],
+                    CmpOp::IsNot => &["is", "not"],
+                    _ => &[],
+                };
+                if let Some(tokens) = operator_tokens(between, lhs_end, words) {
+                    self.rewrite_operator(&tokens, between, lhs_end);
                 }
             }
             lhs_end = rhs.range().end();
         }
     }
 
-    fn process_call(&mut self, call: &ruff_python_ast::ExprCall) {
-        // detect `isinstance(x, y)` with exactly 2 positional args and no
-        // keyword args. anything else stays as-is to avoid losing semantics
-        if !matches!(call.func.as_ref(), Expr::Name(n) if n.id.as_str() == "isinstance") {
+    /// replace the located operator tokens with their basedpython spelling
+    ///
+    /// `is` is one token and becomes `===`. `is not` is two, and is normally
+    /// replaced as one span so `!==` lands where the operator was. when a
+    /// comment sits between the two words that span would swallow it, so the
+    /// words are rewritten separately instead — `not` goes with the spaces
+    /// after it, which leaves the comment and the line's indentation intact
+    fn rewrite_operator(&mut self, tokens: &[TextRange], gap: &str, gap_start: TextSize) {
+        let Some(first) = tokens.first() else {
+            return;
+        };
+        let (spelling, Some(last)) = (if tokens.len() == 1 { "===" } else { "!==" }, tokens.get(1))
+        else {
+            // `is` on its own — replace the one word in place
+            self.edits.push(Fix::safe_edit(Edit::range_replacement(
+                "===".to_owned(),
+                *first,
+            )));
+            return;
+        };
+
+        let between_words =
+            &gap[usize::from(first.end() - gap_start)..usize::from(last.start() - gap_start)];
+        if between_words.trim().is_empty() {
+            self.edits.push(Fix::safe_edit(Edit::range_replacement(
+                spelling.to_owned(),
+                TextRange::new(first.start(), last.end()),
+            )));
             return;
         }
-        if !call.arguments.keywords.is_empty() {
+
+        // a comment sits between the two words, so replace them separately.
+        // `not` goes along with the spaces after it, which keeps the line it
+        // sat on indented as it was
+        self.edits.push(Fix::safe_edit(Edit::range_replacement(
+            spelling.to_owned(),
+            *first,
+        )));
+        let trailing = gap[usize::from(last.end() - gap_start)..]
+            .bytes()
+            .take_while(|byte| matches!(byte, b' ' | b'\t'))
+            .count();
+        self.edits
+            .push(Fix::safe_edit(Edit::range_deletion(TextRange::new(
+                last.start(),
+                last.end() + TextSize::from(u32::try_from(trailing).unwrap_or(0)),
+            ))));
+    }
+
+    /// `not isinstance(x, y)` → `x is not y`, the exact inverse of the forward
+    /// transform. rewriting only the call would leave the correct but clumsier
+    /// `not x is y`
+    fn process_unary(&mut self, unary: &ruff_python_ast::ExprUnaryOp) {
+        if unary.op != UnaryOp::Not {
             return;
         }
-        if call.arguments.args.len() != 2 {
+        let Expr::Call(call) = unary.operand.as_ref() else {
+            return;
+        };
+        let Some((x, y)) = isinstance_operands(call) else {
+            return;
+        };
+        let (x_src, y_src) = (
+            self.src(x.range()).to_owned(),
+            self.src(y.range()).to_owned(),
+        );
+        self.folded_into_not.push(call.range());
+        self.edits.push(Fix::safe_edit(Edit::range_replacement(
+            format!("{x_src} is not {y_src}"),
+            unary.range(),
+        )));
+    }
+
+    fn process_call(&mut self, call: &ruff_python_ast::ExprCall) {
+        if self.folded_into_not.contains(&call.range()) {
             return;
         }
-        let x = &call.arguments.args[0];
-        let y = &call.arguments.args[1];
-        let x_src = self.src(x.range()).to_owned();
-        let y_src = self.src(y.range()).to_owned();
+        let Some((x, y)) = isinstance_operands(call) else {
+            return;
+        };
+        let (x_src, y_src) = (
+            self.src(x.range()).to_owned(),
+            self.src(y.range()).to_owned(),
+        );
         self.edits.push(Fix::safe_edit(Edit::range_replacement(
             format!("{x_src} is {y_src}"),
             call.range(),
@@ -71,10 +152,72 @@ impl<'src> IdentitySwapReverse<'src> {
     }
 }
 
+/// the two operands of an `isinstance(x, y)` call. anything else — a keyword
+/// argument, a different arity — stays as-is rather than lose semantics
+fn isinstance_operands(call: &ruff_python_ast::ExprCall) -> Option<(&Expr, &Expr)> {
+    if !matches!(call.func.as_ref(), Expr::Name(n) if n.id.as_str() == "isinstance") {
+        return None;
+    }
+    if !call.arguments.keywords.is_empty() {
+        return None;
+    }
+    let [x, y] = &*call.arguments.args else {
+        return None;
+    };
+    Some((x, y))
+}
+
+/// the range of each word of the operator written between two comparison
+/// operands, where `gap_start` is that gap's offset in the file
+///
+/// the gap holds only the operator, but it may also hold comments, line
+/// continuations and newlines — a comment is skipped rather than searched, so
+/// `a is  # this\n not b` finds the real `not` and not the one inside the
+/// comment. `None` if what is there is not exactly `words`, which leaves an
+/// operator this cannot account for untouched
+fn operator_tokens(gap: &str, gap_start: TextSize, words: &[&str]) -> Option<Vec<TextRange>> {
+    if words.is_empty() {
+        return None;
+    }
+    let mut tokens = Vec::with_capacity(words.len());
+    let mut cursor = 0usize;
+    while cursor < gap.len() {
+        let rest = &gap[cursor..];
+        let skip = match rest.as_bytes()[0] {
+            b'#' => rest.find('\n').map_or(rest.len(), |end| end + 1),
+            b'\\' => 1,
+            byte if byte.is_ascii_whitespace() => 1,
+            _ => 0,
+        };
+        if skip > 0 {
+            cursor += skip;
+            continue;
+        }
+        let end = rest
+            .find(|c: char| !c.is_alphanumeric() && c != '_')
+            .unwrap_or(rest.len());
+        if end == 0 {
+            return None;
+        }
+        if tokens.len() == words.len() || &rest[..end] != words[tokens.len()] {
+            return None;
+        }
+        let start = gap_start + TextSize::try_from(cursor).ok()?;
+        tokens.push(TextRange::new(
+            start,
+            gap_start + TextSize::try_from(cursor + end).ok()?,
+        ));
+        cursor += end;
+    }
+    (tokens.len() == words.len()).then_some(tokens)
+}
+
 impl<'ast> Visitor<'ast> for IdentitySwapReverse<'_> {
     fn visit_expr(&mut self, expr: &'ast Expr) {
         match expr {
             Expr::Compare(c) => self.process_compare(c),
+            // before the walk reaches the call inside it
+            Expr::UnaryOp(unary) => self.process_unary(unary),
             Expr::Call(call) => self.process_call(call),
             _ => {}
         }
@@ -88,7 +231,7 @@ impl<'ast> Visitor<'ast> for IdentitySwapReverse<'_> {
 
 #[cfg(test)]
 mod tests {
-    use crate::{Config, reverse_transpile};
+    use crate::{Config, reverse_transpile, transpile};
     use indoc::indoc;
 
     fn check(input: &str, expected: &str) {
@@ -98,6 +241,19 @@ mod tests {
         );
     }
 
+    /// python in, reversed to basedpython, transpiled forward again: the
+    /// comparison must come back meaning what it meant. this is what a bare
+    /// `is not` used to fail — it survived the reverse untouched and then read
+    /// as `not isinstance(...)` on the way out
+    fn check_round_trip(python: &str) {
+        let by = reverse_transpile(python, &Config::test_default()).unwrap();
+        let back = transpile(&by, &Config::test_default()).unwrap();
+        assert!(
+            back.ends_with(python),
+            "round trip diverged\n python: {python:?}\n     by: {by:?}\n   back: {back:?}"
+        );
+    }
+
     #[test]
     fn isinstance_to_is() {
         check(
@@ -120,14 +276,101 @@ mod tests {
                     pass
             "},
             indoc! {"
-                if not x is str:
+                if x is not str:
                     pass
             "},
         );
     }
 
+    #[test]
+    fn identity_to_triple_equals() {
+        check("y = a is b\n", "y = a === b\n");
+    }
+
+    #[test]
+    fn negated_identity_to_bang_equals() {
+        check("y = a is not b\n", "y = a !== b\n");
+    }
+
+    #[test]
+    fn negated_identity_over_multiple_lines() {
+        check(
+            indoc! {"
+                y = (
+                    a
+                    is
+                    not b
+                )
+            "},
+            indoc! {"
+                y = (
+                    a
+                    !== b
+                )
+            "},
+        );
+    }
+
+    /// a comment inside the operator must not be swallowed by the replacement,
+    /// and must not stop the rewrite either — leaving `is not` in place would
+    /// re-read it as `not isinstance(...)`
+    #[test]
+    fn negated_identity_around_a_comment() {
+        check(
+            indoc! {"
+                y = (a is  # this note mentions not
+                     not b)
+            "},
+            indoc! {"
+                y = (a !==  # this note mentions not
+                     b)
+            "},
+        );
+    }
+
+    /// a literal rhs is identity in both languages, so the forward transform
+    /// leaves it as `is` and the reverse must not churn it
+    #[test]
+    fn literal_comparisons_left_alone() {
+        check("y = a is None\n", "y = a is None\n");
+        check("y = a is not None\n", "y = a is not None\n");
+        check("y = a is True\n", "y = a is True\n");
+        check("y = a is not 1\n", "y = a is not 1\n");
+    }
+
+    /// the comment case cannot round-trip byte for byte — the operator's layout
+    /// normalises around the comment. what must survive is the *meaning*: it
+    /// has to come back as identity, not as the `not isinstance(...)` a
+    /// left-alone `is not` used to produce
+    #[test]
+    fn comment_case_round_trips_semantically() {
+        let python = "y = (a is  # note\n     not b)\n";
+        let by = reverse_transpile(python, &Config::test_default()).unwrap();
+        let back = transpile(&by, &Config::test_default()).unwrap();
+        assert!(back.contains("is not"), "{back:?}");
+        assert!(!back.contains("isinstance"), "{back:?}");
+    }
+
     #[test]
     fn unrelated_call_left_alone() {
         check("y = some(x, int)\n", "y = some(x, int)\n");
     }
+
+    #[test]
+    fn isinstance_with_keyword_left_alone() {
+        check(
+            "y = isinstance(x, class_or_tuple=int)\n",
+            "y = isinstance(x, class_or_tuple=int)\n",
+        );
+    }
+
+    #[test]
+    fn round_trips() {
+        check_round_trip("y = a is b\n");
+        check_round_trip("y = a is not b\n");
+        check_round_trip("y = a is None\n");
+        check_round_trip("y = a is not None\n");
+        check_round_trip("y = isinstance(a, int)\n");
+        check_round_trip("y = not isinstance(a, int)\n");
+    }
 }
diff --git a/crates/by_typeshed_patch/src/patches/container_overlapping.rs b/crates/by_typeshed_patch/src/patches/container_overlapping.rs
index 415e76cc92..1ba0d103de 100644
--- a/crates/by_typeshed_patch/src/patches/container_overlapping.rs
+++ b/crates/by_typeshed_patch/src/patches/container_overlapping.rs
@@ -3,8 +3,10 @@
 //! `Container` is covariant in its element (`out Element`), so a membership test
 //! consumes that covariant typevar in an input position. basedpython types the
 //! parameter as `Overlapping[Element]`: a value is accepted iff it is not
-//! disjoint from `Element`, so `1 in xs` and `object() in xs` are allowed for an
-//! `xs: Container[int]`, while `"a" in xs` is rejected
+//! disjoint from `Element`, so for an `xs: Container[int]` both `1 in xs` and
+//! `o in xs` (an `o: object`) are allowed, while `"a" in xs` is rejected. a bare
+//! `object()` is inferred `final object` — exactly `object`, so disjoint from
+//! `int` — and is rejected like any other disjoint operand
 //!
 //! `Container.__contains__` is the abstract membership requirement. every other
 //! container that already declares `__contains__` keeps its own declaration
diff --git a/crates/ty/src/cli-reference.md b/crates/ty/src/cli-reference.md
index 28923babcf..a73406f147 100644
--- a/crates/ty/src/cli-reference.md
+++ b/crates/ty/src/cli-reference.md
@@ -50,7 +50,7 @@ transpiled output to stdout:
 
 ```sh
 by transpile hello.by
-echo 'x[(a, b)]' | by transpile
+echo 'a = b ?? 1' | by transpile
 ```
 
 ### `--reverse`
diff --git a/crates/ty_python_semantic/src/api_lockfile.rs b/crates/ty_python_semantic/src/api_lockfile.rs
index 31b907b4e4..3e699573ab 100644
--- a/crates/ty_python_semantic/src/api_lockfile.rs
+++ b/crates/ty_python_semantic/src/api_lockfile.rs
@@ -5,8 +5,9 @@
 //! the lockfile is meant to be diffed, not parsed back into types. any
 //! type-level change in a public symbol surfaces as a line-level diff
 //!
-//! the first line is `#api-lock:v=1` (grammar version). subsequent lines are
-//! sorted lexicographically. one record per line:
+//! four `#`-prefixed header lines come first: `#api-lock:v=1` (grammar
+//! version), `#tool:by=<version>`, `#python:<target>` and `#modules:<count>`.
+//! the records follow, sorted lexicographically, one per line:
 //!
 //! ```text
 //! <qualified>:c[<bases>]                              # class
diff --git a/docs/basedpython/acknowledgements.md b/docs/basedpython/acknowledgements.md
deleted file mode 100644
index 434adcb7cc..0000000000
--- a/docs/basedpython/acknowledgements.md
+++ /dev/null
@@ -1,37 +0,0 @@
-# acknowledgements
-
-third-party work basedpython relies on but does not include
-
-the root [`LICENSE`](https://github.com/KotlinIsland/basedpython/blob/main/LICENSE)
-covers the libraries basedpython is *derived* from — code vendored into this
-repository. the entries below are different: nothing here is copied,
-redistributed, or linked. they are packages that transpiled basedpython output
-imports at runtime, and that the person running that output installs
-themselves. they are acknowledged here because relying on someone's work is
-worth saying out loud, even when no licence obliges it
-
-## regex
-
-|            |                                                        |
-| ---------- | ------------------------------------------------------ |
-| package    | [`regex`](https://pypi.org/project/regex/)             |
-| author     | Matthew Barnett                                        |
-| repository | [mrab-regex](https://github.com/mrabarnett/mrab-regex) |
-| licence    | `Apache-2.0 AND CNRI-Python`                           |
-
-the [grapheme string surface](features/character.md) — `count`, `first`,
-`last`, `characters`, `character_at`, `reversed`, `prefix`, `suffix` — is
-grapheme-correct, and grapheme correctness needs an engine that implements
-[UAX #29](https://unicode.org/reports/tr29/). `regex` is the only widely
-available python engine that does, via its `\X` escape, so the lowerings for
-those accessors emit `import regex` and it becomes a runtime dependency of any
-program that uses them. the standard library's `re` has no `\X`, and splitting
-on code points instead would silently miscount every multi-code-point grapheme
-— five for `"🤦🏼‍♂️"` rather than one
-
-the two licences apply to different parts of the package: `CNRI-Python` to the
-original `re` code derived from CPython (copyright 1998-2001 Secret Labs AB),
-`Apache-2.0` to Matthew Barnett's additions and alterations (copyright 2020).
-both are permissive, and basedpython neither vendors nor redistributes any of
-it — `import regex` in generated output is an ordinary dependency of the
-generated program, resolved from the user's own environment
diff --git a/docs/basedpython/credits.md b/docs/basedpython/credits.md
new file mode 100644
index 0000000000..df535d021b
--- /dev/null
+++ b/docs/basedpython/credits.md
@@ -0,0 +1,46 @@
+# credits
+
+- [kotlinisland](https://github.com/KotlinIsland) - author and maintainer
+- [Joren Hammudoglu](https://github.com/jorenham) - design work
+- [charliecloudberry](https://github.com/charliecloudberry) - technical writer
+- [detachhead](https://github.com/detachhead) - design work
+- Chloe Assouline - graphic design
+
+## upstream
+
+basedpython is a fork of [ruff](https://github.com/astral-sh/ruff), and its
+type checker is built on [ty](https://github.com/astral-sh/ty). the parser, the
+AST, the fix-application machinery and the whole checking core are the work of
+the [Astral](https://astral.sh) team and the wider ruff community — basedpython
+adds a language on top of tools that were already excellent
+
+every ruff and ty contributor is credited in
+[the upstream repository's history](https://github.com/astral-sh/ruff/graphs/contributors);
+their copyright is carried in the root
+[`LICENSE`](https://github.com/KotlinIsland/basedpython/blob/main/LICENSE)
+
+## third-party runtime dependencies
+
+these are packages that transpiled basedpython output
+imports at runtime, and that the person running that output installs
+themselves
+
+### regex
+
+|            |                                                        |
+| ---------- | ------------------------------------------------------ |
+| package    | [`regex`](https://pypi.org/project/regex/)             |
+| author     | Matthew Barnett                                        |
+| repository | [mrab-regex](https://github.com/mrabarnett/mrab-regex) |
+| licence    | `Apache-2.0 AND CNRI-Python`                           |
+
+used for [`Character` and grapheme support](features/character.md) — its `\X`
+escape implements [UAX #29](https://unicode.org/reports/tr29/), which the
+standard library's `re` has no equivalent for
+
+the two licences apply to different parts of the package: `CNRI-Python` to the
+original `re` code derived from CPython (copyright 1998-2001 Secret Labs AB),
+`Apache-2.0` to Matthew Barnett's additions and alterations (copyright 2020).
+both are permissive, and basedpython neither vendors nor redistributes any of
+it — `import regex` in generated output is an ordinary dependency of the
+generated program, resolved from the user's own environment
diff --git a/docs/basedpython/development/type-def-design.md b/docs/basedpython/development/type-def-design.md
index 68128ce4b7..639d35f308 100644
--- a/docs/basedpython/development/type-def-design.md
+++ b/docs/basedpython/development/type-def-design.md
@@ -1,8 +1,5 @@
 # `type def` — user-defined type functions
 
-status: design. a **proof of concept** of the shaded parts exists — see
-[what is implemented](#what-is-implemented) — but this document is the proposal,
-not a description of existing behaviour
 
 ## summary
 
@@ -660,7 +657,7 @@ would delete outright
 - third-party ones do not, until listed:
 
     ```toml
-    [tool.by.type-functions]
+    [tool.basedpython.type-functions]
     trust = ["some_package"]
     ```
 
@@ -679,7 +676,7 @@ functions in cheap-to-import modules is a documented recommendation, and
 ## configuration
 
 ```toml
-[tool.by.type-functions]
+[tool.basedpython.type-functions]
 enabled = true
 trust = []
 workers = 4
diff --git a/docs/basedpython/features/api-lock.md b/docs/basedpython/features/api-lock.md
index f9d5f70d25..ebf577782d 100644
--- a/docs/basedpython/features/api-lock.md
+++ b/docs/basedpython/features/api-lock.md
@@ -21,9 +21,11 @@ by generate-api-file -o public.lock
 
 ## record grammar
 
-each non-header line is one record. fields are colon-separated. the first
-line is the format-version header (`#api-lock:v=1`); the remaining lines
-are sorted lexicographically
+the file opens with four `#`-prefixed header lines: the format version
+(`#api-lock:v=1`), the generating `by` version (`#tool:by=0.0.5`), the target
+(`#python:3.13`, or `#python:default` when no `--python-version` was given) and
+the number of modules walked (`#modules:12`). every line after them is one
+record. fields are colon-separated, and the records are sorted lexicographically
 
 ```text
 <qualified>:c[<bases>]                       # class
diff --git a/docs/basedpython/features/character.md b/docs/basedpython/features/character.md
index 15dd37e422..7732ae270a 100644
--- a/docs/basedpython/features/character.md
+++ b/docs/basedpython/features/character.md
@@ -59,7 +59,7 @@ rather than silently miscounting — `len`-style code-point splitting would give
 `5` for the facepalm above, not `1`
 
 `regex` is Matthew Barnett's work, licensed `Apache-2.0 AND CNRI-Python` — see
-[acknowledgements](../acknowledgements.md)
+[credits](../credits.md#regex)
 
 the rewrites are type-directed: they fire only when the receiver is a string
 (`str`, `Character`, `LiteralString`, a literal, or a `str` subclass).
diff --git a/docs/basedpython/features/checked-cast.md b/docs/basedpython/features/checked-cast.md
index 05a8ae40d4..02ef8ce178 100644
--- a/docs/basedpython/features/checked-cast.md
+++ b/docs/basedpython/features/checked-cast.md
@@ -28,7 +28,7 @@ def _checked_cast(_v, _t):
         )
     return _v
 
-def f(a):
+def f(a: object):
     b = _checked_cast(a, int)
     print(b)
 ```
diff --git a/docs/basedpython/features/differences-from-python.md b/docs/basedpython/features/differences-from-python.md
new file mode 100644
index 0000000000..2ebdc08b0d
--- /dev/null
+++ b/docs/basedpython/features/differences-from-python.md
@@ -0,0 +1,153 @@
+# differences from python
+
+`.by` is not a superset of `.py`. almost all python means the same thing in
+basedpython, and this page is the rest of it: every construct that reads
+differently, so that renaming a `.py` file to `.by` is a decision rather than a
+formality
+
+each one is a deliberate fix to something python cannot change without breaking
+the world
+
+!!! tip "you don't have to port by hand"
+
+    [`by transpile --reverse`](../getting-started.md#converting-python-to-basedpython)
+    rewrites python source into basedpython idioms, including the constructs
+    below
+
+## runtime behaviour
+
+the same source, running, does something else
+
+### `is` is an instance check
+
+`is` means `isinstance` and `===` means identity:
+
+| you write    | python does            |
+| ------------ | ---------------------- |
+| `x is y`     | `isinstance(x, y)`     |
+| `x is not y` | `not isinstance(x, y)` |
+| `x === y`    | `x is y`               |
+| `x !== y`    | `x is not y`           |
+
+the compiler doesn't always do `isinstance`, for example `x is None` will become `x is None` in
+python, this is because "type of x is None" and "value of x is None" have identical meanings
+
+see [identity and isinstance](identity-swap.md)
+
+### a mutable default is re-evaluated per call
+
+```by
+def append_one(items=[]):
+    items.append(1)
+    return items
+```
+
+python returns an ever-growing list; basedpython returns `[1]` every time. only
+non-scalar defaults are affected — numbers, bools, strings, `None` and `...`
+stay as plain python defaults. see
+[default argument re-evaluation](mutable-defaults.md)
+
+### a loop target is a fresh binding per iteration
+
+```by
+fns = []
+for i in [1, 2, 3]:
+    fns.append(lambda: print(i))
+```
+
+python prints `3 3 3`, because the loop has one cell shared by every iteration.
+basedpython prints `1 2 3`. comprehension targets bind the same way. see
+[unique loop bindings](unique-loop-bindings.md)
+
+### imports are lazy by default
+
+every `import` and `from ... import` in a `.by` file is marked lazy, so the
+module's body does not execute until something first touches it:
+
+```by
+import os
+
+print(os)   # this is what loads it
+```
+
+an import with a side effect — registering a plugin, patching something at
+module scope — no longer happens just because the importing module was loaded.
+`from __future__ import ...`, `from x import *`, and an unaliased `import a.b`
+stay eager. see [lazy imports](lazy-imports.md)
+
+## what an annotation means
+
+the same annotation denotes a different type
+
+### a string is a string type, not a forward reference
+
+```by
+x: "Foo"
+```
+
+python reads that as a deferred reference to the name `Foo`; basedpython reads
+it as the string-literal type. there is no manual forward-reference syntax
+because none is needed — the transpiler
+[quotes a self-reference for you](forward-references.md) when the
+runtime requires it
+
+### `float` means `float`
+
+python's typing spec special-cases `float` to mean `int | float`, and `complex`
+to mean `int | float | complex`. basedpython does not:
+
+```by
+def takes(x: float) -> None: ...
+
+takes(1)   # rejected
+```
+
+see [strict `float` and `complex`](no-number-promotions.md)
+
+### `class A[**Kwargs]` is keyword type arguments, not a parameter specification
+
+python's typing denotes that `**P` is a parameter specification, but basedpython
+generalises the concept as an upper bound of a standard type parameter:
+
+```by
+def f[P: (*: *, **: *)](fn: (**P) -> None): ...
+
+f[(int, str, foo: bool)]
+
+class HasKeywords[**Kwargs]
+
+HasKeywords[foo=int, bar=str]
+```
+
+see [generics](generics.md)
+
+## type checking
+
+the code runs the same; the checker's verdict differs
+
+### an unsolved type variable is `Never`
+
+where a type variable is never solved, python's checkers infer `Unknown` and
+stop checking. basedpython infers `Never` in covariant and bivariant positions,
+which keeps checking. see
+[precise unsolved type variables](precise-unsolved-typevars.md)
+
+### inference is sound where python's is gradual
+
+basedpython infers a precise type in places the spec allows a gradual one, so
+code that leaned on `Any` flowing through silently now reports. see
+[sound types](sound-types.md)
+
+### the stdlib is typed differently
+
+[typeshed improvements](typeshed.md) lists the whole set. the ones most
+likely to report on existing code:
+
+- an optional `re` capture group is `str | None`, not `Any`, so
+    `m.group(1).upper()` is an error
+- a `functools.cache`d function keeps its parameter list, so a wrong-arity call
+    to it is an error
+- `dict` / `set` keys are bounded by `Hashable`
+- a membership test checks that the operands
+    [overlap](overlapping.md), so `"a" in [1, 2]` is an error rather
+    than a guaranteed `False`
diff --git a/docs/basedpython/features/float-literals.md b/docs/basedpython/features/float-literals.md
index 2975958988..a02da5b4bf 100644
--- a/docs/basedpython/features/float-literals.md
+++ b/docs/basedpython/features/float-literals.md
@@ -105,6 +105,6 @@ surrounding whitespace) — constructs an ordinary `float`
 
 ```by
 def f(x: str) -> None:
-    reveal_type(float(x))  # revealed: float
-    reveal_type(float("1_000.5"))  # revealed: float
+    reveal_type(float(x))  # revealed: final float
+    reveal_type(float("1_000.5"))  # revealed: final float
 ```
diff --git a/docs/basedpython/features/implementations.md b/docs/basedpython/features/implementations.md
index e8a6440732..b5a0da8f79 100644
--- a/docs/basedpython/features/implementations.md
+++ b/docs/basedpython/features/implementations.md
@@ -331,7 +331,7 @@ implementation A for B:
 →
 
 ```python
-class __by_impl__A__B(_by_Implementation, A):  # basedpython: implementation A for B
+class _by_impl__A__B(_by_Implementation, A):  # basedpython: implementation A for B
     __slots__ = ()
 
     def f(self):
@@ -387,8 +387,8 @@ xs: list[A] = [b1, b2]
 →
 
 ```python
-f(__by_impl__A__B(b))
-xs: list[A] = [__by_impl__A__B(b1), __by_impl__A__B(b2)]
+f(_by_impl__A__B(b))
+xs: list[A] = [_by_impl__A__B(b1), _by_impl__A__B(b2)]
 ```
 
 when the implementation lives in another module, the lowering emits the precise
@@ -396,7 +396,7 @@ import of the witness class, keyed off the checker's resolution — the same
 implicit-import treatment extension members get:
 
 ```python
-from adapters import __by_impl__A__B
+from adapters import _by_impl__A__B
 ```
 
 ## round-tripping
@@ -497,7 +497,7 @@ settling separately. adding inherent members is what extensions are for
         (`project_db` + `transpile_typed`), beside
         `imported_extension_rewrites_call_and_adds_import`: a conversion site
         whose witness class lives in another module must wrap the expression *and*
-        emit `from impl_mod import __by_impl__A__B`, and the anonymous mangled
+        emit `from impl_mod import _by_impl__A__B`, and the anonymous mangled
         name must agree between the two files
     - **runtime** — an `implementation_runtime.rs` beside the other `*_runtime.rs`
         integration tests, for shared mutation through a witness, `==` / `hash`
diff --git a/docs/basedpython/features/index.md b/docs/basedpython/features/index.md
index 703763f9f7..f0379f8d4c 100644
--- a/docs/basedpython/features/index.md
+++ b/docs/basedpython/features/index.md
@@ -1,20 +1,62 @@
 # features
 
-the basedpython language reference
+the basedpython language reference — one page per feature, each with the
+surface syntax, what it checks, and the python it lowers to
+
+!!! tip "new here?"
+
+    [getting started](../getting-started.md) installs `by` and walks a `.by`
+    file through to running python. this page is the reference you come back to
+
+## python compatibility
+
+`.by` is not a superset of `.py`
+
+<div class="by-index" markdown>
+
+- [differences from python](differences-from-python.md) — every place the same
+    source reads differently
+
+</div>
 
 ## runtime compatibility
 
+what the transpiled python does at runtime, beyond what you wrote
+
+<div class="by-index" markdown>
+
 - [polyfills](polyfills.md) — write modern python, run it on older interpreters
 - [runtime type-soundness checks](soundness.md)
 
+</div>
+
 ## project-level
 
+features that apply to a project rather than to a file
+
+<div class="by-index" markdown>
+
 - [api lockfile (`api.lock`)](api-lock.md)
 
+</div>
+
+## standard library
+
+what basedpython's vendored typeshed says that upstream's does not
+
+<div class="by-index" markdown>
+
+- [typeshed improvements](typeshed.md) — covariant mapping keys, honest `re`
+    groups, precise `functools.cache`, and the rest
+
+</div>
+
 ## enhancements that also apply to python
 
 type-checking improvements with no new syntax — they work in `.by` and `.py` files alike
 
+<div class="by-index" markdown>
+
 - [fluid specializations](fluid-specializations.md)
 - [sound types](sound-types.md) — infer precise types instead of gradual ones
 - [precise unsolved type variables](precise-unsolved-typevars.md) — an unsolved type variable is
@@ -22,8 +64,14 @@ type-checking improvements with no new syntax — they work in `.by` and `.py` f
 - [regex group types](regex-groups.md) — type a match from the pattern it came from
 - [boolean conditions](conditions.md) — catch a test that conflates two members, or asks nothing
 
+</div>
+
 ## type system
 
+what a type is allowed to say
+
+<div class="by-index" markdown>
+
 - [tuple type literals](tuple-types.md)
 - [callable arrow syntax](callable.md)
 - [implicit receivers (`int.() -> str`)](implicit-receivers.md)
@@ -51,8 +99,14 @@ type-checking improvements with no new syntax — they work in `.by` and `.py` f
 - [implicit overload stubs](overloads.md)
 - [type narrowing predicates](type-is.md)
 
+</div>
+
 ## generics
 
+type parameters — their bounds, their variance, and what survives to runtime
+
+<div class="by-index" markdown>
+
 - [generics](generics.md)
 - [explicit typevar constraints](constraints.md)
 - [type parameter bound ranges](bound-ranges.md)
@@ -69,8 +123,14 @@ type-checking improvements with no new syntax — they work in `.by` and `.py` f
 - [type reification](type-reification.md)
 - [parametric type tests](parametric-type-tests.md)
 
+</div>
+
 ## declarations
 
+the forms a class, function or binding can take
+
+<div class="by-index" markdown>
+
 - [modifiers and visibility](modifiers.md)
 - [based enums (`enum class`)](enums.md)
 - [sealed classes](sealed-classes.md)
@@ -81,8 +141,14 @@ type-checking improvements with no new syntax — they work in `.by` and `.py` f
 - [`sentinel` declarations](sentinel.md)
 - [decorator keyword](decorator-keyword.md)
 
+</div>
+
 ## expressions and statements
 
+syntax inside a function body
+
+<div class="by-index" markdown>
+
 - [context-sensitive resolution](context-sensitive-resolution.md) — `a: Color = Red`
 - [identity and isinstance (`===` / `!==` / `is`)](identity-swap.md)
 - [optional chaining (`?.`)](optional-chaining.md)
@@ -107,15 +173,21 @@ type-checking improvements with no new syntax — they work in `.by` and `.py` f
 - [lazy imports](lazy-imports.md)
 - [export imports](export-imports.md) — `from x export y`
 - [extensions](extensions.md)
+- [implementations (`implementation A for B`)](implementations.md) — declare that
+    an existing type satisfies an existing interface
 - [conversions (`__from__` / `__into__` / `__of__`)](conversions.md)
 - [context parameters](context-parameters.md)
 - [local lifetimes (`local` / `once`)](local-lifetimes.md)
 - [exception tracking (`raises`)](exceptions.md)
 
+</div>
+
 ## formatting
 
-- [assignment alignment](assignment-alignment.md) — line up the `=` of consecutive assignments
+how the formatter lays basedpython out
 
-## planned
+<div class="by-index" markdown>
+
+- [assignment alignment](assignment-alignment.md) — line up the `=` of consecutive assignments
 
-- [implementations (`implementation A for B`)](implementations.md)
+</div>
diff --git a/docs/basedpython/features/keyword-variadic.md b/docs/basedpython/features/keyword-variadic.md
index be3c10c165..2b501fb12e 100644
--- a/docs/basedpython/features/keyword-variadic.md
+++ b/docs/basedpython/features/keyword-variadic.md
@@ -54,7 +54,7 @@ class A[**Kwargs]:
     init(**kwargs: **Kwargs)
 
 a = A(x=1, y="s")
-reveal_type(a)  # A[x=int, y=str]
+reveal_type(a)  # final A[x=int, y=str]
 ```
 
 the pack is solved as a whole rather than per-argument, so `A()` gives the empty pack `A[()]`. field
diff --git a/docs/basedpython/features/none-coalesce.md b/docs/basedpython/features/none-coalesce.md
index d548b10473..28ed632f6e 100644
--- a/docs/basedpython/features/none-coalesce.md
+++ b/docs/basedpython/features/none-coalesce.md
@@ -9,9 +9,13 @@ name = user.display_name ?? "anonymous"
 transpiles to:
 
 ```python
-name = user.display_name if user.display_name is not None else "anonymous"
+name = __by_t_0__ if (__by_t_0__ := user.display_name) is not None else "anonymous"
 ```
 
+a compound left operand is bound to a temp by the walrus so it is evaluated
+exactly once. a bare name needs no temp and is repeated directly — `a ?? b` is
+`a if a is not None else b`
+
 ## semantics
 
 `??` tests `is not None` (identity) — not falsiness. an empty string, zero,
diff --git a/docs/basedpython/features/not-type.md b/docs/basedpython/features/not-type.md
index da675ad5f0..9a413e9c77 100644
--- a/docs/basedpython/features/not-type.md
+++ b/docs/basedpython/features/not-type.md
@@ -6,7 +6,7 @@
 def f(x: not int) -> None: ...
 
 f("a")  # ok
-f()1)   # error
+f(1)    # error
 ```
 
 transpiles to:
diff --git a/docs/basedpython/features/overlapping.md b/docs/basedpython/features/overlapping.md
index 6074aeff29..bec685d760 100644
--- a/docs/basedpython/features/overlapping.md
+++ b/docs/basedpython/features/overlapping.md
@@ -5,10 +5,10 @@ it lets a [covariant](variance.md) (`out T`) class declare a
 method that *consumes* `T` without giving up covariance:
 
 ```by
-def f(xs: list[int]):
-    1 in xs         # ok - 1 overlaps with int
-    object() in xs  # ok - object overlaps with int
-    "a" in xs       # error - str does not overlap with int
+def f(xs: list[int], o: object):
+    1 in xs     # ok - 1 overlaps with int
+    o in xs     # ok - object overlaps with int
+    "a" in xs   # error - str does not overlap with int
 ```
 
 it is the loose sibling of [`SafeVariance`](safe-variance.md): both are asymmetric
@@ -23,17 +23,17 @@ class Mapping[out Key, out Value]:
         reveal_type(key)  # object — the upper bound of Key
         return True
 
-def f(m: Mapping[int, object]):
-    1 in m         # ok — int overlaps int
-    object() in m  # ok — object overlaps int (it could be an int)
-    "a" in m       # error — str is disjoint from int
+def f(m: Mapping[int, object], o: object):
+    1 in m     # ok — int overlaps int
+    o in m     # ok — object overlaps int (it could be an int)
+    "a" in m   # error — str is disjoint from int
 ```
 
 - **at the call site**, an argument is accepted iff it is *not disjoint from* the
     specialized `Key` — i.e. their types overlap (`Overlapping[T]` means exactly
     "not disjoint from `T`"). so a provably-unrelated argument like `"a"` is
-    rejected, but a could-be-a-`Key` argument like `object()` is allowed. this is
-    looser than a plain `Key` parameter (which would reject `object()`) and
+    rejected, but a could-be-a-`Key` argument like `o` is allowed. this is
+    looser than a plain `Key` parameter (which would reject `o`) and
     stricter than `object` (which would accept `"a"`)
 - **inside the body**, the parameter is seen as the upper bound of `Key`, so the
     consumed value can never be written back into `Key`-typed covariant storage.
@@ -82,6 +82,11 @@ a union is accepted whenever *any* member overlaps, matching the whole-operand
 behaviour of a membership test — `x: str | None` may be tested against a
 `dict[str, int]` because its `str` part overlaps the key
 
+precision cuts the other way for a bare constructor call: `object()` is inferred
+[`final object`](type-modifiers.md#a-constructor-call-is-inferred-final), meaning
+exactly `object` and never a subclass, which is *disjoint* from `int`. so
+`object() in xs` is rejected where a value declared `o: object` is accepted
+
 ## `Overlapping[T]` is a parameter annotation
 
 `Overlapping[T]` is only meaningful as a parameter annotation. inside the body
diff --git a/docs/basedpython/features/precise-unsolved-typevars.md b/docs/basedpython/features/precise-unsolved-typevars.md
index edec932740..6caa19d494 100644
--- a/docs/basedpython/features/precise-unsolved-typevars.md
+++ b/docs/basedpython/features/precise-unsolved-typevars.md
@@ -43,6 +43,7 @@ reveal_type(build(None))   # dict[Unknown, int]  — a `dict[Never, int]` could
 ```
 
 ```python
+def sink(x) -> None: ...
 def pipe[A, B](f: Callable[[A], B]) -> Callable[[A], B]: ...
 
 reveal_type(pipe(sink))    # (Unknown, /) -> None  — a `(Never, /)` could never be called
diff --git a/docs/basedpython/features/soundness.md b/docs/basedpython/features/soundness.md
index d9c4241f88..5b2490b667 100644
--- a/docs/basedpython/features/soundness.md
+++ b/docs/basedpython/features/soundness.md
@@ -64,7 +64,7 @@ def f(a: A[int]): ...
 with `parameters` enabled, `f` transpiles to:
 
 ```python
-def f(a):
+def f(a: A[int]):
     _soundness_parametric(a, A[int], (0,))
     ...
 ```
diff --git a/docs/basedpython/features/trailing-lambdas.md b/docs/basedpython/features/trailing-lambdas.md
index 6c64a1c704..e4a6a2a9e5 100644
--- a/docs/basedpython/features/trailing-lambdas.md
+++ b/docs/basedpython/features/trailing-lambdas.md
@@ -100,23 +100,26 @@ with a fresh block local. the lowering inserts the `global` / `nonlocal`
 declaration the closure needs, so no manual `nonlocal` is required:
 
 ```by
-a: int = 1
+n: int = 1
 f:
-    a = 2
-print(a)  # 2
+    n = 2
+print(n)  # 2
 ```
 
 →
 
 ```python
-a: int = 1
+n: int = 1
 def _trailing_lambda_0(it=None):
-    global a
-    a = 2
+    global n
+    n = 2
 f(a=_trailing_lambda_0)
-print(a)
+print(n)
 ```
 
+(`a` is `f`'s last parameter, from the definition at the top of the page — the
+keyword names the callback slot, not anything the block assigns)
+
 a module-level binding is captured with `global`, an enclosing function's local
 with `nonlocal`. a name bound in no enclosing scope stays a plain block local,
 and an attribute or item target (`obj.x = …`) rebinds no name, so neither is
diff --git a/docs/basedpython/features/type-reification.md b/docs/basedpython/features/type-reification.md
index 6ede2fcb2e..9a73c2e45e 100644
--- a/docs/basedpython/features/type-reification.md
+++ b/docs/basedpython/features/type-reification.md
@@ -1,30 +1,24 @@
 # type reification
 
 standard python erases inferred specializations: `A(1)` constructs an `A`
-with no record that it was an `A[int]`, and `[1, 2]` is just a `list`. the
-transpiler makes every inferred specialization explicit in the generated
-python, for generic constructor calls and for collection literals:
+with no record that it was an `A[int]`. the transpiler makes the inferred
+specialization of a user-defined generic constructor explicit in the generated
+python:
 
 ```by
 class A[T]:
     def __init__(self, t: T):
         self.t = t
 
-a = A(1)
-xs = [1, 2]
-d = {"k": 1}
-t = 1, "x"
-s = {3}
+a1 = A(1)
+a2 = A("x")
 ```
 
 →
 
 ```python
-a = A[int](1)
-xs = list[int]([1, 2])
-d = dict[str, int]({"k": 1})
-t = tuple[int, str]((1, "x"))
-s = set[int]({3})
+a1 = A[int](1)
+a2 = A[str]("x")
 ```
 
 `A[int](…)` routes through `types.GenericAlias.__call__`, which stamps
@@ -36,14 +30,29 @@ a = A(1)          # in basedpython source
 print(a.__orig_class__)   # A[int] at runtime
 ```
 
-the builtin collections silently reject the `__orig_class__` stamp, so for
-literals the reification lives in the generated source (and costs one extra
-constructor call); the constructed value is identical
-
 the stamp is what makes a runtime specialization visible — see
-[parametric type tests](parametric-type-tests.md) for `x is list[int]`, which
+[parametric type tests](parametric-type-tests.md) for `x is A[int]`, which
 reads it back.
 
+## collection literals stay bare
+
+a display is left exactly as written, even where its element type is known:
+
+```by
+xs = [1, 2]
+d = {"k": 1}
+s = {3}
+t = 1, "x"
+```
+
+the builtin collections silently reject the `__orig_class__` stamp, so
+`list[int]([1, 2])` constructs a value indistinguishable from `[1, 2]` — the
+wrap would carry no runtime information and cost a constructor call
+
+that is why a parametric test cannot read a specialization back off a builtin:
+`x is list[int]` resolves statically or through a [reified](reified-generics.md)
+type parameter instead
+
 ## where the types come from
 
 the injected spelling is read from the specialization ty already inferred for
@@ -55,35 +64,32 @@ separate solver, so the injected arguments never disagree with the checker, and
 usage-based widening of an inferred specialization flows straight into the
 injection
 
-an explicit specialization is always kept as written: `A[int](1)` and
-`list[int]([1, 2])` transpile unchanged
+an explicit specialization is always kept as written: `A[int](1)` transpiles
+unchanged, and is never wrapped twice
 
 ## best-effort, never an error
 
 unlike [reified type parameters](reified-generics.md) — where the runtime
 *needs* the type argument and an uninjectable bare call is a checker error —
-constructor and literal reification changes nothing the body can observe, so
-it simply doesn't fire when no runtime spelling exists:
+constructor reification changes nothing the body can observe, so it simply
+doesn't fire when no runtime spelling exists:
 
-- an unsolved or dynamic argument (`A()` inferred as `A[Unknown]`, `[]`)
-- a scope-local class (its bare name doesn't resolve at module scope)
-- a shadowed builtin (`list` rebound at module level)
-- a variable-length tuple (`(1, *rest)`)
+- an unsolved or dynamic argument — `A()` inferred as `A[Unknown]`, or `A(x)`
+    for an unannotated `x`
+- a type argument with no spelling at the call site, such as a class defined
+    inside a function: `A(Local())` stays bare
+- a non-generic class, which has no specialization to make explicit
 
 ## what never reifies
 
 - type expressions: annotations, type-parameter lists, `type X = …` values,
     and type-context subscript slices (the `[int]` list of a legacy
     `Callable[[int], str]` is type syntax, not a value)
-- dunders that static readers consume structurally: `__all__`, `__slots__`,
-    `__match_args__`
+- the values of dunders that static readers consume structurally: `__all__`,
+    `__slots__`, `__match_args__`
 - `sys.version_info` comparisons — every static reader (including ty on the
     generated python) must see the literal tuple gate
-- value-position subscript keys (`d[(1, 2)]`) — a key is a structural index
-    read verbatim by tuple-key and kw-subscript handling, not a constructed
-    value (displays nested inside a key still reify)
 - function parameter defaults — a non-scalar default is consumed whole by
     the [mutable defaults](mutable-defaults.md) lowering and re-evaluated in a
-    body guard. lambda defaults are not sentinel-lowered, so they reify
-- stubs (no runtime to observe) and targets below python 3.9 (pep 585 is
-    what makes the builtins subscriptable at runtime)
+    body guard. lambda defaults are not sentinel-lowered, so they do reify
+- stubs (no runtime to observe) and targets below python 3.9
diff --git a/docs/basedpython/features/typeshed.md b/docs/basedpython/features/typeshed.md
new file mode 100644
index 0000000000..d6afc80ee8
--- /dev/null
+++ b/docs/basedpython/features/typeshed.md
@@ -0,0 +1,157 @@
+# typeshed improvements
+
+basedpython vendors typeshed as `.byi` stubs, regenerated from upstream on every
+sync and then patched deterministically. some of those patches change what the
+stdlib's types *mean*; the rest change how they read. both are listed here —
+[typeshed patches](../development/typeshed-patches.md) covers how the machinery
+works
+
+## type fixes
+
+what basedpython's stdlib says that upstream's does not
+
+### mapping keys are covariant
+
+upstream declares `Mapping` with an invariant key. basedpython makes it
+covariant, so a `Mapping[str, int]` is a `Mapping[object, int]`:
+
+```by
+def f(m: Mapping[object, int]): ...
+
+f(dict[str, int](a=1))   # accepted
+```
+
+`MutableMapping` keeps an invariant key — `__setitem__` needs it
+
+### `re` capture groups are optional, not `Any`
+
+upstream types every "this group may not have participated" position as
+`AnyStr | MaybeNone`, and `MaybeNone` is `Any` — so calling a `str` method on a
+group that is `None` at runtime passes silently. basedpython spells the
+possibility out:
+
+```by
+m = re.match(r"(a)?(b)", s)
+m.group(1).upper()   # error: `str | None` has no attribute `upper`
+```
+
+this covers `Match.group`, `Match.groups`, `Match.groupdict`,
+`Match.__getitem__` and the `split` functions. where the pattern is a literal,
+[regex group types](regex-groups.md) reads it and gives something exact instead;
+this is the fallback for a pattern the checker cannot see
+
+### membership tests check for overlap
+
+`Container` is covariant in its element, so `in` consumes a covariant type
+variable in an input position. upstream gives up and types the parameter
+`object`. basedpython types it [`Overlapping[Element]`](overlapping.md) — a
+value is accepted if it is not disjoint from the element type:
+
+```by
+def f(xs: list[int], o: object):
+    1 in xs     # ok
+    o in xs     # ok — `object` overlaps `int`
+    "a" in xs   # error — `str` and `int` are disjoint
+```
+
+`Mapping` and `dict` apply the same treatment to `__getitem__` and `get`, which
+consume the covariant key
+
+### a fresh container widens at the call site
+
+an invariant container cannot be assigned to a wider specialization — a caller
+holding `list[int | None]` could insert a `None` into your `list[int]`. but a
+method returning a *brand new* container (`list.copy`, `list.__add__`, the set
+algebra, `dict.copy`, ...) hands back an object the caller solely owns, so
+widening it is sound:
+
+```by
+a: list[int] = [1]
+b: list[int | None] = a.copy()   # ok — nothing else holds the copy
+
+reveal_type(a.copy())            # still `list[int]`
+```
+
+it is a `Never`-defaulted type parameter unioned into the return type, so with
+no expected type inference is unchanged
+
+### `functools.cache` keeps the wrapped signature
+
+upstream parametrizes `_lru_cache_wrapper` by the return type only, so a cached
+function loses its parameter list:
+
+```by
+@cache
+def f(x: int) -> int: ...
+
+f(1, 2, 3)   # accepted upstream; an error in basedpython
+```
+
+basedpython captures the whole callable and recovers the signature through
+generic self-binding, with a `__get__` overload so a cached *method* is checked
+too — no `ParamSpec` or `Concatenate` spelling needed
+
+### hashable keys are required
+
+the key of `dict` and `frozendict`, and the element of `set` and `frozenset`,
+are bounded by `Hashable` — an unhashable key is a type error rather than a
+runtime `TypeError`
+
+### more covariance in `builtins`
+
+- `frozendict` is fully covariant — it has no mutators, so there is nothing to
+    make it invariant
+- the value projection of `type.__dict__` is covariant
+
+### borrowing builtins are marked `local`
+
+the builtins that cannot retain their argument take it as
+[`local`](local-lifetimes.md), so the checker knows the value does not escape
+the call
+
+### context-manager entry methods are abstract
+
+`AbstractContextManager.__enter__` and `AbstractAsyncContextManager.__aenter__`
+return `self`, which the type system cannot spell, so upstream marks them
+abstract
+
+### deletions
+
+- **mypy/pyright-only overloads** — typeshed carries overloads whose sole
+    purpose is to nudge another checker's inference, and which their own comments
+    describe as technically covered by a more general overload. `builtins.getattr`
+    is the clearest case. ty does not need them
+- **dead symbols** — `builtins.function`, a `@type_check_only` stand-in ty models
+    natively as `FunctionType`, and `typing.AwaitableGenerator`, which upstream
+    itself marks obsolete
+
+## idiom rewrites
+
+same meaning, written the way a `.by` file writes it
+
+- **pep 695 headers** — every legacy `TypeVar(...)` + `Generic[...]` class
+    becomes a pep 695 header with [explicit variance](variance.md) (`out` / `in` /
+    `in out`) and readable type-parameter names (`_KT_co` → `Key`, `_T_co` →
+    `Element`). this is the bulk of the diff
+- **`protocol` keyword** — `class C(Base, Protocol)` → [`protocol C(Base)`](inline-protocol.md)
+- **arrow callables** — `Callable[[A, B], R]` → [`(A, B) -> R`](callable.md)
+- **bare literals** — `Literal[a, b]` → [`a | b`](literal-types.md)
+- **`final` modifier** — a `@final` decorator stacked with others becomes the
+    [`final`](modifiers.md) class or def modifier
+- **`final` declarations** — `x: Final[T]` → `final x: T`
+- **`init` shorthand** — a plain `def __init__(self, ...) -> None` →
+    [`init(self, ...)`](init-method.md)
+- **read-only properties** — a non-computed `@property` → a valueless
+    [`let NAME: T`](properties.md), which declares the same thing without the
+    descriptor machinery
+- **type-alias statements** — a non-generic `X: TypeAlias = V` → `type X = V`
+- **private aliases and protocols** — an underscore-prefixed alias or protocol
+    that nothing outside its module uses →
+    `private type X` / `private protocol X`
+- **homogeneous tuples** — `tuple[X, ...]` → [`(*: X)`](tuple-types.md)
+- **`dynamic`** — every surviving `Any` → [`dynamic`](dynamic.md)
+- **implicit typing imports** — the `from typing import ...` names basedpython
+    [provides implicitly](implicit-typing.md) are dropped; runtime helpers stay
+- **cleanups** — another checker's suppression comments, leftover `: ...` bodies
+    on decorated stubs, stranded private typevars, and stray upstream comments
+    about mypy quirks are all removed
diff --git a/docs/basedpython/frameworks/index.md b/docs/basedpython/frameworks/index.md
index 45aabb7326..0f6bbc294a 100644
--- a/docs/basedpython/frameworks/index.md
+++ b/docs/basedpython/frameworks/index.md
@@ -1,48 +1,93 @@
 # framework support
 
-basedpython provides deep support for popular python frameworks. the type checker understands framework-specific patterns, and the transpiler keeps basedpython features compatible with framework runtime behavior.
+the type checker understands framework-specific patterns, and the transpiler
+keeps basedpython features working inside them
 
-supported frameworks: [Pydantic](pydantic.md), [SQLAlchemy](sqlalchemy.md), [pytest](pytest.md), and [Django](django.md).
+<div class="grid cards" markdown>
+
+- :simple-pydantic:{ .lg .middle } **[Pydantic](pydantic.md)**
+
+    ______________________________________________________________________
+
+    model fields, synthesized constructors, validators, and generic models
+
+- :simple-sqlalchemy:{ .lg .middle } **[SQLAlchemy](sqlalchemy.md)**
+
+    ______________________________________________________________________
+
+    2.0 declarative models, `Mapped[T]` columns, and mixins
+
+- :simple-pytest:{ .lg .middle } **[pytest](pytest.md)**
+
+    ______________________________________________________________________
+
+    fixture injection typed end to end, plus diagnostics for fixtures that
+    don't exist
+
+- :simple-django:{ .lg .middle } **[Django](django.md)**
+
+    ______________________________________________________________________
+
+    model fields, reverse accessors, and querysets, on a library with no
+    annotations of its own
+
+</div>
 
 ## what framework support means
 
 when you use a supported framework with basedpython:
 
-- **type checking works precisely** — the checker understands framework magic like synthesized constructors, descriptor fields, and dependency injection, so your `.by` code checks correctly
-- **transpilation stays compatible** — basedpython features (like checked cast, optional chaining, reified generics) work correctly inside framework constructs, tested against the real framework
-- **framework-specific diagnostics** — you get checks that make sense for the framework (unknown fixture names in pytest, invalid field lookups in django, etc.)
+- **type checking works precisely** — the checker understands framework magic
+    like synthesized constructors, descriptor fields, and dependency injection,
+    so your `.by` code checks correctly
+- **transpilation stays compatible** — basedpython features (like checked cast,
+    optional chaining, reified generics) work correctly inside framework
+    constructs, tested against the real framework
+- **framework-specific diagnostics** — you get checks that make sense for the
+    framework (unknown fixture names in pytest, invalid field lookups in django,
+    and so on)
 
 ## framework support limitations
 
-framework support is graceful: if a pattern is too dynamic to type-check, the checker falls back to ordinary inference rather than guessing. this means:
+framework support is graceful: if a pattern is too dynamic to type-check, the
+checker falls back to ordinary inference rather than guessing. this means:
 
 - a framework not installed → no special checking activates for it
-- a pattern the checker can't resolve → you'll see an `unknown attribute` error, which you can annotate around if needed
+- a pattern the checker can't resolve → you'll see an `unresolved-attribute`
+    error, which you can annotate around if needed
 - a limitation → documented in the framework's page with a workaround
 
-framework support is also **not exhaustive**. each framework has a conformance matrix showing what works and what doesn't, including baseline limitations of the framework itself (e.g., django has no type annotations at all, so field types must come from stubs).
-
-## getting started
-
-check each framework's documentation to learn what works, what doesn't, and any limitations or required setup (like installing additional stubs packages).
+framework support is also **not exhaustive**. each framework has a conformance
+matrix showing what works and what doesn't, including baseline limitations of
+the framework itself — django, for instance, has no type annotations at all, so
+field types must come from stubs
 
 ## basedpython features and framework compatibility
 
-basedpython features generally work well inside framework code, but some patterns interact with framework syntax and have restrictions:
-
-- **`init` shorthand and `data class` modifiers** — these conflict with frameworks that synthesize their own constructors (pydantic, sqlalchemy, django). you'll get an error if you try to use them in a framework model or declarative class
-- **basedpython enums as fields** — payload-less enums work fine; payload enums also work but have limitations in some frameworks
-- **reified generics** — works with generic framework classes (e.g., pydantic's generic models), but the transpiler never wraps a framework class itself with the generic machinery
-- **optional chaining, checked cast, coalesce** — all work correctly inside framework code
+basedpython features generally work well inside framework code, but some
+patterns interact with framework syntax and have restrictions:
+
+- **`init` shorthand and `data class` modifiers** — these conflict with
+    frameworks that synthesize their own constructors (pydantic, sqlalchemy,
+    django). you'll get an error if you try to use them in a framework model or
+    declarative class
+- **basedpython enums as fields** — payload-less enums work fine; payload enums
+    also work but have limitations in some frameworks
+- **reified generics** — works with generic framework classes (e.g., pydantic's
+    generic models), but the transpiler never wraps a framework class itself
+    with the generic machinery
+- **optional chaining, checked cast, coalesce** — all work correctly inside
+    framework code
 - **lazy imports** — compatible with framework registration and initialization
 
-each framework page details its specific limitations.
+each framework page details its specific limitations
 
 ## future candidates
 
 worth supporting next, in rough value-per-effort order:
 
-- **attrs** — minimal friction, mostly works through existing dataclass machinery
+- **attrs** — minimal friction, mostly works through existing dataclass
+    machinery
 - **fastapi** — high value; reuses pydantic support and pytest fixture injection
 - **msgspec** — compact struct support
 - **typer / click** — decorator-based parameter DSL
diff --git a/docs/basedpython/getting-started.md b/docs/basedpython/getting-started.md
index 961b779da7..5e46379f76 100644
--- a/docs/basedpython/getting-started.md
+++ b/docs/basedpython/getting-started.md
@@ -1,12 +1,20 @@
 # getting started
 
+install `by`, write a `.by` file, and run it. everything below takes about five
+minutes
+
 ## installation
 
-```sh
-uv add --dev basedpython
-```
+basedpython ships as the `basedpython` package, which installs two executables:
+`by`, the type checker and transpiler, and `buff`, the linter and formatter
 
-this installs the `by` CLI. verify it works:
+=== "uv"
+
+    ```sh
+    uv add --dev basedpython
+    ```
+
+verify it works:
 
 ```sh
 by --help
@@ -27,7 +35,14 @@ run it directly:
 by run main
 ```
 
-`by run main` finds `main.by` in the current directory, transpiles it (and all other `.by` files in the project) to a temporary directory, then executes `python -m main` from there
+`by run main` finds `main.by` in the current directory, transpiles it (and all
+other `.by` files in the project) to a temporary directory, then executes
+`python -m main` from there
+
+!!! note "`by run` takes a module, not a path"
+
+    the argument is what you would pass to `python -m`, so it is `main`, not
+    `main.by` — and a nested entry point is `pkg.main`
 
 naming the module every time gets old once a project has an entry point. configure one and `by run` alone is enough:
 
@@ -46,27 +61,10 @@ main = "main"
 
 see [configuration](configuration.md) for everything that can go in there
 
-## project layout
-
-a typical basedpython project looks like:
-
-```text
-myproject/
-├── main.by
-├── utils.by
-├── out/          # transpiled .py output — gitignore this
-└── pyproject.toml
-```
-
-add the output directory to `.gitignore`:
-
-```text
-out/
-```
-
 ## building
 
-`by build` transpiles all `.by` files in the project and writes the output to `out/`, mirroring the source structure:
+`by build` transpiles all `.by` files in the project and writes the output to
+`out/`, mirroring the source structure:
 
 ```sh
 by build
@@ -88,8 +86,6 @@ mypy out/
 ruff check out/
 ```
 
-type checkers and linters operate on the generated Python. if your editor shows type errors in `.by` files, point it at the corresponding `.py` output instead
-
 ## CI integration
 
 ```yaml
@@ -102,17 +98,91 @@ type checkers and linters operate on the generated Python. if your editor shows
   run: pytest out/
 ```
 
+## converting python to basedpython
+
+you don't have to start from an empty file. `by transpile --reverse` runs the
+transpiler backwards, rewriting python source into the basedpython idiom it
+would have lowered from:
+
+```sh
+by transpile --reverse legacy.py
+```
+
+```py
+from typing import Callable, Optional
+
+
+class Node:
+    children: list["Node"]
+
+    def __eq__(self, other: object) -> bool:
+        if other is self:
+            return True
+        return isinstance(other, Node) and other.children == self.children
+
+    def find(self, key: str) -> Optional["Node"]: ...
+
+
+on_visit: Callable[[Node], None]
+```
+
+comes back as:
+
+```by
+from typing import Optional
+
+
+class Node:
+    children: list[Node]
+
+    def __eq__(self, other: object) -> bool:
+        if other === self:
+            return True
+        return other is Node and other.children == self.children
+
+    def find(self, key: str) -> Optional[Node]
+
+
+on_visit: (Node) -> None
+```
+
+the identity fast path became `===` and the `isinstance` became
+[`is`](features/identity-swap.md), the quotes came off the self-references,
+`Callable[[Node], None]` became an [arrow type](features/callable.md), the
+`: ...` body became an [empty declaration](features/empty-declarations.md), and
+the now-unused `Callable` import was pruned
+
+point it at a directory to convert a whole tree in place, every `.py` to a
+`.by`:
+
+```sh
+by transpile --reverse src/
+```
+
+each reverse transform mirrors a forward one, so a converted file transpiles
+back to the program you started with
+
+!!! warning "read the diff"
+
+    reversing converts the constructs that have a reverse transform and leaves
+    the rest alone — `__init__` does not become
+    [`init(...)`](features/init-method.md), `Optional[T]` does not become `T?`.
+    it is a head start, not a port. run `by check` on the result, and read
+    [differences from python](features/differences-from-python.md) before you
+    commit it
+
 ## low-level: single file transpilation
 
-`by transpile` is the low-level command for single-file transforms. it reads a file (or stdin) and writes the transpiled Python to stdout:
+`by transpile` is the low-level command for single-file transforms. it reads a
+file (or stdin) and writes the transpiled python to stdout:
 
 ```sh
 by transpile hello.by
-echo 'x[(a, b)]' | by transpile
-# → x[(a, b),]
+echo 'a = b ?? 1' | by transpile
+# → a = b if b is not None else 1
 ```
 
-output always goes to stdout — redirect it to a file if you want to keep it
+output goes to stdout - redirect it to a file if you want to keep it
 (`by transpile hello.by > hello.py`). use `by build` to transpile a whole
 project into `out/`
 
@@ -133,3 +203,33 @@ evaluated lazily (PEP 649), and if you target an older runtime but want
 every annotation deferred anyway you can opt into a blanket
 `from __future__ import annotations` — in either case the reference is left
 as-is
+
+## next
+
+<div class="grid cards" markdown>
+
+- :lucide-book-open:{ .lg .middle } **[the feature reference](features/index.md)**
+
+    ______________________________________________________________________
+
+    every piece of syntax basedpython adds, one page at a time
+
+- :lucide-package:{ .lg .middle } **[framework support](frameworks/index.md)**
+
+    ______________________________________________________________________
+
+    what changes when pydantic, sqlalchemy, pytest or django is in the project
+
+- :lucide-terminal:{ .lg .middle } **[`by` CLI reference](cli-reference.md)**
+
+    ______________________________________________________________________
+
+    every command and flag, including the ones inherited from `ty`
+
+- :lucide-arrow-right-left:{ .lg .middle } **[how transpilation works](development/how-transpilation-works.md)**
+
+    ______________________________________________________________________
+
+    what happens between the `.by` file and the python that runs
+
+</div>
diff --git a/docs/basedpython/index.md b/docs/basedpython/index.md
index b94ff3f691..eab5adde62 100644
--- a/docs/basedpython/index.md
+++ b/docs/basedpython/index.md
@@ -1,6 +1,23 @@
 # basedpython
 
-a python-like language that transpiles to pure python
+<p class="by-tagline" markdown>
+a python-like language that transpiles to pure python — sum types, extensions,
+optional chaining and a type system that knows what your code means, lowered to
+files any python tool can read
+</p>
+
+- **a python type checker with [framework support](frameworks/index.md)** —
+    pydantic, sqlalchemy, pytest and django are modelled directly, so the magic
+    they do at runtime checks like ordinary code
+- **basedpython, a python-like language that builds into python wheels**
+- **compiles into high performance python extension modules**
+- **a language server, formatter and linter** — `by server` drives the editor,
+    and `buff` is the basedpython build of ruff
+
+<div class="by-actions" markdown>
+[get started](getting-started.md){ .md-button .md-button--primary }
+[browse the features](features/index.md){ .md-button }
+</div>
 
 ```by
 enum class Shape:
@@ -8,9 +25,11 @@ enum class Shape:
     case Rect(width: int, height: int)
 
     def area(self) -> int:
-        match self:
-            case Shape.Circle(r): return 3 * r * r
-            case Shape.Rect(w, h): return w * h
+        return match self:
+            case Shape.Circle(r):
+                3 * r * r
+            case Shape.Rect(w, h):
+                w * h
 
 extension list[Element: Shape]:
     def first_circle(self) -> Shape.Circle?:
@@ -29,21 +48,90 @@ def main():
     print(shapes.first_circle()?.radius ?? 0)
 ```
 
-## contents
+## what you get
+
+<div class="grid cards" markdown>
+
+- :lucide-file-code-2:{ .lg .middle } **plain python out the other end**
+
+    ______________________________________________________________________
+
+    `by build` writes ordinary `.py` files. pytest, mypy, ruff and everything
+    else in your stack keep working, because what they see is python
+
+    [:octicons-arrow-right-24: how transpilation works](development/how-transpilation-works.md)
+
+- :lucide-shapes:{ .lg .middle } **syntax python doesn't have**
+
+    ______________________________________________________________________
+
+    sum types with payloads, extension methods, destructuring, trailing lambda
+    blocks, `?.`, `??`, and properties that read like declarations
+
+    [:octicons-arrow-right-24: the language reference](features/index.md)
+
+- :lucide-shield-check:{ .lg .middle } **a type system that keeps up**
+
+    ______________________________________________________________________
+
+    intersections, negations, match types, symbolic arithmetic in type
+    parameters, and inference that narrows instead of shrugging
+
+    [:octicons-arrow-right-24: type system features](features/index.md#type-system)
+
+- :lucide-blocks:{ .lg .middle } **frameworks understood, not tolerated**
+
+    ______________________________________________________________________
+
+    pydantic, sqlalchemy, pytest and django are modelled directly, so
+    synthesized constructors and injected fixtures check like real code
+
+    [:octicons-arrow-right-24: framework support](frameworks/index.md)
+
+</div>
+
+## where to go
+
+<div class="grid cards" markdown>
+
+- :lucide-rocket:{ .lg .middle } **[getting started](getting-started.md)**
+
+    ______________________________________________________________________
+
+    install, your first `.by` file, project layout, and wiring `by build` into
+    CI
+
+- :lucide-book-open:{ .lg .middle } **[features](features/index.md)**
+
+    ______________________________________________________________________
+
+    the full language reference, one page per feature
+
+- :lucide-settings:{ .lg .middle } **[configuration](configuration.md)**
+
+    ______________________________________________________________________
+
+    where settings live and how they resolve
+
+- :lucide-package:{ .lg .middle } **[framework support](frameworks/index.md)**
+
+    ______________________________________________________________________
+
+    what basedpython knows about pydantic, sqlalchemy, pytest and django
+
+- :lucide-triangle-alert:{ .lg .middle } **[differences from python](features/differences-from-python.md)**
+
+    ______________________________________________________________________
+
+    every place the same source means something different in a `.by` file
 
-- [getting started](getting-started.md) — install, your first file, project layout
-- [configuration](configuration.md) — where settings live and how they resolve
-- [features](features/index.md) — the full language reference
-- [framework support](frameworks/index.md) — popular python library support
-- [`by` cli reference](cli-reference.md) — commands and flags
+- :lucide-terminal:{ .lg .middle } **[`by` CLI reference](cli-reference.md)**
 
-## development
+    ______________________________________________________________________
 
-- [how transpilation works](development/how-transpilation-works.md)
-- [reverse transforms](development/reverse-transforms.md)
-- [sourcemaps](development/sourcemaps.md)
-- [typeshed patches](development/typeshed-patches.md)
+    every command and flag the `by` driver adds
 
-## acknowledgements
+</div>
 
-- [third-party work basedpython relies on](acknowledgements.md)
+[credits](credits.md) for contributors and the
+third-party work basedpython relies on
diff --git a/docs/basedpython/stylesheets/extra.css b/docs/basedpython/stylesheets/extra.css
new file mode 100644
index 0000000000..14526b8fd4
--- /dev/null
+++ b/docs/basedpython/stylesheets/extra.css
@@ -0,0 +1,97 @@
+/* basedpython documentation theme
+ *
+ * the theme this builds on is already close to what we want, so everything
+ * here is either something the theme has no concept of (inlay hints, the
+ * landing hero) or a place the reference's shape strains the default (a
+ * ninety-page feature nav, cards used as link indexes)
+ */
+
+/* --- landing hero ------------------------------------------------------ */
+
+.by-tagline {
+  color: var(--md-default-fg-color--light);
+  font-size: 1.1rem;
+  font-weight: 300;
+  line-height: 1.5;
+  margin: 0.6em 0 1.2em;
+  max-width: 34em;
+}
+
+/* the hero buttons sit directly under the tagline, so they need to breathe
+   without inheriting the paragraph's line height */
+.by-actions {
+  display: flex;
+  flex-wrap: wrap;
+  gap: 0.5rem;
+  margin: 0 0 2rem;
+}
+
+.by-actions .md-button {
+  margin: 0;
+}
+
+/* --- cards ------------------------------------------------------------- */
+
+/* the theme colours a card's leading icon like body text; an accent makes a
+   grid of them scannable */
+.md-typeset .grid.cards > ul > li > p:first-child .twemoji {
+  color: var(--md-accent-fg-color);
+}
+
+/* a card's heading is usually also its link. underlining it makes a grid of
+   cards read as a list of links rather than as a set of headings */
+.md-typeset .grid.cards > ul > li > p:first-child > strong > a {
+  color: var(--md-default-fg-color);
+  text-decoration: none;
+}
+
+.md-typeset .grid.cards > ul > li:hover > p:first-child > strong > a {
+  color: var(--md-accent-fg-color);
+}
+
+/* --- the feature index -------------------------------------------------- */
+
+/* the reference has ninety pages in nine sections, two of which are nearly
+ * thirty entries long. as one column that is a page of scrolling; columns keep
+ * a section on screen at once, which is the whole point of an index */
+.by-index ul {
+  column-gap: 2.4rem;
+  columns: 2;
+}
+
+.by-index li {
+  break-inside: avoid;
+}
+
+@media screen and (max-width: 76.234375em) {
+  .by-index ul {
+    columns: 1;
+  }
+}
+
+/* --- inlay hints -------------------------------------------------------- */
+
+/* the docs write what an editor renders — an inferred specialization, an
+ * injected argument — between angle brackets. the `by` lexer gives that its own
+ * token so it can look like the hint it stands for, and not like source
+ *
+ * `.err` is here because the notation also appears in a `python` block, where
+ * no lexer knows it. `scripts/check_by_lexer.py` enforces that this is the only
+ * thing in the docs that lexes to an error token */
+.md-typeset .highlight .cs,
+.md-typeset .highlight .err {
+  background-color: var(--md-default-fg-color--lightest);
+  border-radius: 0.2rem;
+  color: var(--md-default-fg-color--light);
+  font-style: normal;
+  padding: 0 0.2em;
+}
+
+/* --- navigation --------------------------------------------------------- */
+
+/* the feature reference is deep and its titles are long. wrapping is better
+   than truncation here, but the default line height makes a wrapped item hard
+   to tell from two items */
+.md-nav__link {
+  line-height: 1.3;
+}
diff --git a/pyproject.toml b/pyproject.toml
index 3754003d35..00fa263ba9 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -65,14 +65,20 @@ dev = [
     "prek==0.4.9",
 ]
 docs = [
+    "basedpython-pygments",
     "zensical",
 ]
 release = [
     "rooster==0.1.1",
 ]
 
+[tool.uv.sources]
+# the pygments lexer that highlights `by` code blocks in the docs
+basedpython-pygments = { path = "python/basedpython-pygments" }
+
 [tool.uv.dependency-groups]
 dev = { requires-python = ">=3.12" }
+docs = { requires-python = ">=3.12" }
 release = { requires-python = ">=3.12" }
 
 [tool.ruff]
@@ -112,6 +118,12 @@ ignore = [
     "E501"
 ]
 
+[tool.ruff.lint.per-file-ignores]
+# a pygments lexer declares its public api as plain class attributes, and the
+# framework reads `tokens` at class-creation time. `ClassVar` annotations would
+# be correct at runtime but unique to this lexer among every lexer pygments has
+"python/basedpython-pygments/**" = ["RUF012"]
+
 [tool.ruff.lint.isort]
 required-imports = ["from __future__ import annotations"]
 combine-as-imports = true
diff --git a/python/basedpython-pygments/README.md b/python/basedpython-pygments/README.md
new file mode 100644
index 0000000000..d3055e96d8
--- /dev/null
+++ b/python/basedpython-pygments/README.md
@@ -0,0 +1,23 @@
+# basedpython-pygments
+
+a [pygments](https://pygments.org) lexer for basedpython, so that ```` ```by ```` code
+blocks in the documentation are syntax highlighted
+
+pygments picks the lexer up from an entry point, so nothing needs to reference it —
+installing the package is enough. it is pulled into the `docs` dependency group of the
+repository root, which is what the docs build installs
+
+```sh
+uv sync --group docs --no-install-project
+uv run --no-sync zensical serve
+```
+
+## keeping it honest
+
+basedpython's added keywords are soft: `get`, `data` and `out` are all still ordinary
+identifiers, and the real parser tells them apart by position. the lexer approximates
+that with per-keyword lookaheads, so it can drift from the language
+
+`scripts/check_by_lexer.py` runs the lexer over every `by` block in `docs/basedpython`
+and fails if a block produces an error token, or if a keyword the docs demonstrate does
+not come out as a keyword. it runs in `prek`
diff --git a/python/basedpython-pygments/basedpython_pygments/__init__.py b/python/basedpython-pygments/basedpython_pygments/__init__.py
new file mode 100644
index 0000000000..7feb85330f
--- /dev/null
+++ b/python/basedpython-pygments/basedpython_pygments/__init__.py
@@ -0,0 +1,163 @@
+"""a pygments lexer for basedpython
+
+the docs are almost entirely ```by``` code, and pygments has no idea what `by`
+is — every block used to render as undifferentiated plain text. this lexer
+extends pygments' python lexer with basedpython's surface syntax so the
+reference reads like code instead of a wall of grey
+
+basedpython's added keywords are all *soft*: `get`, `data`, `out` and friends
+stay perfectly good identifiers, and the parser tells them apart by position.
+a regex lexer has no parser to ask, so the rules below fall into two tiers:
+
+- `RESERVED` — words with no python meaning and no plausible use as a name.
+  matched anywhere
+- everything else — matched only through a lookahead that mirrors the
+  grammatical position the keyword is legal in, so `data class Point` reads as
+  a modifier while `def f(data: bytes)` reads as a parameter
+
+`scripts/check_by_lexer.py` runs this over every `by` block in the docs and
+checks both tiers, so a new keyword that isn't wired up here gets caught
+"""
+
+from __future__ import annotations
+
+from pygments.lexer import bygroups, inherit, words
+from pygments.lexers.python import PythonLexer
+from pygments.token import Comment, Keyword, Name, Operator, Whitespace
+
+__all__ = ["BasedPythonLexer"]
+
+#: keywords that shadow nothing in python and read as keywords wherever they
+#: appear
+RESERVED = (
+    "asserts",
+    "export",
+    "extension",
+    "implementation",
+    "let",
+    "raises",
+    "reified",
+    "typeof",
+)
+
+#: modifiers that may be written, in any order and any number, ahead of the
+#: declaration they modify
+MODIFIERS = (
+    "abstract",
+    "data",
+    "enum",
+    "final",
+    "frozen",
+    "late",
+    "open",
+    "override",
+    "private",
+    "public",
+    "sealed",
+    "static",
+)
+
+#: what a modifier chain is allowed to end in — a further modifier, or the
+#: keyword that actually introduces the declaration
+INTRODUCERS = (
+    "async",
+    "class",
+    "def",
+    "extension",
+    "implementation",
+    "let",
+    "type",
+    "var",
+)
+
+#: modifiers written ahead of a parameter, binding its lifetime or promoting it
+#: to an attribute
+PARAM_MODIFIERS = ("local", "once", "var", "let")
+
+#: modifiers written ahead of a type in a type expression
+TYPE_MODIFIERS = ("final", "literal")
+
+#: accessor blocks inside a property construct. these share their spelling with
+#: very common method names (`d.get(k)`), so they only count at the head of a
+#: line, where a `def` would otherwise go
+ACCESSORS = ("field", "get", "set")
+
+
+def _any(candidates: tuple[str, ...]) -> str:
+    return "|".join(candidates)
+
+
+class BasedPythonLexer(PythonLexer):
+    """basedpython — python's lexer plus basedpython's surface syntax"""
+
+    name = "basedpython"
+    url = "https://kotlinisland.github.io/basedpython/"
+    aliases = ["by", "basedpython"]
+    filenames = ["*.by", "*.byi"]
+    mimetypes = ["text/x-basedpython"]
+
+    tokens = {
+        "keywords": [
+            (words(RESERVED, prefix=r"\b", suffix=r"\b"), Keyword),
+            # `x cast int`, `x cast? int` — infix, so never followed by a call.
+            # `cast(...)` stays the ordinary `typing.cast`
+            (r"\bcast\?(?!\w)|\bcast\b(?!\s*\()", Keyword),
+            # a modifier only binds when something modifiable follows it. the
+            # lookahead accepts another modifier, which is what lets a chain
+            # like `frozen data class` resolve one word at a time
+            (
+                rf"\b(?:{_any(MODIFIERS)})\b(?=\s+(?:{_any(MODIFIERS + INTRODUCERS)})\b)",
+                Keyword,
+            ),
+            # `x: literal int`, `xs: final list[int]`
+            (rf"(?<![\w.])(?:{_any(TYPE_MODIFIERS)})(?=\s+[A-Za-z_])", Keyword),
+            # `def f(local xs: list[int])`, `init(var name: str)`
+            (rf"\b(?:{_any(PARAM_MODIFIERS)})\b(?=\s+[A-Za-z_]\w*\s*[:,)=])", Keyword),
+            # `class Mapping[out Key, out Value]`
+            (r"(?<![\w.])out(?=\s+[A-Za-z_])", Keyword),
+            # `sentinel MISSING`
+            (r"\bsentinel(?=\s+[A-Za-z_])", Keyword),
+            # `class C[T: constraints (int, str)]`
+            (r"\bconstraints(?=\s*\()", Keyword),
+            # `protocol(a: int; def f(self) -> int)`
+            (r"\bprotocol(?=\s*\()", Keyword),
+            inherit,
+        ],
+        "builtins": [
+            # `dynamic` is basedpython's spelling of `Any`
+            (r"(?<![\w.])dynamic\b", Keyword.Type),
+            inherit,
+        ],
+        "expr": [
+            # the docs write an inlay hint — what the editor renders, not what
+            # the file contains — between angle brackets
+            (r"⟨[^⟩\n]*⟩", Comment.Special),
+            # `a?.b` optional chaining, `a ?? b` none-coalesce, `T?` optional
+            (r"\?\.|\?\?|\?", Operator),
+            # `a === b` / `a !== b` identity
+            (r"===|!==", Operator),
+            # `expr!` force-unwrap. `!=` stays python's inequality
+            (r"!(?!=)", Operator),
+            inherit,
+        ],
+        "root": [
+            # a property accessor stands where a `def` would, so it only counts
+            # at the head of a line. `d.get(k)` and `def get(self)` keep their
+            # name token
+            (
+                rf"^([ \t]*)({_any(ACCESSORS)})\b(?=\s*[(:=])",
+                bygroups(Whitespace, Keyword),
+            ),
+            # `enum class Shape:` / `case Circle(radius: int)` — a variant
+            # declaration reads like the class header it lowers to
+            (
+                r"^([ \t]*)(case)(\s+)([A-Za-z_]\w*)",
+                bygroups(Whitespace, Keyword, Whitespace, Name.Class),
+            ),
+            inherit,
+        ],
+    }
+
+    def analyse_text(self, text: str) -> float:
+        # never win a fight with the python lexer over a `.py` file
+        return 0.0
diff --git a/python/basedpython-pygments/pyproject.toml b/python/basedpython-pygments/pyproject.toml
new file mode 100644
index 0000000000..dd4dccfacb
--- /dev/null
+++ b/python/basedpython-pygments/pyproject.toml
@@ -0,0 +1,19 @@
+[project]
+name = "basedpython-pygments"
+version = "0.0.0"
+description = "a pygments lexer for basedpython, used to highlight `by` code in the docs"
+readme = "README.md"
+requires-python = ">=3.9"
+dependencies = ["pygments>=2.19"]
+
+# pygments discovers third-party lexers through this entry point group, so
+# installing the package is all it takes for ```by``` fences to highlight
+[project.entry-points."pygments.lexers"]
+basedpython = "basedpython_pygments:BasedPythonLexer"
+
+[build-system]
+requires = ["hatchling"]
+build-backend = "hatchling.build"
+
+[tool.hatch.build.targets.wheel]
+packages = ["basedpython_pygments"]
diff --git a/scripts/check_by_lexer.py b/scripts/check_by_lexer.py
new file mode 100644
index 0000000000..a492ae59a3
--- /dev/null
+++ b/scripts/check_by_lexer.py
@@ -0,0 +1,176 @@
+"""check the basedpython pygments lexer against the docs it highlights
+
+`python/basedpython-pygments` approximates basedpython's soft keywords with
+lookaheads rather than a parser, so it can drift from the language. three checks
+keep it anchored:
+
+1. every ```by``` block in `docs/basedpython` lexes without producing an error
+   token
+2. across every *other* fenced language, the only text that lexes to an error
+   token is the docs' inlay-hint notation, which no stock lexer knows. the
+   stylesheet leans on that: it renders an error token like the hint it stands
+   for, which is only safe while nothing else produces one
+3. a table of snippets, one per keyword, comes out classified as a keyword.
+   this is what catches a keyword being added to the language and to the docs
+   but never to the lexer
+
+run directly, or through `prek`
+"""
+
+from __future__ import annotations
+
+import re
+import sys
+from pathlib import Path
+
+from pygments.lexers import get_lexer_by_name
+from pygments.token import Error, Keyword
+from pygments.util import ClassNotFound
+
+ROOT = Path(__file__).parent.parent
+DOCS = ROOT / "docs/basedpython"
+
+# a fence may be indented, inside a list item or an admonition
+FENCE = re.compile(r"^([ \t]*)```([\w+-]*)\n(.*?)^\1```", re.DOTALL | re.MULTILINE)
+
+# the docs write an inlay hint — what an editor renders, not what the file
+# contains — between these. the `by` lexer knows them; no other lexer does
+HINT_DELIMITERS = {"⟨", "⟩"}
+
+# each entry is a snippet and the word in it that must lex as a keyword. keep
+# the snippets minimal — they document the position that makes the word a
+# keyword, which is exactly what the lexer's lookaheads encode
+KEYWORDS = [
+    ("let x = 1", "let"),
+    ("def f(var name: str): ...", "var"),
+    ("a: typeof b", "typeof"),
+    ("b = a cast int", "cast"),
+    ("b = a cast? int", "cast?"),
+    ("sentinel MISSING", "sentinel"),
+    ("extension list[int]:", "extension"),
+    ("implementation Show for Point:", "implementation"),
+    ("def f(x: protocol(a: int)): ...", "protocol"),
+    ("class C[reified T]: ...", "reified"),
+    ("def check(x: int | None) -> asserts x: ...", "asserts"),
+    ("def parse(t: str) -> int raises ValueError: ...", "raises"),
+    ("def f(local xs: list[int]): ...", "local"),
+    ("def f(once cb: () -> None): ...", "once"),
+    ("from x export y", "export"),
+    ("data class Point:", "data"),
+    ("enum class Shape:", "enum"),
+    ("sealed class Shape:", "sealed"),
+    ("frozen data class D:", "frozen"),
+    ("abstract class A:", "abstract"),
+    ("open class A:", "open"),
+    ("final def f(): ...", "final"),
+    ("override def f(): ...", "override"),
+    ("static let x: int", "static"),
+    ("private type X = int", "private"),
+    ("public let x = 1", "public"),
+    ("late var x: int", "late"),
+    ("class Mapping[out Key]: ...", "out"),
+    ("def f(x: literal int): ...", "literal"),
+    ("class C[T: constraints (int, str)]: ...", "constraints"),
+    ("a: dynamic = 1", "dynamic"),
+    ("    get() = 1", "get"),
+    ("    set(value):", "set"),
+    ("    field = value", "field"),
+]
+
+# words the lexer must leave alone, because they are ordinary names here. these
+# are the cost of the soft-keyword lookaheads being wrong in the other
+# direction, which is just as visible in the rendered page
+NON_KEYWORDS = [
+    ("os.environ.get(key)", "get"),
+    ("def get(self) -> int: ...", "get"),
+    ("def read(data: bytes): ...", "data"),
+    ("import enum", "enum"),
+    ("literal: object | None", "literal"),
+    ("x = open(path)", "open"),
+    ("cast(int, x)", "cast"),
+]
+
+
+def blocks() -> list[tuple[Path, str, str]]:
+    """every fenced block in the docs, as (path, language, source)"""
+    found = []
+    for path in sorted(DOCS.rglob("*.md")):
+        found += [
+            (path, m.group(2), m.group(3)) for m in FENCE.finditer(path.read_text())
+        ]
+    return found
+
+
+def main() -> int:
+    by_lexer = get_lexer_by_name("by")
+    problems: list[str] = []
+    by_blocks = 0
+
+    for path, language, source in blocks():
+        if not language:
+            continue
+        try:
+            lexer = get_lexer_by_name(language)
+        except ClassNotFound:
+            # a fence tagged with something pygments has no lexer for renders
+            # as plain text, which is a deliberate choice, not a lexer bug
+            continue
+        by_blocks += language == "by"
+        # a `by` block must lex cleanly; anything else may only fail on the
+        # inlay-hint notation, which the stylesheet renders as a hint
+        allowed: set[str] = set() if language == "by" else HINT_DELIMITERS
+        errors = {
+            value
+            for token, value in lexer.get_tokens(source)
+            if token is Error and value not in allowed
+        }
+        if errors:
+            relative = path.relative_to(ROOT)
+            problems.append(
+                f"{relative}: `{language}` block lexes to error token(s): "
+                f"{sorted(errors)}"
+            )
+
+    for snippet, word in KEYWORDS:
+        tokens = [
+            (token, value)
+            for token, value in by_lexer.get_tokens(snippet)
+            if value.strip()
+        ]
+        if not any(value == word and token in Keyword for token, value in tokens):
+            actual = next(
+                (str(token) for token, value in tokens if value == word),
+                "not tokenized as one word",
+            )
+            problems.append(
+                f"`{snippet}`: expected `{word}` to be a keyword, got {actual}"
+            )
+
+    for snippet, word in NON_KEYWORDS:
+        tokens = [
+            (token, value)
+            for token, value in by_lexer.get_tokens(snippet)
+            if value.strip()
+        ]
+        if any(value == word and token in Keyword for token, value in tokens):
+            problems.append(
+                f"`{snippet}`: expected `{word}` to be an ordinary name, got a keyword"
+            )
+
+    if problems:
+        print("\n".join(problems), file=sys.stderr)
+        print(
+            f"\n{len(problems)} problem(s) — see {Path(__file__).name}",
+            file=sys.stderr,
+        )
+        return 1
+
+    print(
+        f"{by_blocks} `by` blocks lex cleanly; "
+        f"{len(KEYWORDS)} keywords and {len(NON_KEYWORDS)} names classified"
+    )
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())
diff --git a/scripts/check_docs_nav.py b/scripts/check_docs_nav.py
index d40627cbd7..39ea91ce26 100644
--- a/scripts/check_docs_nav.py
+++ b/scripts/check_docs_nav.py
@@ -20,7 +20,11 @@
 FEATURES = Path("docs/basedpython/features")
 
 # reachable through in-page links rather than the nav, deliberately
-NAV_EXEMPT = {"acknowledgements.md", "frameworks/index.md"}
+NAV_EXEMPT: set[str] = set()
+
+# a link in `index.md` that leaves the features directory is prose, not an entry
+# in the reference index, so it takes no part in the three-way comparison
+SIBLING_LINK = re.compile(r"^[\w.-]+\.md$")
 
 
 def nav_paths(nav: object) -> list[str]:
@@ -56,9 +60,13 @@ def main() -> int:
         p.name for p in (ROOT / FEATURES).glob("*.md") if p.name != "index.md"
     )
 
-    index_order = re.findall(
-        r"\]\(([^)\s]+\.md)\)", (ROOT / FEATURES / "index.md").read_text()
-    )
+    index_order = [
+        link
+        for link in re.findall(
+            r"\]\(([^)\s]+\.md)\)", (ROOT / FEATURES / "index.md").read_text()
+        )
+        if SIBLING_LINK.match(link)
+    ]
     indexed = set(index_order)
 
     all_nav = nav_paths(nav)
diff --git a/scripts/pyproject.toml b/scripts/pyproject.toml
index 2a64bb8c16..13dc4e6239 100644
--- a/scripts/pyproject.toml
+++ b/scripts/pyproject.toml
@@ -1,7 +1,18 @@
 [project]
 name = "scripts"
 version = "0.0.1"
-dependencies = ["stdlibs", "tqdm", "mdformat", "pyyaml", "mypy-primer", "httpx"]
+dependencies = [
+    "stdlibs",
+    "tqdm",
+    "mdformat",
+    "pyyaml",
+    "mypy-primer",
+    "httpx",
+    # `check_by_lexer.py` exercises the lexer in `python/basedpython-pygments`.
+    # only `pygments` is imported — the lexer itself is resolved through its
+    # entry point at runtime, so it is not a dependency of this project
+    "pygments",
+]
 requires-python = ">=3.12"
 
 [tool.black]
diff --git a/scripts/uv.lock b/scripts/uv.lock
index 09ab1d58fd..347c8b63cd 100644
--- a/scripts/uv.lock
+++ b/scripts/uv.lock
@@ -117,6 +117,15 @@ name = "mypy-primer"
 version = "0.1.0"
 source = { git = "https://github.com/hauntsaninja/mypy_primer#23bbdd55fea37ca2489043d1327dbe35c4fc7083" }
 
+[[package]]
+name = "pygments"
+version = "2.20.0"
+source = { registry = "https://pypi.org/simple" }
+sdist = { url = "https://files.pythonhosted.org/packages/c3/b2/bc9c9196916376152d655522fdcebac55e66de6603a76a02bca1b6414f6c/pygments-2.20.0.tar.gz", hash = "sha256:6757cd03768053ff99f3039c1a36d6c0aa0b263438fcab17520b30a303a82b5f", size = 4955991, upload-time = "2026-03-29T13:29:33.898Z" }
+wheels = [
+    { url = "https://files.pythonhosted.org/packages/f4/7e/a72dd26f3b0f4f2bf1dd8923c85f7ceb43172af56d63c7383eb62b332364/pygments-2.20.0-py3-none-any.whl", hash = "sha256:81a9e26dd42fd28a23a2d169d86d7ac03b46e2f8b59ed4698fb4785f946d0176", size = 1231151, upload-time = "2026-03-29T13:29:30.038Z" },
+]
+
 [[package]]
 name = "pyyaml"
 version = "6.0.3"
@@ -171,6 +180,7 @@ dependencies = [
     { name = "httpx" },
     { name = "mdformat" },
     { name = "mypy-primer" },
+    { name = "pygments" },
     { name = "pyyaml" },
     { name = "stdlibs" },
     { name = "tqdm" },
@@ -181,6 +191,7 @@ requires-dist = [
     { name = "httpx" },
     { name = "mdformat" },
     { name = "mypy-primer", git = "https://github.com/hauntsaninja/mypy_primer" },
+    { name = "pygments" },
     { name = "pyyaml" },
     { name = "stdlibs" },
     { name = "tqdm" },
diff --git a/uv.lock b/uv.lock
index 6dc657430f..35e85479fd 100644
--- a/uv.lock
+++ b/uv.lock
@@ -61,8 +61,8 @@ dev = [
     { name = "prek", marker = "python_full_version >= '3.12'" },
 ]
 docs = [
-    { name = "zensical", version = "0.0.2", source = { registry = "https://pypi.org/simple" }, marker = "python_full_version < '3.10'" },
-    { name = "zensical", version = "0.0.51", source = { registry = "https://pypi.org/simple" }, marker = "python_full_version >= '3.10'" },
+    { name = "basedpython-pygments", marker = "python_full_version >= '3.12'" },
+    { name = "zensical", marker = "python_full_version >= '3.12'" },
 ]
 release = [
     { name = "rooster", marker = "python_full_version >= '3.12'" },
@@ -72,9 +72,23 @@ release = [
 
 [package.metadata.requires-dev]
 dev = [{ name = "prek", marker = "python_full_version >= '3.12'", specifier = "==0.4.9" }]
-docs = [{ name = "zensical" }]
+docs = [
+    { name = "basedpython-pygments", marker = "python_full_version >= '3.12'", directory = "python/basedpython-pygments" },
+    { name = "zensical", marker = "python_full_version >= '3.12'" },
+]
 release = [{ name = "rooster", marker = "python_full_version >= '3.12'", specifier = "==0.1.1" }]
 
+[[package]]
+name = "basedpython-pygments"
+version = "0.0.0"
+source = { directory = "python/basedpython-pygments" }
+dependencies = [
+    { name = "pygments" },
+]
+
+[package.metadata]
+requires-dist = [{ name = "pygments", specifier = ">=2.19" }]
+
 [[package]]
 name = "certifi"
 version = "2026.6.17"
@@ -988,27 +1002,10 @@ wheels = [
     { url = "https://files.pythonhosted.org/packages/dc/9b/47798a6c91d8bdb567fe2698fe81e0c6b7cb7ef4d13da4114b41d239f65d/typing_inspection-0.4.2-py3-none-any.whl", hash = "sha256:4ed1cacbdc298c220f1bd249ed5287caa16f34d44ef4e9c3d0cbad5b521545e7", size = 14611, upload-time = "2025-10-01T02:14:40.154Z" },
 ]
 
-[[package]]
-name = "zensical"
-version = "0.0.2"
-source = { registry = "https://pypi.org/simple" }
-resolution-markers = [
-    "python_full_version >= '3.8' and python_full_version < '3.10'",
-    "python_full_version < '3.8'",
-]
-sdist = { url = "https://files.pythonhosted.org/packages/f9/95/402f98707f23f6f55f64c89d6b3f33429fa7905df0a448a48498d5669b32/zensical-0.0.2.tar.gz", hash = "sha256:0b74994de625bdc1526748db47aa5104ee3f9127314dd5d930984b64d8278e7a", size = 487, upload-time = "2025-05-17T08:41:41.767Z" }
-wheels = [
-    { url = "https://files.pythonhosted.org/packages/0e/2c/07c07e99d3566a75a937a6fdee290046c0eee756b56f080fac6e897807fd/zensical-0.0.2-py2.py3-none-any.whl", hash = "sha256:a0d8185441eceff831fba020759842066b99c16faa91259462f7e77b80d10bf2", size = 1029, upload-time = "2025-05-17T08:41:43.143Z" },
-]
-
 [[package]]
 name = "zensical"
 version = "0.0.51"
 source = { registry = "https://pypi.org/simple" }
-resolution-markers = [
-    "python_full_version >= '3.12'",
-    "python_full_version >= '3.10' and python_full_version < '3.12'",
-]
 dependencies = [
     { name = "click" },
     { name = "deepmerge" },
diff --git a/zensical.toml b/zensical.toml
index 8db9217379..4654ccdb9b 100644
--- a/zensical.toml
+++ b/zensical.toml
@@ -1,20 +1,67 @@
 [project]
 site_name = "basedpython"
+site_description = "a python-like language that transpiles to pure python"
+site_author = "KotlinIsland"
 site_url = "https://kotlinisland.github.io/basedpython/"
 docs_dir = "docs/basedpython"
+repo_url = "https://github.com/KotlinIsland/basedpython"
+repo_name = "KotlinIsland/basedpython"
+edit_uri = "edit/main/docs/basedpython"
+
+extra_css = ["stylesheets/extra.css"]
+
+[project.theme]
+features = [
+  # a click swaps the page in place instead of reloading the whole document,
+  # and a hovered link is fetched before the click lands
+  "navigation.instant",
+  "navigation.instant.prefetch",
+  "navigation.instant.progress",
+  "navigation.tracking",
+  # the reference is deep, so say where you are and how to leave
+  "navigation.path",
+  "navigation.indexes",
+  "navigation.footer",
+  "navigation.top",
+  "toc.follow",
+  # every page is mostly code, so make it easy to take
+  "content.code.copy",
+  "content.code.annotate",
+  "content.tabs.link",
+  "content.action.edit",
+  "search.highlight",
+]
+
+[project.theme.icon]
+logo = "lucide/binary"
+repo = "fontawesome/brands/github"
 
 [[project.theme.palette]]
 media = "(prefers-color-scheme: light)"
 scheme = "default"
+primary = "black"
+accent = "indigo"
 toggle.icon = "lucide/sun"
 toggle.name = "Switch to dark mode"
 
 [[project.theme.palette]]
 media = "(prefers-color-scheme: dark)"
 scheme = "slate"
+primary = "black"
+accent = "indigo"
 toggle.icon = "lucide/moon"
 toggle.name = "Switch to light mode"
 
+[[project.extra.social]]
+icon = "fontawesome/brands/github"
+link = "https://github.com/KotlinIsland/basedpython"
+name = "basedpython on GitHub"
+
+[[project.extra.social]]
+icon = "fontawesome/brands/python"
+link = "https://pypi.org/project/basedpython/"
+name = "basedpython on PyPI"
+
 [[project.nav]]
 basedpython = "index.md"
 
@@ -29,99 +76,122 @@ configuration = "configuration.md"
 
 [[project.nav]]
 features = [
-  { features = "features/index.md" },
-  { "polyfills" = "features/polyfills.md" },
-  { "runtime type-soundness checks" = "features/soundness.md" },
-  { "api lockfile" = "features/api-lock.md" },
-  { "fluid specializations" = "features/fluid-specializations.md" },
-  { "sound types" = "features/sound-types.md" },
-  { "precise unsolved type variables" = "features/precise-unsolved-typevars.md" },
-  { "regex group types" = "features/regex-groups.md" },
-  { "boolean conditions" = "features/conditions.md" },
-  { "tuple type literals" = "features/tuple-types.md" },
-  { "callable arrow syntax" = "features/callable.md" },
-  { "implicit receivers" = "features/implicit-receivers.md" },
-  { "intersection types" = "features/intersection.md" },
-  { "`or` / `and` type operators" = "features/or-and-types.md" },
-  { "negation types" = "features/not-type.md" },
-  { "unsafe unions" = "features/unsafe-union.md" },
-  { "`dynamic` type" = "features/dynamic.md" },
-  { "`typeof` keyword" = "features/typeof.md" },
-  { "star projections" = "features/star-projection.md" },
-  { "strict `float` and `complex`" = "features/no-number-promotions.md" },
-  { "infinity and nan float literals" = "features/float-literals.md" },
-  { "literal type promotion" = "features/literal-types.md" },
-  { "use-site type modifiers" = "features/type-modifiers.md" },
-  { "symbolic operations in types" = "features/symbolic-type-ops.md" },
-  { "match types" = "features/match-types.md" },
-  { "`type def` type functions" = "features/type-def.md" },
-  { "typed dict literals" = "features/typed-dict-literal.md" },
-  { "anonymous named tuple types" = "features/anonymous-named-tuple.md" },
-  { "inline protocol types" = "features/inline-protocol.md" },
-  { "wrapped optional and result types" = "features/wrapped-results.md" },
-  { "automatic forward references" = "features/forward-references.md" },
-  { "implicit typing imports" = "features/implicit-typing.md" },
-  { "typed lambda" = "features/typed-lambda.md" },
-  { "implicit overload stubs" = "features/overloads.md" },
-  { "type narrowing predicates" = "features/type-is.md" },
-  { "generics" = "features/generics.md" },
-  { "explicit typevar constraints" = "features/constraints.md" },
-  { "type parameter bound ranges" = "features/bound-ranges.md" },
-  { "bounds on a variadic pack" = "features/pack-bounds.md" },
-  { "attribute types" = "features/attribute-types.md" },
-  { "`TypedDict` and `Self` in type parameters" = "features/typeddict-self-bounds.md" },
-  { "keyword-variadic packs" = "features/keyword-variadic.md" },
-  { "type parameter separators" = "features/type-param-separators.md" },
-  { "typevar variance keywords" = "features/variance.md" },
-  { "safe variance" = "features/safe-variance.md" },
-  { "overlapping" = "features/overlapping.md" },
-  { "explicit generic call sites" = "features/generic-calls.md" },
-  { "reified type parameters" = "features/reified-generics.md" },
-  { "type reification" = "features/type-reification.md" },
-  { "parametric type tests" = "features/parametric-type-tests.md" },
-  { "modifiers and visibility" = "features/modifiers.md" },
-  { "based enums" = "features/enums.md" },
-  { "sealed classes" = "features/sealed-classes.md" },
-  { "init method shorthand" = "features/init-method.md" },
-  { "properties" = "features/properties.md" },
-  { "empty declarations" = "features/empty-declarations.md" },
-  { "main function" = "features/main-function.md" },
-  { "`sentinel` declarations" = "features/sentinel.md" },
-  { "decorator keyword" = "features/decorator-keyword.md" },
-  { "context-sensitive resolution" = "features/context-sensitive-resolution.md" },
-  { "identity and isinstance" = "features/identity-swap.md" },
-  { "optional chaining (`?.`)" = "features/optional-chaining.md" },
-  { "none-coalesce operator (`??`)" = "features/none-coalesce.md" },
-  { "postfix await (`.await`)" = "features/await-attribute.md" },
-  { "`cast` keyword" = "features/cast.md" },
-  { "checked & safe casts (`cast` / `cast?`)" = "features/checked-cast.md" },
-  { "`super` keyword" = "features/super.md" },
-  { "tuple member access" = "features/tuple-index.md" },
-  { "keyword arguments in subscripts" = "features/kw-subscript.md" },
-  { "destructuring" = "features/destructuring.md" },
-  { "destructuring with `if let`" = "features/if-let.md" },
-  { "statement expressions" = "features/statement-expressions.md" },
-  { "trailing lambda blocks" = "features/trailing-lambdas.md" },
-  { "unpack syntax" = "features/unpack-syntax.md" },
-  { "mutable default arguments" = "features/mutable-defaults.md" },
-  { "unique loop bindings" = "features/unique-loop-bindings.md" },
-  { "dedented triple-quoted strings" = "features/dedent-strings.md" },
-  { "custom string tags" = "features/string-tags.md" },
-  { "strings and characters" = "features/character.md" },
-  { "repeated `_` parameters" = "features/repeated-underscore.md" },
-  { "lazy imports" = "features/lazy-imports.md" },
-  { "export imports" = "features/export-imports.md" },
-  { "extensions" = "features/extensions.md" },
-  { "conversions (`__from__` / `__into__` / `__of__`)" = "features/conversions.md" },
-  { "context parameters" = "features/context-parameters.md" },
-  { "local lifetimes (`local` / `once`)" = "features/local-lifetimes.md" },
-  { "exception tracking (`raises`)" = "features/exceptions.md" },
-  { "assignment alignment" = "features/assignment-alignment.md" },
-  { "implementations" = "features/implementations.md" },
+  "features/index.md",
+  { "python compatibility" = [
+    { "differences from python" = "features/differences-from-python.md" },
+  ] },
+  { "runtime compatibility" = [
+    { "polyfills" = "features/polyfills.md" },
+    { "runtime type-soundness checks" = "features/soundness.md" },
+  ] },
+  { "project-level" = [
+    { "api lockfile" = "features/api-lock.md" },
+  ] },
+  { "standard library" = [
+    { "typeshed improvements" = "features/typeshed.md" },
+  ] },
+  { "enhancements that also apply to python" = [
+    { "fluid specializations" = "features/fluid-specializations.md" },
+    { "sound types" = "features/sound-types.md" },
+    { "precise unsolved type variables" = "features/precise-unsolved-typevars.md" },
+    { "regex group types" = "features/regex-groups.md" },
+    { "boolean conditions" = "features/conditions.md" },
+  ] },
+  { "type system" = [
+    { "tuple type literals" = "features/tuple-types.md" },
+    { "callable arrow syntax" = "features/callable.md" },
+    { "implicit receivers" = "features/implicit-receivers.md" },
+    { "intersection types" = "features/intersection.md" },
+    { "or / and type operators" = "features/or-and-types.md" },
+    { "negation types" = "features/not-type.md" },
+    { "unsafe unions" = "features/unsafe-union.md" },
+    { "dynamic type" = "features/dynamic.md" },
+    { "typeof keyword" = "features/typeof.md" },
+    { "star projections" = "features/star-projection.md" },
+    { "strict float and complex" = "features/no-number-promotions.md" },
+    { "infinity and nan float literals" = "features/float-literals.md" },
+    { "literal type promotion" = "features/literal-types.md" },
+    { "use-site type modifiers" = "features/type-modifiers.md" },
+    { "symbolic operations in types" = "features/symbolic-type-ops.md" },
+    { "match types" = "features/match-types.md" },
+    { "type def type functions" = "features/type-def.md" },
+    { "typed dict literals" = "features/typed-dict-literal.md" },
+    { "anonymous named tuple types" = "features/anonymous-named-tuple.md" },
+    { "inline protocol types" = "features/inline-protocol.md" },
+    { "wrapped optional and result types" = "features/wrapped-results.md" },
+    { "automatic forward references" = "features/forward-references.md" },
+    { "implicit typing imports" = "features/implicit-typing.md" },
+    { "typed lambda" = "features/typed-lambda.md" },
+    { "implicit overload stubs" = "features/overloads.md" },
+    { "type narrowing predicates" = "features/type-is.md" },
+  ] },
+  { "generics" = [
+    { "generics" = "features/generics.md" },
+    { "explicit typevar constraints" = "features/constraints.md" },
+    { "type parameter bound ranges" = "features/bound-ranges.md" },
+    { "bounds on a variadic pack" = "features/pack-bounds.md" },
+    { "attribute types" = "features/attribute-types.md" },
+    { "TypedDict and Self in type parameters" = "features/typeddict-self-bounds.md" },
+    { "keyword-variadic packs" = "features/keyword-variadic.md" },
+    { "type parameter separators" = "features/type-param-separators.md" },
+    { "typevar variance keywords" = "features/variance.md" },
+    { "safe variance" = "features/safe-variance.md" },
+    { "overlapping" = "features/overlapping.md" },
+    { "explicit generic call sites" = "features/generic-calls.md" },
+    { "reified type parameters" = "features/reified-generics.md" },
+    { "type reification" = "features/type-reification.md" },
+    { "parametric type tests" = "features/parametric-type-tests.md" },
+  ] },
+  { "declarations" = [
+    { "modifiers and visibility" = "features/modifiers.md" },
+    { "based enums" = "features/enums.md" },
+    { "sealed classes" = "features/sealed-classes.md" },
+    { "init method shorthand" = "features/init-method.md" },
+    { "properties" = "features/properties.md" },
+    { "empty declarations" = "features/empty-declarations.md" },
+    { "main function" = "features/main-function.md" },
+    { "sentinel declarations" = "features/sentinel.md" },
+    { "decorator keyword" = "features/decorator-keyword.md" },
+  ] },
+  { "expressions and statements" = [
+    { "context-sensitive resolution" = "features/context-sensitive-resolution.md" },
+    { "identity and isinstance" = "features/identity-swap.md" },
+    { "optional chaining (?.)" = "features/optional-chaining.md" },
+    { "none-coalesce operator (??)" = "features/none-coalesce.md" },
+    { "postfix await (.await)" = "features/await-attribute.md" },
+    { "cast keyword" = "features/cast.md" },
+    { "checked & safe casts (cast / cast?)" = "features/checked-cast.md" },
+    { "super keyword" = "features/super.md" },
+    { "tuple member access" = "features/tuple-index.md" },
+    { "keyword arguments in subscripts" = "features/kw-subscript.md" },
+    { "destructuring" = "features/destructuring.md" },
+    { "destructuring with if let" = "features/if-let.md" },
+    { "statement expressions" = "features/statement-expressions.md" },
+    { "trailing lambda blocks" = "features/trailing-lambdas.md" },
+    { "unpack syntax" = "features/unpack-syntax.md" },
+    { "mutable default arguments" = "features/mutable-defaults.md" },
+    { "unique loop bindings" = "features/unique-loop-bindings.md" },
+    { "dedented triple-quoted strings" = "features/dedent-strings.md" },
+    { "custom string tags" = "features/string-tags.md" },
+    { "strings and characters" = "features/character.md" },
+    { "repeated _ parameters" = "features/repeated-underscore.md" },
+    { "lazy imports" = "features/lazy-imports.md" },
+    { "export imports" = "features/export-imports.md" },
+    { "extensions" = "features/extensions.md" },
+    { "implementations" = "features/implementations.md" },
+    { "conversions (__from__ / __into__ / __of__)" = "features/conversions.md" },
+    { "context parameters" = "features/context-parameters.md" },
+    { "local lifetimes (local / once)" = "features/local-lifetimes.md" },
+    { "exception tracking (raises)" = "features/exceptions.md" },
+  ] },
+  { "formatting" = [
+    { "assignment alignment" = "features/assignment-alignment.md" },
+  ] },
 ]
 
 [[project.nav]]
 "framework support" = [
+  "frameworks/index.md",
   { "Pydantic" = "frameworks/pydantic.md" },
   { "SQLAlchemy" = "frameworks/sqlalchemy.md" },
   { "pytest" = "frameworks/pytest.md" },
@@ -136,3 +206,6 @@ development = [
   { "type functions" = "development/type-def-design.md" },
   { "typeshed patches" = "development/typeshed-patches.md" },
 ]
+
+[[project.nav]]
+credits = "credits.md"