diff --git a/.github/dependabot.yml b/.github/dependabot.yml
new file mode 100644
index 0000000..ca79ca5
--- /dev/null
+++ b/.github/dependabot.yml
@@ -0,0 +1,6 @@
+version: 2
+updates:
+  - package-ecosystem: github-actions
+    directory: /
+    schedule:
+      interval: weekly
diff --git a/.github/workflows/bench.yml b/.github/workflows/bench.yml
new file mode 100644
index 0000000..a1a833b
--- /dev/null
+++ b/.github/workflows/bench.yml
@@ -0,0 +1,107 @@
+name: Benchmark
+
+# `/bench` PR comment runs the benchmarks and posts a results comment.
+# issue_comment workflows run the copy on the default branch, so it only
+# takes effect once merged there.
+
+on:
+  issue_comment:
+    types: [created]
+  workflow_dispatch:
+
+permissions:
+  contents: read
+  pull-requests: write
+
+jobs:
+  bench:
+    # Trusted commenters only: builds and runs PR code with a write token.
+    if: >-
+      github.event_name == 'workflow_dispatch' ||
+      (github.event.issue.pull_request &&
+       contains(github.event.comment.body, '/bench') &&
+       contains(fromJSON('["OWNER","MEMBER","COLLABORATOR"]'), github.event.comment.author_association))
+    runs-on: ubuntu-latest
+    env:
+      GH_TOKEN: ${{ github.token }}
+    steps:
+      - name: React to trigger
+        if: github.event_name == 'issue_comment'
+        run: |
+          gh api --method POST \
+            "repos/${{ github.repository }}/issues/comments/${{ github.event.comment.id }}/reactions" \
+            -f content=eyes || true
+
+      - name: Resolve PR head
+        id: pr
+        if: github.event_name == 'issue_comment'
+        run: |
+          num=${{ github.event.issue.number }}
+          pr=$(gh api "repos/${{ github.repository }}/pulls/$num")
+          echo "num=$num" >> "$GITHUB_OUTPUT"
+          echo "sha=$(echo "$pr" | jq -r .head.sha)" >> "$GITHUB_OUTPUT"
+          echo "base=$(echo "$pr" | jq -r .base.sha)" >> "$GITHUB_OUTPUT"
+
+      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+        with:
+          ref: ${{ steps.pr.outputs.sha || github.sha }}
+          fetch-depth: 0
+
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
+        with:
+          build: false
+          test: false
+
+      - name: Run benchmarks
+        run: |
+          # PR head: prim + lean4-parser reference.
+          ( cd bench && lake exe cache get >/dev/null 2>&1 || true; lake exe bench; lake exe benchlp )
+          cp bench/bench-prim.tsv prim-pr.tsv
+          cp bench/bench-lp.tsv   lp.tsv
+          # Baseline: same harness against the PR base commit's prim-parser.
+          : > prim-base.tsv
+          if [ -n "${{ steps.pr.outputs.base }}" ]; then
+            git checkout -q "${{ steps.pr.outputs.base }}" -- PrimParser Examples Tests lakefile.toml \
+              && ( cd bench && lake exe bench ) \
+              && cp bench/bench-prim.tsv prim-base.tsv \
+              || echo "baseline bench failed; reporting PR only"
+          fi
+
+      - name: Format results
+        run: |
+          {
+            echo '<!-- bench -->'
+            echo "### Benchmark results"
+            echo ""
+            echo "PR \`${{ steps.pr.outputs.sha || github.sha }}\` vs base \`${{ steps.pr.outputs.base }}\` — min ms over the repetitions. Δ = PR vs base, lower is better. lean4-parser is an external reference."
+            echo ""
+            awk -F'\t' '
+              FILENAME ~ /prim-pr/   { if (!($1 in seen)) { ord[++k]=$1; seen[$1]=1 }; pr[$1]=$2; next }
+              FILENAME ~ /prim-base/ { base[$1]=$2; next }
+              FILENAME ~ /lp\.tsv/   { lp[$1]=$2; next }
+              END {
+                print "| grammar | prim PR ms | prim base ms | Δ | lean4-parser ms |"
+                print "|---|--:|--:|--:|--:|"
+                for (i = 1; i <= k; i++) {
+                  n = ord[i]
+                  has = (n in base)
+                  bm = has ? sprintf("%.2f", base[n]) : "-"
+                  d  = (has && base[n] > 0) ? sprintf("%+.1f%%", (pr[n] - base[n]) / base[n] * 100) : "-"
+                  printf "| %s | %.2f | %s | %s | %.2f |\n", n, pr[n], bm, d, lp[n]
+                }
+              }' prim-pr.tsv prim-base.tsv lp.tsv
+          } > body.md
+          cat body.md >> "$GITHUB_STEP_SUMMARY"
+
+      - name: Post comment
+        if: steps.pr.outputs.num
+        run: |
+          gh pr comment "${{ steps.pr.outputs.num }}" \
+            --body-file body.md --edit-last --create-if-none
+
+      - name: React done
+        if: github.event_name == 'issue_comment'
+        run: |
+          gh api --method POST \
+            "repos/${{ github.repository }}/issues/comments/${{ github.event.comment.id }}/reactions" \
+            -f content=rocket || true
diff --git a/.gitignore b/.gitignore
index 44949d5..e654d96 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,4 @@
 *.lake
 *.md
+bench-data/
+bench-*.tsv
diff --git a/PrimParser/Basic.lean b/PrimParser/Basic.lean
index 8dba4bb..3c5e72b 100644
--- a/PrimParser/Basic.lean
+++ b/PrimParser/Basic.lean
@@ -12,7 +12,24 @@ behavior at the type level via `Necessity`.
 abbrev Error := String
 
 /-- Input text of statically known length `n`. -/
-abbrev Text (n : Nat) := List.Vector Char n
+structure Text (n : Nat) where
+  arr : Array Char
+  off : Nat
+  inv : off + n = arr.size
+
+/-- Runtime decoder: build the char array in a single pass, straight into an
+`Array` (no intermediate `List`, whose construction dominates for large inputs). -/
+@[inline] def decodeArrFast (s : String) : Array Char := s.foldl (fun a c => a.push c) #[]
+
+/-- Decode a `String` to its character array. Definitionally `s.toList.toArray` (so
+`decide`/kernel proofs on concrete inputs reduce), but compiled to the single-pass
+`decodeArrFast` at runtime. -/
+@[implemented_by decodeArrFast]
+def decodeArr (s : String) : Array Char := s.toList.toArray
+
+/-- Build character input from a `String`. -/
+def ofString (s : String) : Text s.toList.length :=
+  { arr := decodeArr s, off := 0, inv := by simp [decodeArr] }
 
 /-- A parser's static grade: whether it may/must produce errors and
 whether it may/must consume input. -/
@@ -292,7 +309,8 @@ def bind
       | possibly => x'.bindParser f⟩
 
 instance : IsEmpty (Parser ε impossible α) where
-  false p := by cases p.run ⟨[], rfl⟩; contradiction
+  false p := by cases p.run (⟨#[], 0, by simp⟩ : Text 0); contradiction
+
 
 /-- Lift a value into a parser that consumes nothing and never fails. -/
 abbrev pure (a : α) : Parser ε 1 α where
@@ -465,12 +483,12 @@ def runResult? (p : Parser ε ⟨ge, gc⟩ α) (t : Text n) : Option α :=
 def anyChar : Parser Error conditional Char where
   run {n} t :=
     match n, t with
-    | 0, .nil => .inl ⟨Error.eof, .nil, by simp⟩
-    | Nat.succ n, ⟨c :: cs, p⟩ =>
-      .inr {result := c
-            restSize := n
-            restText := by refine ⟨cs, by simpa [List.length_cons] using p⟩
-            witness := by simp}
+    | 0, t => .inl ⟨Error.eof, t, by simp⟩
+    | Nat.succ m, t =>
+      .inr {result := t.arr[t.off]'(by have := t.inv; omega)
+            restSize := m
+            restText := ⟨t.arr, t.off + 1, by have := t.inv; omega⟩
+            witness := by omega}
 
 /-- Like `gpure` but with a flexible grade: both `ge` and `gc` can be `never`
 or `possibly`. Useful in match branches where all cases must share the same grade. -/
diff --git a/Tests/Basic.lean b/Tests/Basic.lean
index 8c95a0c..10fd3e7 100644
--- a/Tests/Basic.lean
+++ b/Tests/Basic.lean
@@ -2,7 +2,7 @@ import PrimParser
 
 open Parser
 
-def toText (s : String) : Text s.toList.length := ⟨s.toList, rfl⟩
+def toText (s : String) : Text s.toList.length := ofString s
 
 -- anyChar
 #guard anyChar.runResult? (toText "abc") == some 'a'
diff --git a/bench/Bench.lean b/bench/Bench.lean
new file mode 100644
index 0000000..819c731
--- /dev/null
+++ b/bench/Bench.lean
@@ -0,0 +1,45 @@
+import PrimParser
+import Examples.Json
+import Examples.Lambda
+import BenchGen
+
+-- prim side. lean4-parser side is BenchLp.lean: separate exe because both
+-- libraries define `_root_.Parser` and can't share a module.
+
+open Parser
+
+def toText (s : String) : Text s.toList.length := ofString s
+
+def primInts : Parser Error flexible (List Nat) := sepBy (string ",") nat
+
+def primSexp : Parser Error conditional Nat :=
+  fix fun self =>
+    let plist : Parser Error conditional Nat := gdo
+      lexeme (char '(')
+      let first ← self
+      let rest ← many (gdo whitespace; self)
+      lexeme (char ')')
+      return first + rest.foldl (· + ·) 0
+    let patom : Parser Error conditional Nat :=
+      (fun _ => 1) <$>ᵍ takeWhile1 Char.isAlphanum
+    patom <|> plist
+
+def primCsv : Parser Error flexible Nat :=
+  (fun rows => rows.foldl (fun a r => a + r.length) 0) <$>ᵍ
+    sepBy (char '\n') (sepBy (char ',') nat)
+
+def main : IO Unit := do
+  let reps := 25
+  let intsIn   ← prep "integers" (genInts 20000)
+  let sexpIn   ← prep "sexp"     (genSexp 3 8)
+  let csvIn    ← prep "csv"      (genCsv 4000 6)
+  let jsonIn   ← prep "json"     (genJson 20000)
+  let lambdaIn ← prep "lambda"   (genLambda 2000)
+  IO.println "prim-parser:"
+  let rows := #[
+    ← benchOne "integers" intsIn   reps (fun _ => (primInts.runResult? (toText intsIn)).map (·.foldl (·+·) 0) |>.getD 0),
+    ← benchOne "sexp"     sexpIn   reps (fun _ => (primSexp.runResult? (toText sexpIn)).getD 0),
+    ← benchOne "csv"      csvIn    reps (fun _ => (primCsv.runResult? (toText csvIn)).getD 0),
+    ← benchOne "json"     jsonIn   reps (fun _ => if (Json.json.runResult? (toText jsonIn)).isSome then 1 else 0),
+    ← benchOne "lambda"   lambdaIn reps (fun _ => if (Term.term.runResult? (toText lambdaIn)).isSome then 1 else 0)]
+  writeTsv "bench-prim.tsv" rows
diff --git a/bench/BenchGen.lean b/bench/BenchGen.lean
new file mode 100644
index 0000000..9e46faa
--- /dev/null
+++ b/bench/BenchGen.lean
@@ -0,0 +1,60 @@
+def genInts (n : Nat) : String := String.intercalate "," ((List.range n).map toString)
+
+def genSexp (w : Nat) : Nat → String
+  | 0     => "a"
+  | d + 1 => "(" ++ String.intercalate " " (List.replicate w (genSexp w d)) ++ ")"
+
+def genCsv (rows cols : Nat) : String :=
+  String.intercalate "\n" ((List.range rows).map fun _ =>
+    String.intercalate "," ((List.range cols).map toString))
+
+def genJson (n : Nat) : String := "[" ++ String.intercalate "," ((List.range n).map toString) ++ "]"
+
+def genLambda (n : Nat) : String := String.join (List.replicate n "\\a. ") ++ "x"
+
+structure Stats where
+  minMs : Float
+  medMs : Float
+  meanMs : Float
+  sdMs : Float
+  mbps : Float
+
+def r2 (x : Float) : Float := (x * 100.0).round / 100.0
+
+def statsOf (ns : Array Nat) (bytes : Nat) : Stats :=
+  let sorted := ns.qsort Nat.blt
+  let k := sorted.size
+  let ms (x : Nat) : Float := Float.ofNat x / 1.0e6
+  let mn := ms (sorted.getD 0 0)
+  let med := ms (sorted.getD (k / 2) 0)
+  let mean := (Float.ofNat (ns.foldl (· + ·) 0) / Float.ofNat k) / 1.0e6
+  let var := (ns.foldl (fun a x => a + (ms x - mean) * (ms x - mean)) 0.0) / Float.ofNat k
+  { minMs := mn, medMs := med, meanMs := mean, sdMs := Float.sqrt var,
+    mbps := (Float.ofNat bytes / 1.0e6) / (mn / 1000.0) }
+
+-- `IO.lazyPure` forces each parse; a pure `act ()` would be hoisted/CSE'd.
+def bench (reps : Nat) (act : Unit → Nat) : IO (Nat × Array Nat) := do
+  let chk ← IO.lazyPure act
+  let mut arr := Array.mkEmpty reps
+  for _ in [0:reps] do
+    let t0 ← IO.monoNanosNow
+    let r ← IO.lazyPure act
+    let t1 ← IO.monoNanosNow
+    if r != chk then throw (IO.userError "nondeterministic checksum")
+    arr := arr.push (t1 - t0)
+  pure (chk, arr)
+
+def prep (name content : String) : IO String := do
+  IO.FS.createDirAll "bench-data"
+  let path := s!"bench-data/{name}.txt"
+  IO.FS.writeFile path content
+  IO.FS.readFile path
+
+def benchOne (name input : String) (reps : Nat) (act : Unit → Nat) : IO (String × Float × Float) := do
+  let (chk, ns) ← bench reps act
+  let s := statsOf ns input.length
+  IO.println s!"  {name} ({input.length}B, chk {chk}): min {r2 s.minMs} / med {r2 s.medMs} ± {r2 s.sdMs} ms  ({r2 s.mbps} MB/s)"
+  pure (name, s.minMs, s.mbps)
+
+def writeTsv (path : String) (rows : Array (String × Float × Float)) : IO Unit :=
+  IO.FS.writeFile path (String.intercalate "\n" (rows.toList.map fun (n, mn, mb) => s!"{n}\t{mn}\t{mb}") ++ "\n")
diff --git a/bench/BenchLp.lean b/bench/BenchLp.lean
new file mode 100644
index 0000000..b4b816d
--- /dev/null
+++ b/bench/BenchLp.lean
@@ -0,0 +1,67 @@
+import Parser
+import BenchGen
+
+-- lean4-parser (`fgdorais/Parser`) baseline: same grammars/inputs as Bench.lean.
+
+open Parser Parser.Char Parser.Char.ASCII
+
+abbrev LP (α) := Parser Unit String.Slice Char α
+
+def runArr (p : LP (Array Nat)) (s : String) : Nat :=
+  match p.run s.toSlice with | .ok _ a => a.foldl (· + ·) 0 | _ => 0
+
+def runChk (p : LP Nat) (s : String) : Nat :=
+  match p.run s.toSlice with | .ok _ a => a | _ => 0
+
+def ws : LP PUnit := Parser.dropMany whitespace
+
+def lpInts : LP (Array Nat) := Parser.sepBy (Parser.token ',') parseNat
+
+def lpCsv : LP Nat :=
+  (fun rows => rows.foldl (fun a r => a + r.size) 0) <$>
+    Parser.sepBy (Parser.token '\n') (Parser.sepBy (Parser.token ',') parseNat)
+
+def lpJson : LP Nat := do
+  let _ ← Parser.token '['
+  let _ ← Parser.sepBy (Parser.token ',') parseNat
+  let _ ← Parser.token ']'
+  pure 1
+
+mutual
+partial def lpSexp : LP Nat := lpList <|> lpAtom
+partial def lpAtom : LP Nat := do
+  let _ ← Parser.takeMany1 alpha; ws; pure 1
+partial def lpList : LP Nat := do
+  let _ ← Parser.token '('; ws
+  let cs ← Parser.takeMany lpSexp
+  let _ ← Parser.token ')'; ws
+  pure (cs.foldl (· + ·) 0)
+end
+
+mutual
+partial def lpLam : LP Nat := lpLamAbs <|> lpVar
+partial def lpVar : LP Nat := do
+  let _ ← Parser.takeMany1 alpha; ws; pure 1
+partial def lpLamAbs : LP Nat := do
+  let _ ← Parser.token '\\'; ws
+  let _ ← Parser.takeMany1 alpha; ws
+  let _ ← Parser.token '.'; ws
+  let b ← lpLam
+  pure (b + 1)
+end
+
+def main : IO Unit := do
+  let reps := 25
+  let intsIn   ← prep "integers" (genInts 20000)
+  let sexpIn   ← prep "sexp"     (genSexp 3 8)
+  let csvIn    ← prep "csv"      (genCsv 4000 6)
+  let jsonIn   ← prep "json"     (genJson 20000)
+  let lambdaIn ← prep "lambda"   (genLambda 2000)
+  IO.println "lean4-parser (fgdorais):"
+  let rows := #[
+    ← benchOne "integers" intsIn   reps (fun _ => runArr lpInts intsIn),
+    ← benchOne "sexp"     sexpIn   reps (fun _ => runChk lpSexp sexpIn),
+    ← benchOne "csv"      csvIn    reps (fun _ => runChk lpCsv csvIn),
+    ← benchOne "json"     jsonIn   reps (fun _ => runChk lpJson jsonIn),
+    ← benchOne "lambda"   lambdaIn reps (fun _ => runChk lpLam lambdaIn)]
+  writeTsv "bench-lp.tsv" rows
diff --git a/bench/lake-manifest.json b/bench/lake-manifest.json
new file mode 100644
index 0000000..028fd38
--- /dev/null
+++ b/bench/lake-manifest.json
@@ -0,0 +1,122 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/fgdorais/lean4-parser",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "d8428e25efb794c9147bb9beac1dfe2e51447c3e",
+   "name": "Parser",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "d8428e25efb794c9147bb9beac1dfe2e51447c3e",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"type": "path",
+   "scope": "",
+   "name": "«prim-parser»",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "../",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "ff04f5c424e50e23476d3539c7c0cc4956e971ad",
+   "name": "UnicodeBasic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "8f9d9cff6bd728b17a24e163c9402775d9e6a365",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.28.0",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "55c8532eb21ec9f6d565d51d96b8ca50bd1fbef3",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "85b59af46828c029a9168f2f9c35119bd0721e6e",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "be3b2e63b1bbf496c478cef98b86972a37c1417d",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.87",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "4f10f47646cb7d5748d6f423f4a07f98f7bbcc9e",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.28.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "«bench-compare»",
+ "lakeDir": ".lake"}
diff --git a/bench/lakefile.toml b/bench/lakefile.toml
new file mode 100644
index 0000000..d10ae0e
--- /dev/null
+++ b/bench/lakefile.toml
@@ -0,0 +1,27 @@
+name = "bench-compare"
+defaultTargets = ["bench", "benchlp"]
+
+[leanOptions]
+pp.unicode.fun = true
+pp.fieldNotation = false
+autoImplicit = false
+
+[[lean_lib]]
+name = "BenchGen"
+
+[[lean_exe]]
+name = "bench"
+root = "Bench"
+
+[[lean_exe]]
+name = "benchlp"
+root = "BenchLp"
+
+[[require]]
+name = "prim-parser"
+path = "../"
+
+[[require]]
+name = "Parser"
+git = "https://github.com/fgdorais/lean4-parser"
+rev = "d8428e25efb794c9147bb9beac1dfe2e51447c3e"