diff --git a/fnotation.cabal b/fnotation.cabal
--- a/fnotation.cabal
+++ b/fnotation.cabal
@@ -1,71 +1,111 @@
-cabal-version:   3.4
-name:            fnotation
-version:         0.1.1.0
-license:         MPL-2.0
-license-file:    LICENSE
-maintainer:      root@owenlynch.org
-author:          Owen Lynch
+cabal-version: 3.4
+name: fnotation
+version: 0.2.0.0
+license: MPL-2.0
+license-file: LICENSE
+maintainer: root@owenlynch.org
+author: Owen Lynch
 description:
-    A lower house syntax for programming language experimentation.
+  A lower house syntax for programming language experimentation.
 
-category:        Language
-build-type:      Simple
+category: Language
+build-type: Simple
 extra-doc-files: CHANGELOG.md
 
 library
-    exposed-modules:
-        FNotation
-        FNotation.Config
-        FNotation.Lexer
-        FNotation.Names
-        FNotation.Parser
-        FNotation.Pretty
-        FNotation.Tokens
-        FNotation.Trees
+  exposed-modules:
+    FNotation
+    FNotation.Config
+    FNotation.Kinds
+    FNotation.Lexer
+    FNotation.Names
+    FNotation.Parser
+    FNotation.Pretty
+    FNotation.Tokens
+    FNotation.Trees
 
-    hs-source-dirs:     src
-    default-language:   GHC2024
-    default-extensions:
-        BlockArguments CPP TypeData DerivingVia FunctionalDependencies
-        ImplicitParams MagicHash NoFieldSelectors OrPatterns
-        OverloadedRecordDot OverloadedStrings PatternSynonyms QualifiedDo
-        StrictData TypeFamilies TypeFamilyDependencies UnboxedSums
-        UnboxedTuples UnicodeSyntax ViewPatterns
+  hs-source-dirs: src
+  default-language: GHC2024
+  default-extensions:
+    BlockArguments
+    CPP
+    DerivingVia
+    FunctionalDependencies
+    ImplicitParams
+    MagicHash
+    NoFieldSelectors
+    OrPatterns
+    OverloadedRecordDot
+    OverloadedStrings
+    PatternSynonyms
+    QualifiedDo
+    StrictData
+    TypeData
+    TypeFamilies
+    TypeFamilyDependencies
+    UnboxedSums
+    UnboxedTuples
+    UnicodeSyntax
+    ViewPatterns
 
-    ghc-options:        -Wall
-    build-depends:
-        base ^>=4.21.0.0,
-        containers,
-        diagnostician,
-        hashable,
-        prettyprinter,
-        text,
-        vector,
-        vector-hashtables >=0.1.2.1
+  ghc-options: -Wall
+  build-depends:
+    base ^>=4.21.0.0,
+    containers,
+    diagnostician,
+    hashable,
+    prettyprinter,
+    text,
+    vector,
+    vector-hashtables >=0.1.2.1,
 
 test-suite fnotation-test
-    type:               exitcode-stdio-1.0
-    main-is:            Main.hs
-    hs-source-dirs:     test
-    default-language:   GHC2024
-    default-extensions:
-        BlockArguments CPP TypeData DerivingVia FunctionalDependencies
-        MagicHash NoFieldSelectors OrPatterns OverloadedRecordDot
-        OverloadedStrings PatternSynonyms QualifiedDo StrictData
-        TypeFamilies TypeFamilyDependencies UnboxedSums UnboxedTuples
-        UnicodeSyntax ViewPatterns
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  hs-source-dirs: test
+  other-modules:
+    Test.FNotation.Common
+    Test.FNotation.Golden
+    Test.FNotation.Property.Gen.Source
+    Test.FNotation.Property.Gen.Token
+    Test.FNotation.Property.Lexing
+    Test.FNotation.Property.Parsing
 
-    ghc-options:        -Wall -Wno-unused-imports
-    build-depends:
-        base ^>=4.21.0.0,
-        bytestring,
-        containers,
-        diagnostician,
-        filepath,
-        fnotation,
-        prettyprinter,
-        tasty,
-        tasty-golden,
-        temporary,
-        text,
-        vector
+  default-language: GHC2024
+  default-extensions:
+    BlockArguments
+    CPP
+    DerivingVia
+    FunctionalDependencies
+    MagicHash
+    NoFieldSelectors
+    OrPatterns
+    OverloadedRecordDot
+    OverloadedStrings
+    PatternSynonyms
+    QualifiedDo
+    StrictData
+    TypeData
+    TypeFamilies
+    TypeFamilyDependencies
+    UnboxedSums
+    UnboxedTuples
+    UnicodeSyntax
+    ViewPatterns
+
+  ghc-options: -Wall
+  build-depends:
+    QuickCheck,
+    base ^>=4.21.0.0,
+    bytestring,
+    containers,
+    diagnostician,
+    filepath,
+    fnotation,
+    prettyprinter,
+    tasty,
+    tasty-golden,
+    tasty-quickcheck,
+    temporary,
+    text,
+    vector,
diff --git a/src/FNotation.hs b/src/FNotation.hs
--- a/src/FNotation.hs
+++ b/src/FNotation.hs
@@ -1,18 +1,18 @@
-module FNotation
-  ( module FNotation.Config,
-    module FNotation.Lexer,
-    module FNotation.Names,
-    module FNotation.Parser,
-    module FNotation.Pretty,
-    module FNotation.Tokens,
-    module FNotation.Trees,
-  )
+module FNotation (
+  module FNotation.Config,
+  module FNotation.Lexer,
+  module FNotation.Names,
+  module FNotation.Parser,
+  module FNotation.Pretty,
+  module FNotation.Kinds,
+  module FNotation.Trees,
+)
 where
 
 import FNotation.Config
+import FNotation.Kinds (Kind)
 import FNotation.Lexer (LexerCode (..), lex, lexerCodeTable)
 import FNotation.Names
 import FNotation.Parser (ParserCode (..), parse, parserCodeTable)
-import FNotation.Pretty (dprettyWithPrecs)
-import FNotation.Tokens (Kind)
-import FNotation.Trees (Ntn, Ntn0, NtnGeneric (..), head, span)
+import FNotation.Pretty (dprettyWithConfigs)
+import FNotation.Trees (Ntn, Ntn0, NtnGeneric (..), head, span, pattern Decl, pattern Group)
diff --git a/src/FNotation/Config.hs b/src/FNotation/Config.hs
--- a/src/FNotation/Config.hs
+++ b/src/FNotation/Config.hs
@@ -23,8 +23,8 @@
   deriving (Eq, Show)
 
 data Prec = Prec
-  { binding :: Int,
-    assoc :: Assoc
+  { binding :: Int
+  , assoc :: Assoc
   }
   deriving (Eq, Show)
 
diff --git a/src/FNotation/Kinds.hs b/src/FNotation/Kinds.hs
new file mode 100644
--- /dev/null
+++ b/src/FNotation/Kinds.hs
@@ -0,0 +1,37 @@
+module FNotation.Kinds where
+
+import Diagnostician (DPretty (..))
+import Prettyprinter
+
+data Kind
+  = -- | alphanumerical identifier
+    AIdent
+  | -- | alphanumerical keyword
+    AKeyword
+  | -- | symbolic identifier
+    SIdent
+  | -- | symbolic keyword
+    SKeyword
+  | Decl
+  | Modifier
+  | Block
+  | End
+  | Tag
+  | Field
+  | Int
+  | String
+  | LParen
+  | RParen
+  | LBrack
+  | RBrack
+  | LCurly
+  | RCurly
+  | Comma
+  | Semicolon
+  | Nl
+  | Eof
+  | Error
+  deriving (Eq, Show)
+
+instance DPretty Kind where
+  dpretty k = pretty (show k)
diff --git a/src/FNotation/Lexer.hs b/src/FNotation/Lexer.hs
--- a/src/FNotation/Lexer.hs
+++ b/src/FNotation/Lexer.hs
@@ -1,6 +1,6 @@
 module FNotation.Lexer where
 
-import Data.Char (isDigit, isLetter, ord)
+import Data.Char (isDigit, isLetter, isPrint, ord)
 import Data.IORef
 import Data.Map (Map)
 import Data.Map qualified as Map
@@ -11,6 +11,7 @@
 import Data.Vector.Mutable qualified as VM
 import Diagnostician
 import FNotation.Config
+import FNotation.Kinds
 import FNotation.Names
 import FNotation.Tokens
 import Prettyprinter
@@ -21,9 +22,9 @@
 --------------------------------------------------------------------------------
 
 data Buffer a = Buffer
-  { next :: IORef Int,
-    size :: Int,
-    values :: VM.IOVector a
+  { next :: IORef Int
+  , size :: Int
+  , values :: VM.IOVector a
   }
 
 bufferWithCapacity :: Int -> IO (Buffer a)
@@ -52,26 +53,36 @@
 data LexerCode
   = UnexpectedCharacter
   | UncontinuedQualifiedName
+  | ExpectedName
+  | InvalidNamespace
+  | KeywordInNamespace
+  | InvalidKeyword
+  | EmptyNameComponent
   deriving (Eq, Ord)
 
 lexerCodeTable :: Map LexerCode CodeMeta
 lexerCodeTable =
   Map.fromList
-    [ (UnexpectedCharacter, CodeMeta 0 SError Nothing),
-      (UncontinuedQualifiedName, CodeMeta 1 SError Nothing)
+    [ (UnexpectedCharacter, CodeMeta 0 SError Nothing)
+    , (UncontinuedQualifiedName, CodeMeta 1 SError Nothing)
+    , (ExpectedName, CodeMeta 2 SError Nothing)
+    , (InvalidNamespace, CodeMeta 3 SError Nothing)
+    , (KeywordInNamespace, CodeMeta 4 SError Nothing)
+    , (InvalidKeyword, CodeMeta 5 SError Nothing)
+    , (EmptyNameComponent, CodeMeta 6 SError Nothing)
     ]
 
 -- Lex monad
 --------------------------------------------------------------------------------
 
 data LexState = LexState
-  { pos :: IORef Int,
-    prev :: IORef Int,
-    iter :: IORef TU.Iter,
-    out :: Buffer Token,
-    file :: File,
-    reporter :: Reporter LexerCode,
-    config :: ConfTable Kind
+  { pos :: IORef Int
+  , prev :: IORef Int
+  , iter :: IORef TU.Iter
+  , out :: Buffer Token
+  , file :: File
+  , reporter :: Reporter LexerCode
+  , config :: ConfTable Kind
   }
 
 -- Fundamental lexing actions
@@ -158,6 +169,10 @@
   advance st
   report st UnexpectedCharacter $ "Unexpected character" <+> "'" <> pretty c <> "'"
 
+emptyNameComponent :: LexState -> IO ()
+emptyNameComponent st = do
+  report st EmptyNameComponent $ "Empty name component"
+
 -- Lexemes
 --------------------------------------------------------------------------------
 
@@ -168,11 +183,11 @@
   e <- readIORef st.pos
   slice st (Span s e)
 
-classifyName :: LexState -> Name -> Kind
-classifyName st x = case confTableLookup st.config x.last of
+classifyNameSeg :: LexState -> Text -> Kind
+classifyNameSeg st x = case confTableLookup st.config x of
   Just kind -> kind
   Nothing ->
-    if isAlphaNumStart (T.head x.last)
+    if isAlphaNumStart (T.head x)
       then AIdent
       else SIdent
 
@@ -182,42 +197,80 @@
   | c == '_' = True
   | otherwise = False
 
-nameSeg :: LexState -> IO Text
+nameSeg :: LexState -> IO (Kind, Text)
 nameSeg st =
   peek st >>= \case
-    c | isAlphaNumStart c -> sliceWhile st isAlphaNum
-    c | isSymbol c -> sliceWhile st isSymbol
-    _ -> P.error "nameSeg should only be called if current character is a letter"
+    c | isAlphaNumStart c -> do
+      t <- sliceWhile st isAlphaNum
+      let k = classifyNameSeg st t
+      pure (k, t)
+    c | isSymbol c -> do
+      t <- sliceWhile st isSymbol
+      let k = classifyNameSeg st t
+      pure (k, t)
+    c | c == '`' -> do
+      advance st
+      t <- sliceWhile st (\c' -> c' /= '`' && isPrint c')
+      c' <- peek st
+      if c' == '`'
+        then advance st
+        else unexpectedChar st c'
+      if T.null t
+        then emptyNameComponent st
+        else pure ()
+      pure (AIdent, t)
+    _ -> P.error "nameSeg should only be called if current character is a letter, symbol, or backtick"
 
-nameFromHeadTail :: Text -> [Text] -> Name
-nameFromHeadTail head tail =
-  let go s [] = ([], s)
-      go s (t : ts) = let (ts', t') = go t ts in (s : ts', t')
-      (init, last) = go head tail
-   in Name init last
+nameSegStart :: Char -> Bool
+nameSegStart c = isAlphaNumStart c || isSymbol c || c == '`'
 
 -- | Lex a name
-name :: LexState -> IO Name
-name st = nameFromHeadTail <$> nameSeg st <*> tail
-  where
-    tail =
-      peek st >>= \case
-        '/' -> advance st >> (:) <$> nameSeg st <*> tail
-        _ -> pure []
+name :: LexState -> Maybe Kind -> IO ()
+name st wanted = do
+  (k, t) <- nameSeg st
+  go k t []
+ where
+  go k t stack =
+    peek st >>= \case
+      '/' -> do
+        case k of
+          AIdent -> pure ()
+          _ -> report st InvalidNamespace "used keyword as namespace component"
+        advance st
+        peek st >>= \case
+          c | nameSegStart c -> do
+            (k', t') <- nameSeg st
+            go k' t' (t : stack)
+          _ -> do
+            report st UncontinuedQualifiedName "expected continuation of qualified name"
+            emitName k t stack
+      _ -> emitName k t stack
+  emitName k t stack = case wanted of
+    Nothing -> case k of
+      AIdent; SIdent -> emit st k (VName $ Name (reverse stack) t)
+      _ -> case stack of
+        [] -> emit st k (VName $ Name (reverse stack) t)
+        _ -> do
+          report st KeywordInNamespace "referred to keyword as a qualified name"
+          let k' = if T.all isSymbol $ T.take 1 t then SIdent else AIdent
+          emit st k' (VName $ Name (reverse stack) t)
+    Just k' -> case k of
+      AIdent -> emit st k' (VName $ Name (reverse stack) t)
+      _ -> do
+        report st InvalidKeyword $ "used reserved word as a" <+> dpretty k'
+        emit st k' (VName $ Name (reverse stack) t)
 
 ident :: LexState -> IO ()
-ident st = do
-  x <- name st
-  emit st (classifyName st x) (VName x)
+ident st = name st Nothing
 
 int :: LexState -> IO Int
 int st = go 0
-  where
-    go i = do
-      c <- peek st
-      if isDigit c
-        then advance st >> go (i * 10 + (ord c - ord '0'))
-        else pure i
+ where
+  go i = do
+    c <- peek st
+    if isDigit c
+      then advance st >> go (i * 10 + (ord c - ord '0'))
+      else pure i
 
 comment :: LexState -> IO ()
 comment st = do
@@ -234,6 +287,12 @@
   x <- slice st (Span (s + 1) (e - 1))
   emit st String (VString x)
 
+tryName :: LexState -> Kind -> DDoc -> IO ()
+tryName st k d =
+  peek st >>= \case
+    c | nameSegStart c -> name st (Just k)
+    _ -> report st ExpectedName $ "expected a name after" <+> d
+
 -- Top-level lexing interface
 --------------------------------------------------------------------------------
 
@@ -254,9 +313,10 @@
     '\n' -> classify st Nl >> run st
     '#' -> comment st >> run st
     '\"' -> string st >> run st
-    '.' -> advance st >> (name st >>= emit st Field . VName) >> run st
-    '\'' -> advance st >> (name st >>= emit st Tag . VName) >> run st
+    '.' -> advance st >> tryName st Field "period" >> run st
+    '\'' -> advance st >> tryName st Tag "single quote" >> run st
     '\0' -> emit0 st Eof
+    '`' -> ident st >> run st
     c | isDigit c -> (int st >>= emit st Int . VInt) >> run st
     c | isLetter c || c == '_' || isSymbol c -> ident st >> run st
     c -> unexpectedChar st c >> run st
@@ -267,7 +327,7 @@
   pos <- newIORef 0
   prev <- newIORef 0
   iter <- newIORef $ TU.iter file.contents 0
-  out <- bufferWithCapacity (TU.lengthWord8 file.contents)
+  out <- bufferWithCapacity (TU.lengthWord8 file.contents + 1)
   let st = LexState pos prev iter out file reporter config
   run st
   bufferUnsafeFreeze st.out
diff --git a/src/FNotation/Names.hs b/src/FNotation/Names.hs
--- a/src/FNotation/Names.hs
+++ b/src/FNotation/Names.hs
@@ -1,29 +1,57 @@
-module FNotation.Names where
+module FNotation.Names (
+  Name (..),
+  dprettyWithKinds,
+  dprettyOpWithKinds,
+) where
 
+import Data.Char (isDigit, isLetter)
+import Data.List (intersperse)
 import Data.String (IsString, fromString)
 import Data.Text (Text)
+import Data.Text qualified as T
 import Diagnostician
+import FNotation.Config (ConfTable, confTableLookup)
+import FNotation.Kinds (Kind (..))
 import Prettyprinter
 
--- | A name of the form `a/b/c`
---
--- The properties of a name (such as the precedence when used as an operator) are
--- determined by the *last* segment. Thus, `a/+` is an infix operator with the
--- same precedence as `+`.
---
--- This also means, for instance, that if `theory` is a keyword, then `fresh/theory`
--- is also a keyword.
+{- | A name of the form `a/b/c`
+
+The properties of a name (such as the precedence when used as an operator) are
+determined by the *last* segment. Thus, `a/+` is an infix operator with the
+same precedence as `+`.  If you quote the `+` with backticks, however, it will parse as a simple identifier with the same name.
+
+Using a keyword as the last segment of a name is an error unless the keyword is quoted with backticks, in which case it is still not a keyword but an ordinary identifier.
+-}
 data Name = Name
-  { init :: [Text],
-    last :: Text
+  { init :: [Text]
+  , last :: Text
   }
   deriving (Eq, Ord)
 
 instance Show Name where
-  show x = mconcat ((<> "/") . show <$> x.init) <> show x.last
+  show x = mconcat ((<> "/") . T.unpack <$> x.init) <> T.unpack x.last
 
 instance DPretty Name where
   dpretty x = mconcat ((<> "/") . pretty <$> x.init) <> pretty x.last
+
+pand :: (a -> Bool) -> (a -> Bool) -> (a -> Bool)
+pand f g x = f x && g x
+
+por :: (a -> Bool) -> (a -> Bool) -> (a -> Bool)
+por f g x = f x || g x
+
+dprettyWithKinds :: ConfTable Kind -> Name -> DDoc
+dprettyWithKinds config x = mconcat . intersperse "/" . map (namesegWithKinds config) $ x.init ++ [x.last]
+
+dprettyOpWithKinds :: ConfTable Kind -> Name -> DDoc
+dprettyOpWithKinds config x = mconcat . intersperse "/" $ (namesegWithKinds config `map` x.init) ++ [pretty x.last]
+
+namesegWithKinds :: ConfTable Kind -> Text -> DDoc
+namesegWithKinds config x = case confTableLookup config x of
+  (Nothing; Just AIdent)
+    | T.all (isLetter `por` isDigit `por` ('_' ==) `por` ('-' ==)) `pand` (T.any (isLetter `por` ('_' ==)) . T.take 1) $ x ->
+        pretty x
+  _ -> "`" <> pretty x <> "`"
 
 instance IsString Name where
   fromString s = Name [] (fromString s)
diff --git a/src/FNotation/Parser.hs b/src/FNotation/Parser.hs
--- a/src/FNotation/Parser.hs
+++ b/src/FNotation/Parser.hs
@@ -7,6 +7,7 @@
 import Data.Vector qualified as V
 import Diagnostician
 import FNotation.Config
+import FNotation.Kinds qualified as T
 import FNotation.Names
 import FNotation.Tokens qualified as T
 import FNotation.Trees
@@ -20,27 +21,29 @@
   = UnexpectedToken
   | DefaultedPrec
   | IncompatiblePrecedences
+  | ModifierWithoutModifyee
   deriving (Eq, Ord)
 
 parserCodeTable :: Map ParserCode CodeMeta
 parserCodeTable =
   Map.fromList
-    [ (UnexpectedToken, CodeMeta 0 SError Nothing),
-      (DefaultedPrec, CodeMeta 1 SWarning Nothing),
-      (IncompatiblePrecedences, CodeMeta 2 SError Nothing)
+    [ (UnexpectedToken, CodeMeta 0 SError Nothing)
+    , (DefaultedPrec, CodeMeta 1 SWarning Nothing)
+    , (IncompatiblePrecedences, CodeMeta 2 SError Nothing)
+    , (ModifierWithoutModifyee, CodeMeta 3 SError Nothing)
     ]
 
 -- Parser monad
 --------------------------------------------------------------------------------
 
 data ParseState = ParseState
-  { pos :: IORef Int,
-    gas :: IORef Int,
-    skipNewlines :: IORef Bool,
-    tokens :: V.Vector T.Token,
-    file :: File,
-    reporter :: Reporter ParserCode,
-    config :: ConfTable Prec
+  { pos :: IORef Int
+  , gas :: IORef Int
+  , skipNewlines :: IORef Bool
+  , tokens :: V.Vector T.Token
+  , file :: File
+  , reporter :: Reporter ParserCode
+  , config :: ConfTable Prec
   }
 
 -- Parsing utilities
@@ -166,14 +169,14 @@
 argStarts :: V.Vector T.Kind
 argStarts =
   V.fromList
-    [ T.LParen,
-      T.LBrack,
-      T.AIdent,
-      T.AKeyword,
-      T.Field,
-      T.Tag,
-      T.Int,
-      T.Block
+    [ T.LParen
+    , T.LBrack
+    , T.AIdent
+    , T.AKeyword
+    , T.Field
+    , T.Tag
+    , T.Int
+    , T.Block
     ]
 
 argStart :: T.Kind -> Bool
@@ -233,7 +236,9 @@
       x <- curString st
       advanceClose st m $ String x
     T.Block -> block st
-    k -> error $ "should only call arg when the starting token is in argStarts, got: " ++ show k
+    k -> do
+      reportUnexpected st k T.CExprStart
+      advanceClose st m Error
 
 args :: ParseState -> IO [Ntn]
 args st = do
@@ -244,59 +249,75 @@
 
 expr :: ParseState -> IO Ntn
 expr st = arg st >>= go (Prec 0 AssocNon)
-  where
-    go p lhs = do
-      cur st >>= \case
-        k@(T.SIdent; T.SKeyword) -> do
-          s <- curSpan st
-          x <- curName st
-          let n = case k of
-                T.SIdent -> Ident x s
-                T.SKeyword -> Keyword x s
-          p' <- case confTableLookup st.config x.last of
-            Just p' -> pure p'
-            Nothing -> do
-              report st s DefaultedPrec $
-                "Defaulted precedence of" <+> dpretty x <+> "to the same as +"
-              pure $ Prec 50 AssocL
-          case precLe p p' of
-            Nothing -> do
-              report st s IncompatiblePrecedences "Incompatible precedences"
-              pure lhs
-            Just False -> pure lhs
-            Just True -> do
-              advance st
-              rhs <- arg st >>= go p'
-              go p (Infix lhs n rhs)
-        k | argStart k -> do
-          spine <- args st
-          go p (App lhs spine)
-        _ -> pure lhs
+ where
+  go p lhs = do
+    cur st >>= \case
+      k@(T.SIdent; T.SKeyword) -> do
+        s <- curSpan st
+        x <- curName st
+        let n = case k of
+              T.SIdent -> Ident x s
+              T.SKeyword -> Keyword x s
+        p' <- case confTableLookup st.config x.last of
+          Just p' -> pure p'
+          Nothing -> do
+            report st s DefaultedPrec $
+              "Defaulted precedence of" <+> dpretty x <+> "to the same as +"
+            pure $ Prec 50 AssocL
+        case precLe p p' of
+          Nothing -> do
+            report st s IncompatiblePrecedences "Incompatible precedences"
+            pure lhs
+          Just False -> pure lhs
+          Just True -> do
+            advance st
+            rhs <- arg st >>= go p'
+            go p (Infix lhs n rhs)
+      k | argStart k -> do
+        rhs <- arg st
+        go p (Juxt lhs rhs)
+      _ -> pure lhs
 
+decl :: ParseState -> IO Ntn
+decl st = do
+  p <- openingPos st
+  go p []
+ where
+  go p mods =
+    cur st >>= \case
+      T.Modifier -> do
+        m <- curName st
+        advance st
+        go p (m : mods)
+      T.Decl -> do
+        x <- curName st
+        advance st
+        n <- expr st
+        expect st T.Nl
+        pure $ MDecl (reverse mods) x n (Span p (endPos n))
+      _ -> do
+        s <- curSpan st
+        report st s ModifierWithoutModifyee "expected a declaration after a declaration modifier"
+        advanceClose st p Error
+
 stmt :: ParseState -> IO Ntn
-stmt st = do
+stmt st =
   cur st >>= \case
-    T.Decl -> do
-      m <- openingPos st
-      x <- curName st
-      advance st
-      n <- expr st
-      expect st T.Nl
-      pure $ Decl x n (Span m (endPos n))
+    T.Modifier; T.Decl -> decl st
     _ -> expr st
 
 stmts :: ParseState -> IO [Ntn]
 stmts st = go []
-  where
-    go ns =
-      cur st >>= \case
-        T.Nl -> do
-          advance st
-          go ns
-        k | k == T.End || k == T.Eof -> pure $ reverse ns
-        _ -> do
-          n <- stmt st
-          go $ n : ns
+ where
+  go ns =
+    cur st >>= \case
+      T.Nl -> do
+        advance st
+        go ns
+      k | k == T.End || k == T.Eof -> pure $ reverse ns
+      _ -> do
+        n <- stmt st
+        go $ n : ns
 
 block :: ParseState -> IO Ntn
 block st =
diff --git a/src/FNotation/Pretty.hs b/src/FNotation/Pretty.hs
--- a/src/FNotation/Pretty.hs
+++ b/src/FNotation/Pretty.hs
@@ -2,6 +2,7 @@
 
 import Diagnostician
 import FNotation.Config
+import FNotation.Kinds (Kind)
 import FNotation.Names
 import FNotation.Trees
 import Prettyprinter
@@ -29,7 +30,7 @@
 looser :: Prec -> PrevPrec -> Bool
 looser p p' = not $ tighter p p'
 
-type ConfigArg = (?config :: ConfTable Prec)
+type ConfigArg = (?config :: ConfTable Prec, ?lconfig :: ConfTable Kind)
 
 prtTop :: (ConfigArg) => NtnGeneric a -> DDoc
 prtTop = prt Top
@@ -43,9 +44,9 @@
 
 prt :: (ConfigArg) => PrevPrec -> NtnGeneric a -> DDoc
 prt p = \case
-  App n ns ->
+  Juxt n n' ->
     par (looser precApp p) $
-      prt (LeftOf precApp) n <+> hsep (prt (RightOf precApp) <$> ns)
+      prt (LeftOf precApp) n <+> prt (RightOf precApp) n'
   Infix l n r ->
     let mp' = case n of
           Ident x _ -> confTableLookup ?config x.last
@@ -58,15 +59,16 @@
       [dpretty x <> maybe mempty ((" " <>) . prtTop) hd]
         ++ [indent 2 $ prtTop stmt | stmt <- stmts]
         ++ ["end"]
-  Decl x n _ -> dpretty x <+> prtTop n
-  Ident x _ -> dpretty x
+  MDecl ms x n _ -> hsep (dpretty <$> (ms ++ [x])) <+> prtTop n
+  Ident x _ | Bot <- p -> dprettyOpWithKinds ?lconfig x
+  Ident x _ -> dprettyWithKinds ?lconfig x
   Keyword x _ -> dpretty x
-  Field x _ -> "." <> dpretty x
-  Tag x _ -> "'" <> dpretty x
+  Field x _ -> "." <> dprettyWithKinds ?lconfig x
+  Tag x _ -> "'" <> dprettyWithKinds ?lconfig x
   Int i _ -> pretty i
   String x _ -> "\"" <> pretty x <> "\""
   Tuple ns _ -> list $ prtTop <$> ns
   Error _ -> "<error>"
 
-dprettyWithPrecs :: ConfTable Prec -> NtnGeneric a -> DDoc
-dprettyWithPrecs config n = let ?config = config in prtTop n
+dprettyWithConfigs :: ConfTable Prec -> ConfTable Kind -> NtnGeneric a -> DDoc
+dprettyWithConfigs config lconfig n = let ?config = config; ?lconfig = lconfig in prtTop n
diff --git a/src/FNotation/Tokens.hs b/src/FNotation/Tokens.hs
--- a/src/FNotation/Tokens.hs
+++ b/src/FNotation/Tokens.hs
@@ -2,73 +2,42 @@
 
 import Data.Text (Text)
 import Diagnostician
+import FNotation.Kinds
 import FNotation.Names
 import Prettyprinter
 
--- Token kinds
---------------------------------------------------------------------------------
-
-data Kind
-  = -- | alphanumerical identifier
-    AIdent
-  | -- | alphanumerical keyword
-    AKeyword
-  | -- | symbolic identifier
-    SIdent
-  | -- | symbolic keyword
-    SKeyword
-  | Decl
-  | Block
-  | End
-  | Tag
-  | Field
-  | Int
-  | String
-  | LParen
-  | RParen
-  | LBrack
-  | RBrack
-  | LCurly
-  | RCurly
-  | Comma
-  | Semicolon
-  | Nl
-  | Eof
-  | Error
-  deriving (Eq, Show)
-
-instance DPretty Kind where
-  dpretty k = pretty (show k)
+-- * Tokens
 
--- Tokens
 --------------------------------------------------------------------------------
 
 data TokenValue = VEmpty | VName Name | VInt Int | VString Text
   deriving (Eq, Show)
 
--- | A @Token@ consists of a kind along with an attached value and a source code
--- location.
---
--- We split the kind and the attached value so that we can store a set of token
--- kinds as a data structure; otherwise the only way to classify tokens would be
--- functions.
+{- | A @Token@ consists of a kind along with an attached value and a source code
+location.
+
+We split the kind and the attached value so that we can store a set of token
+kinds as a data structure; otherwise the only way to classify tokens would be
+functions.
+-}
 data Token = Token
-  { kind :: Kind,
-    value :: TokenValue,
-    span :: Span
+  { kind :: Kind
+  , value :: TokenValue
+  , span :: Span
   }
   deriving (Eq)
 
 instance DPretty Token where
   dpretty (Token k v s) = dpretty k <> pv <+> "(" <> dpretty s <> ")"
-    where
-      pv = case v of
-        VEmpty -> mempty
-        VName x -> " " <> dpretty x
-        VInt i -> " " <> pretty i
-        VString i -> " " <> pretty i
+   where
+    pv = case v of
+      VEmpty -> mempty
+      VName x -> " " <> dpretty x
+      VInt i -> " " <> pretty i
+      VString i -> " " <> pretty i
 
--- Token classes (used for error messages)
+-- * Token classes (used for error messages)
+
 --------------------------------------------------------------------------------
 
 data Class
diff --git a/src/FNotation/Trees.hs b/src/FNotation/Trees.hs
--- a/src/FNotation/Trees.hs
+++ b/src/FNotation/Trees.hs
@@ -1,5 +1,8 @@
+{-# LANGUAGE ViewPatterns #-}
+
 module FNotation.Trees where
 
+import Data.List.NonEmpty (NonEmpty (..))
 import Data.Maybe (maybeToList)
 import Data.Text (Text)
 import Diagnostician
@@ -10,20 +13,22 @@
 -- Notation data structure
 --------------------------------------------------------------------------------
 
--- | Notation is the output of parsing.
---
--- Each notation is associated with a span. Most variants store that span; `App`
--- and `Infix` don't because the span can be inferred by looking at the left and
--- right children.
---
--- In the variants which take a span, we put the span last because in the parser
--- we have utility methods which take `Span -> Ntn`, and if the span is last, we
--- can use currying to our advantage here.
+{- | Notation is the output of parsing.
+
+Each notation is associated with a span. Most variants store that span; `App`
+and `Infix` don't because the span can be inferred by looking at the left and
+right children.
+
+In the variants which take a span, we put the span last because in the parser
+we have utility methods which take `Span -> Ntn`, and if the span is last, we
+can use currying to our advantage here.
+-}
 data NtnGeneric a
-  = App (NtnGeneric a) [NtnGeneric a]
+  = Juxt (NtnGeneric a) (NtnGeneric a)
   | Infix (NtnGeneric a) (NtnGeneric a) (NtnGeneric a)
   | Block Name (Maybe (NtnGeneric a)) [NtnGeneric a] a
-  | Decl Name (NtnGeneric a) a
+  | -- a declaration with modifiers
+    MDecl [Name] Name (NtnGeneric a) a
   | Tuple [NtnGeneric a] a
   | Ident Name a
   | Keyword Name a
@@ -33,15 +38,29 @@
   | String Text a
   | Error a
 
+pattern Decl :: Name -> NtnGeneric a -> a -> NtnGeneric a
+pattern Decl x n s = MDecl [] x n s
+
+pattern Group :: NonEmpty (NtnGeneric a) -> NtnGeneric a
+pattern Group xs <- (getGroup [] -> xs)
+  where
+    Group (x :| xs) = foldl' (flip Juxt) x xs
+
+{-# COMPLETE Group #-}
+
+getGroup :: [NtnGeneric a] -> NtnGeneric a -> NonEmpty (NtnGeneric a)
+getGroup xs (Juxt f x) = getGroup (x : xs) f
+getGroup xs f = f :| xs
+
 type Ntn = NtnGeneric Span
 
 type Ntn0 = NtnGeneric ()
 
 startPos :: Ntn -> Pos
-startPos (App f _) = startPos f
+startPos (Juxt f _) = startPos f
 startPos (Infix x _ _) = startPos x
 startPos (Block _ _ _ s) = s.start
-startPos (Decl _ _ s) = s.start
+startPos (MDecl _ _ _ s) = s.start
 startPos (Ident _ s) = s.start
 startPos (Keyword _ s) = s.start
 startPos (Field _ s) = s.start
@@ -52,10 +71,10 @@
 startPos (Error s) = s.start
 
 endPos :: Ntn -> Pos
-endPos (App _ xs) = endPos (last xs)
+endPos (Juxt _ x) = endPos x
 endPos (Infix _ _ y) = endPos y
 endPos (Block _ _ _ s) = s.end
-endPos (Decl _ _ s) = s.end
+endPos (MDecl _ _ _ s) = s.end
 endPos (Ident _ s) = s.end
 endPos (Keyword _ s) = s.end
 endPos (Field _ s) = s.end
@@ -72,10 +91,10 @@
 --------------------------------------------------------------------------------
 
 head :: Ntn -> DDoc
-head (App _ _) = "App"
+head (Juxt _ _) = "Juxt"
 head (Infix _ _ _) = "Infix"
 head (Block x _ _ _) = "Block" <+> dpretty x
-head (Decl x _ _) = "Decl" <+> dpretty x
+head (MDecl mods x _ _) = "MDecl" <+> hsep (dpretty <$> mods ++ [x])
 head (Ident x _) = "Ident" <+> dpretty x
 head (Keyword x _) = "Keyword" <+> dpretty x
 head (Field x _) = "Field" <+> dpretty x
@@ -86,10 +105,10 @@
 head (Error _) = "Error"
 
 children :: Ntn -> [Ntn]
-children (App f xs) = f : xs
+children (Juxt f x) = [f, x]
 children (Infix x op y) = [x, op, y]
 children (Block _ mh xs _) = maybeToList mh ++ xs
-children (Decl _ x _) = [x]
+children (MDecl _ _ n _) = [n]
 children (Ident _ _) = []
 children (Keyword _ _) = []
 children (Field _ _) = []
@@ -101,6 +120,6 @@
 
 instance DPretty Ntn where
   dpretty n = if null cs then h else vsep [h, indent 2 $ vsep cs]
-    where
-      h = head n <+> "(" <> dpretty (span n) <> ")"
-      cs = map dpretty (children n)
+   where
+    h = head n <+> "(" <> dpretty (span n) <> ")"
+    cs = map dpretty (children n)
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -1,117 +1,20 @@
-module Main (main) where
+module Main where
 
-import Data.ByteString.Lazy qualified as LBS
-import Data.Functor.Contravariant (contramap, (>$<))
-import Data.Map (Map)
-import Data.Map qualified as Map
-import Data.Text.IO.Utf8 qualified as T
-import Data.Text.Lazy.Encoding qualified as TLE
-import Data.Vector qualified as V
-import Diagnostician
-import FNotation
-import FNotation.Tokens qualified as K
-import Prettyprinter
-import Prettyprinter.Render.Text
-import System.FilePath (replaceExtension, takeBaseName)
-import System.IO
-import System.IO.Temp (withSystemTempFile)
-import Test.Tasty (TestTree, defaultMain, testGroup)
-import Test.Tasty.Golden (findByExtension, goldenVsString)
-import Prelude hiding (lex)
+import Test.FNotation.Golden (goldenTests)
+import Test.FNotation.Property.Lexing (lexerProperties)
+import Test.FNotation.Property.Parsing (parserProperties)
+import Test.Tasty
 
 main :: IO ()
-main = defaultMain =<< goldenTests
-
-render :: DDoc -> LBS.ByteString
-render = TLE.encodeUtf8 . renderLazy . layoutPretty defaultLayoutOptions
-
-lexConfig :: ConfTable Kind
-lexConfig =
-  confTableFromList
-    [ ("sig", K.Block),
-      ("struct", K.Block),
-      ("sum", K.Block),
-      ("match", K.Block),
-      ("theory", K.Decl),
-      ("def", K.Decl),
-      ("type", K.Decl),
-      ("let", K.Decl),
-      ("open", K.Decl),
-      ("import", K.Decl),
-      ("end", K.End),
-      ("Type", K.AKeyword),
-      ("Int", K.AKeyword),
-      ("String", K.AKeyword),
-      (":=", K.SKeyword),
-      ("=", K.SKeyword),
-      (":", K.SKeyword),
-      ("->", K.SKeyword),
-      ("=>", K.SKeyword)
-    ]
-
-parseConfig :: ConfTable Prec
-parseConfig =
-  confTableFromList
-    [ (":=", Prec 10 AssocNon),
-      (":", Prec 20 AssocNon),
-      ("->", Prec 30 AssocR),
-      ("=>", Prec 30 AssocR),
-      ("=", Prec 40 AssocNon),
-      ("+", Prec 50 AssocL),
-      ("-", Prec 50 AssocL),
-      ("*", Prec 60 AssocL),
-      ("/", Prec 60 AssocL)
-    ]
-
-data TestCode = LexerCode LexerCode | ParserCode ParserCode
-  deriving (Eq, Ord)
-
-codeTable :: Map TestCode CodeMeta
-codeTable =
-  mconcat
-    [ promoteCodeTable lexerCodeTable LexerCode 0,
-      promoteCodeTable parserCodeTable ParserCode 100
-    ]
-
-instance Code TestCode where
-  codeMeta c = case Map.lookup c codeTable of
-    Just m -> m
-    Nothing -> error "unregistered code"
-
-parseToPretty :: FilePath -> IO LBS.ByteString
-parseToPretty fp = do
-  src <- T.readFile fp
-  let f = newFile fp src
-  withSystemTempFile "reporter-output" $ \path h -> do
-    let r = fileReporter h
-    tokens <- lex lexConfig (contramap LexerCode r) f
-    ns <- parse parseConfig (contramap ParserCode r) f tokens
-    hFlush h
-    hClose h
-    msgs <- T.readFile path
-    pure $
-      render $
-        vsep
-          [ "-- tokens",
-            vsep $ dpretty <$> V.toList tokens,
-            "",
-            "-- notation",
-            vsep $ dpretty <$> ns,
-            "",
-            "-- pretty",
-            vsep $ dprettyWithPrecs parseConfig <$> ns,
-            "",
-            "-- messages",
-            pretty $ msgs
-          ]
-
-goldenTests :: IO TestTree
-goldenTests = do
-  ntnFiles <- findByExtension [".ntn"] "."
-  return $
+main = do
+  golden <- goldenTests
+  defaultMain $
     testGroup
-      "FNotation golden tests"
-      [ goldenVsString (takeBaseName ntnFile) outputFile (parseToPretty ntnFile)
-      | ntnFile <- ntnFiles,
-        let outputFile = replaceExtension ntnFile ".output"
+      "FNotation"
+      [ golden
+      , testGroup
+          "Property Tests"
+          [ lexerProperties
+          , parserProperties
+          ]
       ]
diff --git a/test/Test/FNotation/Common.hs b/test/Test/FNotation/Common.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/FNotation/Common.hs
@@ -0,0 +1,45 @@
+module Test.FNotation.Common where
+
+import FNotation
+import FNotation.Kinds qualified as K
+import Prelude hiding (lex)
+
+lexConfig :: ConfTable Kind
+lexConfig =
+  confTableFromList
+    [ ("sig", K.Block)
+    , ("struct", K.Block)
+    , ("sum", K.Block)
+    , ("match", K.Block)
+    , ("theory", K.Decl)
+    , ("def", K.Decl)
+    , ("type", K.Decl)
+    , ("let", K.Decl)
+    , ("open", K.Decl)
+    , ("import", K.Decl)
+    , ("inductive", K.Modifier)
+    , ("export", K.Modifier)
+    , ("end", K.End)
+    , ("Type", K.AKeyword)
+    , ("Int", K.AKeyword)
+    , ("String", K.AKeyword)
+    , (":=", K.SKeyword)
+    , ("=", K.SKeyword)
+    , (":", K.SKeyword)
+    , ("->", K.SKeyword)
+    , ("=>", K.SKeyword)
+    ]
+
+parseConfig :: ConfTable Prec
+parseConfig =
+  confTableFromList
+    [ (":=", Prec 10 AssocNon)
+    , (":", Prec 20 AssocNon)
+    , ("->", Prec 30 AssocR)
+    , ("=>", Prec 30 AssocR)
+    , ("=", Prec 40 AssocNon)
+    , ("+", Prec 50 AssocL)
+    , ("-", Prec 50 AssocL)
+    , ("*", Prec 60 AssocL)
+    , ("/", Prec 60 AssocL)
+    ]
diff --git a/test/Test/FNotation/Golden.hs b/test/Test/FNotation/Golden.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/FNotation/Golden.hs
@@ -0,0 +1,82 @@
+module Test.FNotation.Golden (goldenTests) where
+
+import Control.Exception
+import Data.ByteString.Lazy qualified as LBS
+import Data.Functor.Contravariant (contramap)
+import Data.Map (Map)
+import Data.Map qualified as Map
+import Data.Text.IO.Utf8 qualified as T
+import Data.Text.Lazy qualified as TL
+import Data.Text.Lazy.Encoding qualified as TLE
+import Data.Vector qualified as V
+import Diagnostician
+import FNotation
+import Prettyprinter
+import Prettyprinter.Render.Text
+import System.FilePath (replaceExtension, takeBaseName)
+import System.IO
+import System.IO.Temp (withSystemTempFile)
+import Test.FNotation.Common
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.Golden (findByExtension, goldenVsString)
+import Prelude hiding (lex)
+
+render :: DDoc -> LBS.ByteString
+render = TLE.encodeUtf8 . renderLazy . layoutPretty defaultLayoutOptions
+
+data TestCode = LexerCode LexerCode | ParserCode ParserCode
+  deriving (Eq, Ord)
+
+codeTable :: Map TestCode CodeMeta
+codeTable =
+  mconcat
+    [ promoteCodeTable lexerCodeTable LexerCode 0
+    , promoteCodeTable parserCodeTable ParserCode 100
+    ]
+
+instance Code TestCode where
+  codeMeta c = case Map.lookup c codeTable of
+    Just m -> m
+    Nothing -> error "unregistered code"
+
+parseToPretty :: FilePath -> IO LBS.ByteString
+parseToPretty fp = do
+  src <- T.readFile fp
+  let f = newFile fp src
+  withSystemTempFile "reporter-output" $ \path h -> do
+    let r = fileReporter h
+    try @SomeException (lex lexConfig (contramap LexerCode r) f) >>= \case
+      Left err -> pure $ TLE.encodeUtf8 $ "lex error:\n" <> TL.show err
+      Right tokens -> do
+        try @SomeException (parse parseConfig (contramap ParserCode r) f tokens) >>= \case
+          Left err -> pure $ TLE.encodeUtf8 $ "parse error:\n" <> TL.show err
+          Right ns -> do
+            hFlush h
+            hClose h
+            msgs <- T.readFile path
+            pure $
+              render $
+                vsep
+                  [ "-- tokens"
+                  , vsep $ dpretty <$> V.toList tokens
+                  , ""
+                  , "-- notation"
+                  , vsep $ dpretty <$> ns
+                  , ""
+                  , "-- pretty"
+                  , vsep $ dprettyWithConfigs parseConfig lexConfig <$> ns
+                  , ""
+                  , "-- messages"
+                  , pretty $ msgs
+                  ]
+
+goldenTests :: IO TestTree
+goldenTests = do
+  ntnFiles <- findByExtension [".ntn"] "."
+  return $
+    testGroup
+      "Golden tests"
+      [ goldenVsString (takeBaseName ntnFile) outputFile (parseToPretty ntnFile)
+      | ntnFile <- ntnFiles
+      , let outputFile = replaceExtension ntnFile ".output"
+      ]
diff --git a/test/Test/FNotation/Property/Gen/Source.hs b/test/Test/FNotation/Property/Gen/Source.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/FNotation/Property/Gen/Source.hs
@@ -0,0 +1,280 @@
+-- | QuickCheck generators for FNotation source text.
+module Test.FNotation.Property.Gen.Source (
+  -- * Source text generator
+  FNSource (..),
+)
+where
+
+import Data.Text (Text)
+import Data.Text qualified as T
+import Test.QuickCheck
+
+--------------------------------------------------------------------------------
+-- FNotation source text generator
+--------------------------------------------------------------------------------
+
+{- | A newtype wrapper for generated FNotation source text that is suitable
+for feeding to the lexer. The generated text exercises every lexer code path:
+
+ * Alphanumeric identifiers (starting with letter or @_@, containing
+   letters, digits, @_@, @-@)
+ * Symbolic identifiers (sequences of @\< \> - + / * ~ : =@)
+ * Qualified names (@a\/b\/c@, alphanumeric segments separated by @\/@)
+ * Integer literals
+ * String literals (@\"...\"@)
+ * Field access (@.name@)
+ * Tag literals (@\'name@)
+ * Punctuation: @( ) [ ] { } , ;@
+ * Newlines
+ * Whitespace (spaces and tabs)
+ * Comments (@# ...@)
+ * Unexpected characters (to test error recovery)
+-}
+newtype FNSource = FNSource {getText :: Text}
+  deriving (Show)
+
+instance Arbitrary FNSource where
+  arbitrary = sized \n -> FNSource . T.concat <$> genTokenList (max 1 n)
+  shrink (FNSource t) =
+    let ts = [deleteAt i t | i <- [0 .. T.length t - 1]]
+        deleteAt i s =
+          let (a, b) = T.splitAt i s
+           in a <> T.drop 1 b
+     in FNSource <$> ts
+
+{- | Generate a list of textual token fragments that together form valid
+(or intentionally invalid) FNotation source.
+-}
+genTokenList :: Int -> Gen [Text]
+genTokenList n = do
+  numTokens <- chooseInt (1, max 1 (n * 2))
+  go numTokens
+ where
+  go 0 = pure []
+  go remaining = do
+    (tok, sep) <- genSourceToken
+    rest <- go (remaining - 1)
+    pure (tok : sep : rest)
+
+{- | Generate a single source token fragment together with an appropriate
+trailing separator. Returns @(token, separator)@.
+
+The frequency weights ensure good coverage of all lexer paths while
+biasing towards the most common constructs.
+-}
+genSourceToken :: Gen (Text, Text)
+genSourceToken =
+  frequency
+    [ -- Alphanumeric identifiers: most common token type
+      (15, withSep genAlphaIdent)
+    , -- Symbolic identifiers/operators
+      (8, withSep genSymIdent)
+    , -- Qualified alphanumeric names (a/b, a/b/c)
+      (5, withSep genQualifiedName)
+    , -- Integer literals
+      (6, withSep genIntLiteral)
+    , -- String literals (self-delimiting, no separator needed)
+      (4, noSep genStringLiteral)
+    , -- Field access (.name)
+      (4, noSep genFieldAccess)
+    , -- Tag literal ('name)
+      (4, noSep genTagLiteral)
+    , -- Parentheses
+      (4, noSep $ elements ["(", ")"])
+    , -- Square brackets
+      (4, noSep $ elements ["[", "]"])
+    , -- Curly braces
+      (3, noSep $ elements ["{", "}"])
+    , -- Comma
+      (3, noSep $ pure ",")
+    , -- Semicolon
+      (3, noSep $ pure ";")
+    , -- Newline
+      (5, noSep $ pure "\n")
+    , -- Whitespace (spaces and tabs)
+      (3, noSep genWhitespace)
+    , -- Comments (# to end of line)
+      (3, noSep genComment)
+    , -- Unexpected characters (test error recovery)
+      (1, withSep genUnexpectedChar)
+    ]
+ where
+  withSep g = do
+    tok <- g
+    sep <- genSeparator
+    pure (tok, sep)
+  noSep g = do
+    tok <- g
+    pure (tok, "")
+
+{- | Generate a separator between tokens. Usually a space, sometimes nothing,
+a tab, or a newline.
+-}
+genSeparator :: Gen Text
+genSeparator =
+  frequency
+    [ (5, pure " ")
+    , (1, pure "\t")
+    , (1, pure "\n")
+    , (1, pure "  ")
+    , (1, pure "")
+    ]
+
+{- | Alphanumeric identifier: starts with a letter or @_@, followed by
+letters, digits, @_@, or @-@.
+
+Covers: @isAlphaNumStart@ and @isAlphaNum@ in the lexer.
+-}
+genAlphaIdent :: Gen Text
+genAlphaIdent = do
+  first <- genAlphaStart
+  restLen <- chooseInt (0, 8)
+  rest <- vectorOf restLen genAlphaNumChar
+  pure $ T.pack (first : rest)
+
+-- | Starting character for alphanumeric names: letter or underscore.
+genAlphaStart :: Gen Char
+genAlphaStart =
+  frequency
+    [ (20, elements (['a' .. 'z'] ++ ['A' .. 'Z']))
+    , (2, pure '_')
+    ]
+
+-- | Continuation character for alphanumeric names: letter, digit, @_@, or @-@.
+genAlphaNumChar :: Gen Char
+genAlphaNumChar =
+  frequency
+    [ (15, elements (['a' .. 'z'] ++ ['A' .. 'Z']))
+    , (5, elements ['0' .. '9'])
+    , (2, pure '_')
+    , (1, pure '-')
+    ]
+
+{- | Symbolic identifier: a non-empty sequence of symbol characters.
+Symbol chars: @\< \> - + / * ~ : =@
+
+Note: @/@ is a symbol character, so it gets consumed greedily into
+symbolic tokens. This means qualified names only work with alphanumeric
+leading segments.
+-}
+genSymIdent :: Gen Text
+genSymIdent = do
+  len <- chooseInt (1, 4)
+  T.pack <$> vectorOf len genSymbolChar
+
+-- | A single symbol character as recognized by the lexer's @isSymbol@.
+genSymbolChar :: Gen Char
+genSymbolChar = elements ['<', '>', '-', '+', '/', '*', '~', ':', '=']
+
+{- | Qualified alphanumeric name: two or more alphanumeric segments joined
+by @/@. For example: @mul\/unitl@, @a\/b\/c@.
+
+Qualification only works when segments are alphanumeric (since @/@ is a
+symbol character, a symbolic segment would greedily consume the @/@).
+-}
+genQualifiedName :: Gen Text
+genQualifiedName = do
+  numSegs <- chooseInt (2, 4)
+  segs <- vectorOf numSegs genAlphaSegment
+  pure $ T.intercalate "/" segs
+
+genAlphaSegment :: Gen Text
+genAlphaSegment = do
+  first <- genAlphaStart
+  restLen <- chooseInt (0, 5)
+  rest <- vectorOf restLen genAlphaNumChar
+  pure $ T.pack (first : rest)
+
+-- | Integer literal: a sequence of digits.
+genIntLiteral :: Gen Text
+genIntLiteral = do
+  len <- chooseInt (1, 6)
+  T.pack <$> vectorOf len (elements ['0' .. '9'])
+
+{- | String literal: @\"contents\"@. The lexer reads until the closing @\"@
+with no escape sequences.
+-}
+genStringLiteral :: Gen Text
+genStringLiteral = do
+  len <- chooseInt (0, 20)
+  -- Content can be anything except '"' and '\0' (null terminates the lexer)
+  contents <- vectorOf len genStringChar
+  pure $ T.pack ('"' : contents ++ ['"'])
+
+-- | Characters valid inside a string literal: anything except @\"@ and @\\0@.
+genStringChar :: Gen Char
+genStringChar =
+  frequency
+    [ (10, elements (['a' .. 'z'] ++ ['A' .. 'Z'] ++ ['0' .. '9']))
+    , (3, elements [' ', '\t', '!', '?', '.', ',', ';', ':', '-', '+'])
+    , (1, elements ['\n', '(', ')', '[', ']', '{', '}', '#', '\'', '/'])
+    ]
+
+{- | Field access: @.@ immediately followed by a name. The lexer handles
+this specially — it advances past the dot, then lexes a name.
+-}
+genFieldAccess :: Gen Text
+genFieldAccess = T.cons '.' <$> genFieldOrTagName
+
+-- | Tag literal: @\'@ immediately followed by a name.
+genTagLiteral :: Gen Text
+genTagLiteral = T.cons '\'' <$> genFieldOrTagName
+
+{- | Name suitable for field access or tag literal. Can start with either
+an alphanumeric start char or a symbol char (the lexer's @nameSeg@
+dispatches on both).
+-}
+genFieldOrTagName :: Gen Text
+genFieldOrTagName =
+  frequency
+    [ (4, genAlphaIdent)
+    , (1, genSymIdent)
+    ]
+
+{- | Whitespace: one or more spaces/tabs (not newlines, those are separate
+tokens).
+-}
+genWhitespace :: Gen Text
+genWhitespace = do
+  len <- chooseInt (1, 4)
+  T.pack <$> vectorOf len (elements [' ', '\t'])
+
+{- | Comment: @#@ followed by non-newline characters, terminated by a newline.
+The lexer's @comment@ function advances while @(/= \'\\n\')@ then consumes
+the newline.
+-}
+genComment :: Gen Text
+genComment = do
+  len <- chooseInt (0, 30)
+  body <- vectorOf len genCommentChar
+  pure $ T.pack ('#' : body ++ ['\n'])
+
+-- | Characters valid inside a comment body: anything except newline and null.
+genCommentChar :: Gen Char
+genCommentChar =
+  frequency
+    [ (10, elements (['a' .. 'z'] ++ ['A' .. 'Z'] ++ ['0' .. '9']))
+    , (3, elements [' ', '\t', '!', '?', '.', ',', ';', ':', '-', '+', '*'])
+    , (1, elements ['(', ')', '[', ']', '{', '}', '"', '\'', '/', '#'])
+    ]
+
+{- | Unexpected character: a character that doesn't match any lexer rule,
+triggering the @unexpectedChar@ error path.
+
+These are characters that are not: whitespace, newline, null, digits,
+letters, underscore, symbol chars, punctuation, @#@, @\"@, @.@, or @\'@.
+-}
+genUnexpectedChar :: Gen Text
+genUnexpectedChar =
+  T.singleton
+    <$> elements
+      [ '@'
+      , '\\'
+      , '`'
+      , '!'
+      , '?'
+      , '^'
+      , '&'
+      , '$'
+      , '%'
+      ]
diff --git a/test/Test/FNotation/Property/Gen/Token.hs b/test/Test/FNotation/Property/Gen/Token.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/FNotation/Property/Gen/Token.hs
@@ -0,0 +1,260 @@
+{- | QuickCheck generators for FNotation token streams.
+
+These generators produce 'V.Vector Token' values that satisfy the invariants
+expected by the parser ('FNotation.Parser.parse'):
+
+ 1. Every token has the correct 'Kind'/'TokenValue' pairing:
+
+      * 'AIdent', 'AKeyword', 'SIdent', 'SKeyword', 'Decl', 'Block', 'End',
+        'Field', 'Tag' carry a 'VName'.
+      * 'Int' carries a 'VInt'.
+      * 'String' carries a 'VString'.
+      * All punctuation and structural kinds ('LParen', 'RParen', 'LBrack',
+        'RBrack', 'LCurly', 'RCurly', 'Comma', 'Semicolon', 'Nl', 'Eof',
+        'Error') carry 'VEmpty'.
+
+ 2. The stream is non-empty and always ends with an 'Eof' token (the parser's
+    @stmts@ loop terminates only on 'End' or 'Eof').
+
+ 3. Spans are synthetic but well-formed (non-negative, start <= end), assigned
+    sequentially so they don't overlap.
+-}
+module Test.FNotation.Property.Gen.Token (
+  -- * Token stream wrapper
+  FNTokens (..),
+
+  -- * Individual token generators
+  genToken,
+  genNameToken,
+  genPunctToken,
+)
+where
+
+import Data.Char (chr)
+import Data.Text (Text)
+import Data.Text qualified as T
+import Data.Vector qualified as V
+import Diagnostician (Span (..))
+import FNotation.Kinds (Kind (..))
+import FNotation.Names (Name (..))
+import FNotation.Tokens (Token (..), TokenValue (..))
+import Test.QuickCheck
+
+--------------------------------------------------------------------------------
+-- Token stream newtype
+--------------------------------------------------------------------------------
+
+{- | A newtype wrapper around a non-empty 'V.Vector' of 'Token's that is
+always terminated by 'Eof'. Suitable for feeding directly to
+'FNotation.Parser.parse'.
+-}
+newtype FNTokens = FNTokens {getTokens :: V.Vector Token}
+
+instance Show FNTokens where
+  show (FNTokens ts) =
+    "FNTokens ("
+      ++ show (V.length ts)
+      ++ " tokens): "
+      ++ show (V.toList (V.map (\t -> t.kind) ts))
+
+instance Arbitrary FNTokens where
+  arbitrary = sized \n -> do
+    numTokens <- chooseInt (0, max 0 (n * 3))
+    toks <- genTokenStream numTokens
+    pure (FNTokens toks)
+
+  shrink (FNTokens ts)
+    | V.length ts <= 1 = []
+    | otherwise =
+        -- Remove one non-Eof token at a time, re-assign spans
+        [ FNTokens (reassignSpans (V.ifilter (\i _ -> i /= j) ts))
+        | j <- [0 .. V.length ts - 2]
+        ]
+
+--------------------------------------------------------------------------------
+-- Token stream generation
+--------------------------------------------------------------------------------
+
+{- | Generate a complete token stream: a sequence of arbitrary tokens
+followed by an 'Eof' sentinel. Spans are assigned sequentially.
+-}
+genTokenStream :: Int -> Gen (V.Vector Token)
+genTokenStream n = do
+  toks <- vectorOf n genToken
+  let eof = Token Eof VEmpty dummySpan
+  pure $ reassignSpans (V.fromList (toks ++ [eof]))
+
+{- | Re-assign spans to a token vector so they are sequential and
+non-overlapping. Each token gets a 1-unit span, placed end-to-end.
+-}
+reassignSpans :: V.Vector Token -> V.Vector Token
+reassignSpans = V.imap \i tok -> tok{span = Span i (i + 1)}
+
+-- | A dummy span used as a placeholder before 'reassignSpans' fixes them up.
+dummySpan :: Span
+dummySpan = Span 0 0
+
+--------------------------------------------------------------------------------
+-- Individual token generators
+--------------------------------------------------------------------------------
+
+{- | Generate a single token with a well-formed kind/value pairing.
+
+The frequency distribution covers every 'Kind' constructor. Kinds that the
+parser actively dispatches on ('AIdent', 'SIdent', 'LParen', 'LBrack', 'Nl',
+etc.) are weighted more heavily to produce interesting parse trees.
+-}
+genToken :: Gen Token
+genToken =
+  frequency
+    [ -- Name-bearing tokens (parser dispatches on these in arg/expr/stmt)
+      (10, genNameToken AIdent)
+    , (3, genNameToken AKeyword)
+    , (6, genNameToken SIdent)
+    , (3, genNameToken SKeyword)
+    , (3, genNameToken Decl)
+    , (3, genNameToken Block)
+    , (2, genNameToken End)
+    , (3, genNameToken Field)
+    , (3, genNameToken Tag)
+    , -- Int literals
+      (4, genIntToken)
+    , -- String literals
+      (3, genStringToken)
+    , -- Punctuation / structural
+      (5, genPunctToken LParen)
+    , (5, genPunctToken RParen)
+    , (4, genPunctToken LBrack)
+    , (4, genPunctToken RBrack)
+    , (2, genPunctToken LCurly)
+    , (2, genPunctToken RCurly)
+    , (3, genPunctToken Comma)
+    , (2, genPunctToken Semicolon)
+    , (6, genPunctToken Nl)
+    , -- Error token (parser may encounter these from lexer errors)
+      (1, genPunctToken Error)
+    ]
+
+-- | Generate a token whose kind requires a 'VName' payload.
+genNameToken :: Kind -> Gen Token
+genNameToken k = do
+  n <- genName
+  pure $ Token k (VName n) dummySpan
+
+-- | Generate a token with 'VEmpty' payload (punctuation, structural, error).
+genPunctToken :: Kind -> Gen Token
+genPunctToken k = pure $ Token k VEmpty dummySpan
+
+-- | Generate an integer literal token.
+genIntToken :: Gen Token
+genIntToken = do
+  i <- chooseInt (0, 9999)
+  pure $ Token Int (VInt i) dummySpan
+
+-- | Generate a string literal token.
+genStringToken :: Gen Token
+genStringToken = do
+  t <- genShortText
+  pure $ Token String (VString t) dummySpan
+
+--------------------------------------------------------------------------------
+-- Name generation
+--------------------------------------------------------------------------------
+
+{- | Generate a 'Name'. Names have zero or more qualifying segments and a
+final segment. Each segment is a short alphabetic string.
+-}
+genName :: Gen Name
+genName =
+  frequency
+    [ (4, Name [] <$> genLastSegment)
+    , (2, Name <$> listOf1to3 genQualSegment <*> genLastSegment)
+    ]
+ where
+  listOf1to3 g = do
+    n <- chooseInt (1, 3)
+    vectorOf n g
+
+{- | Generate the final segment of a name. This determines the name's
+classification (identifier vs keyword, alphanumeric vs symbolic), so we
+generate both kinds.
+-}
+genLastSegment :: Gen Text
+genLastSegment =
+  frequency
+    [ (4, genAlphaSegment)
+    , (1, genSymSegment)
+    , (1, genLitSegment)
+    ]
+
+{- | Qualifying segments are never symbolic (symbolic segments
+greedily consume @/@).
+-}
+genQualSegment :: Gen Text
+genQualSegment =
+  frequency
+    [ (4, genAlphaSegment)
+    , (1, genLitSegment)
+    ]
+
+{- | A short alphanumeric name segment: starts with a letter or @_@,
+followed by letters, digits, @_@, or @-@.
+-}
+genAlphaSegment :: Gen Text
+genAlphaSegment = do
+  first <- genAlphaStart
+  restLen <- chooseInt (0, 5)
+  rest <- vectorOf restLen genAlphaNumChar
+  pure $ T.pack (first : rest)
+
+-- | Starting character for alphanumeric segments.
+genAlphaStart :: Gen Char
+genAlphaStart =
+  frequency
+    [ (20, elements (['a' .. 'z'] ++ ['A' .. 'Z']))
+    , (2, pure '_')
+    ]
+
+-- | Continuation character for alphanumeric segments.
+genAlphaNumChar :: Gen Char
+genAlphaNumChar =
+  frequency
+    [ (15, elements (['a' .. 'z'] ++ ['A' .. 'Z']))
+    , (5, elements ['0' .. '9'])
+    , (2, pure '_')
+    , (1, pure '-')
+    ]
+
+{- | A short literal name segment: starts with a backtick,
+followed by non-backtick characters and another backtick
+-}
+genLitSegment :: Gen Text
+genLitSegment = do
+  restLen <- chooseInt (0, 5)
+  rest <- vectorOf restLen genLitChar
+  pure $ T.pack ('`' : rest ++ ['`'])
+
+-- | Continuation character for literal segments.
+genLitChar :: Gen Char
+genLitChar =
+  fmap chr $
+    frequency
+      [ (15, fmap (\case c | c >= 96 -> c + 1 | otherwise -> c) $ chooseInt (32, 254))
+      , (5, chooseInt (256, 0xd7ff))
+      , (2, do plane <- chooseInt (1, 16); off <- chooseInt (0, 0xfffd); pure $ 0x10000 * plane + off)
+      , (1, chooseInt (0xe000, 0xfffd))
+      ]
+
+{- | A short symbolic name segment: a non-empty sequence of symbol characters
+(@\< \> - + \/ * ~ : =@).
+-}
+genSymSegment :: Gen Text
+genSymSegment = do
+  len <- chooseInt (1, 3)
+  T.pack <$> vectorOf len (elements ['<', '>', '-', '+', '/', '*', '~', ':', '='])
+
+-- | A short arbitrary text for string literal payloads.
+genShortText :: Gen Text
+genShortText = do
+  len <- chooseInt (0, 15)
+  T.pack <$> vectorOf len arbitraryPrintableChar
diff --git a/test/Test/FNotation/Property/Lexing.hs b/test/Test/FNotation/Property/Lexing.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/FNotation/Property/Lexing.hs
@@ -0,0 +1,26 @@
+module Test.FNotation.Property.Lexing where
+
+import Data.Vector qualified as V
+import Diagnostician
+import FNotation
+import Test.FNotation.Common
+import Test.FNotation.Property.Gen.Source
+import Test.Tasty
+import Test.Tasty.QuickCheck
+import Prelude hiding (lex)
+
+-- | A reporter that silently discards all diagnostics.
+nullReporter :: Reporter LexerCode
+nullReporter = Reporter{reportIO = \_ -> pure ()}
+
+-- | Property: the lexer should not crash on any generated source text.
+lexerProperties :: TestTree
+lexerProperties =
+  testGroup
+    "Lexer properties"
+    [ testProperty "lexer does not crash on arbitrary source" \(FNSource src) ->
+        ioProperty do
+          let f = newFile "<quickcheck>" src
+          tokens <- lex lexConfig nullReporter f
+          pure $ V.length tokens `seq` True
+    ]
diff --git a/test/Test/FNotation/Property/Parsing.hs b/test/Test/FNotation/Property/Parsing.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/FNotation/Property/Parsing.hs
@@ -0,0 +1,24 @@
+module Test.FNotation.Property.Parsing where
+
+import Diagnostician
+import FNotation
+import Test.FNotation.Common
+import Test.FNotation.Property.Gen.Token
+import Test.Tasty
+import Test.Tasty.QuickCheck
+
+-- | A reporter that silently discards all diagnostics.
+nullReporter :: Reporter ParserCode
+nullReporter = Reporter{reportIO = \_ -> pure ()}
+
+-- | Property: the parser should not crash on any generated token stream.
+parserProperties :: TestTree
+parserProperties =
+  testGroup
+    "Parser properties"
+    [ testProperty "parser does not crash on arbitrary tokens" \(FNTokens tokens) ->
+        ioProperty do
+          let f = newFile "<quickcheck>" ""
+          ns <- parse parseConfig nullReporter f tokens
+          length ns `seq` pure True
+    ]