diff --git a/.github/workflows/bar.yml b/.github/workflows/bar.yml
new file mode 100644
index 0000000..32457ed
--- /dev/null
+++ b/.github/workflows/bar.yml
@@ -0,0 +1,21 @@
+name: verified bar
+
+on:
+  push:
+  pull_request:
+  # Rerun when the spec reviewer approves, or an approval is dismissed.
+  pull_request_review:
+    types: [submitted, dismissed]
+
+jobs:
+  bar:
+    # pull-requests: read lets the check confirm the spec approval on GitHub.
+    permissions:
+      contents: read
+      pull-requests: read
+    # Both lines pin the same commit of Proven-Commons/mission: bar v2, as
+    # proposed in its pull request #2. Move both to a release tag once
+    # mission publishes one.
+    uses: Proven-Commons/mission/.github/workflows/verified-bar.yml@6ba85c27abaaf07905c9316aa96dc29f7b5847a2
+    with:
+      bar-ref: 6ba85c27abaaf07905c9316aa96dc29f7b5847a2
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..ae73679
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+.lake/
+__pycache__/
diff --git a/Main.lean b/Main.lean
new file mode 100644
index 0000000..0cf7f43
--- /dev/null
+++ b/Main.lean
@@ -0,0 +1,112 @@
+/-
+  Command line front end, used by the differential tests.
+
+    protowire serve
+
+  answers requests on standard input, one per line:
+
+    decode HEX       prints  OK, then one tab-separated item per field,
+                     NUMBER:KIND:VALUE; or REJECT
+    encode FIELDS    prints  the hex of the encoded message, or INVALID
+                     when a field cannot be written
+
+  KIND is `varint`, `i64`, `len` or `i32`. VALUE is a decimal number of
+  at most 30 digits, or for `len` the bytes in lower case hex (empty for
+  no bytes). FIELDS is NUMBER:KIND:VALUE items separated by commas, or
+  `-` for none. HEX is lower case.
+
+  A malformed request prints `error`: an unknown operation, hex digits
+  that are not lower case or not in pairs, a number of more than 30
+  digits, or a field item that does not parse. A request line may end in
+  LF or CR LF. Each answer is flushed as soon as it is written.
+
+  Every answer comes from the proved functions in `Protobuf/`: `decode`,
+  `encode` and `Field.isValid`. The parsing and printing here are covered
+  by the tests, not by a proof.
+-/
+
+import Protobuf
+
+open Protobuf
+
+def hexValue (c : Char) : Option Nat :=
+  if '0' ≤ c ∧ c ≤ '9' then some (c.toNat - '0'.toNat)
+  else if 'a' ≤ c ∧ c ≤ 'f' then some (c.toNat - 'a'.toNat + 10)
+  else none
+
+def hexBytes : List Char → Option (List UInt8)
+  | [] => some []
+  | a :: b :: rest => do
+    let hi ← hexValue a
+    let lo ← hexValue b
+    let bs ← hexBytes rest
+    pure ((hi * 16 + lo).toUInt8 :: bs)
+  | [_] => none
+
+def hexDigit (n : Nat) : Char := "0123456789abcdef".toList.getD n '?'
+
+def showHex (bs : List UInt8) : String :=
+  String.ofList (bs.flatMap fun b => [hexDigit (b.toNat / 16), hexDigit (b.toNat % 16)])
+
+/-- A number in plain decimal digits, refused past 30 digits so that a
+    huge request cannot make the conversion slow. -/
+def number (t : String) : Option Nat :=
+  let ds := t.toList
+  if ds.isEmpty || !ds.all Char.isDigit || ds.length > 30 then none else t.toNat?
+
+def showField (f : Field) : String :=
+  let (kind, value) := match f.value with
+    | .varint v => ("varint", toString v)
+    | .i64 v => ("i64", toString v)
+    | .len d => ("len", showHex d)
+    | .i32 v => ("i32", toString v)
+  s!"{f.number}:{kind}:{value}"
+
+def readField (item : String) : Option Field :=
+  match item.splitOn ":" with
+  | [n, kind, v] => do
+    let n ← number n
+    match kind with
+    | "varint" => pure ⟨n, .varint (← number v)⟩
+    | "i64" => pure ⟨n, .i64 (← number v)⟩
+    | "len" => pure ⟨n, .len (← hexBytes v.toList)⟩
+    | "i32" => pure ⟨n, .i32 (← number v)⟩
+    | _ => none
+  | _ => none
+
+/-- The answer to one request line, or `none` when it is malformed. -/
+def request (line : String) : Option String :=
+  match line.splitOn " " with
+  | ["decode", h] => do
+    let bs ← hexBytes h.toList
+    pure <| match decode bs with
+      | some fs => "\t".intercalate ("OK" :: fs.map showField)
+      | none => "REJECT"
+  | ["encode", "-"] => pure (showHex (encode []))
+  | ["encode", items] => do
+    let fs ← (items.splitOn ",").mapM readField
+    pure <| if fs.all Field.isValid then showHex (encode fs) else "INVALID"
+  | _ => none
+
+/-- The line without its line ending: LF, or CR LF. -/
+def chomp (line : String) : String :=
+  let cs := line.toList
+  if cs.getLast? = some '\n' then
+    let cs := cs.dropLast
+    String.ofList (if cs.getLast? = some '\r' then cs.dropLast else cs)
+  else line
+
+def main (args : List String) : IO UInt32 := do
+  match args with
+  | ["serve"] =>
+    let stdin ← IO.getStdin
+    let stdout ← IO.getStdout
+    repeat
+      let line ← stdin.getLine
+      if line.isEmpty then break
+      stdout.putStrLn ((request (chomp line)).getD "error")
+      stdout.flush
+    return 0
+  | _ =>
+    IO.eprintln "usage: protowire serve"
+    return 2
diff --git a/Proofs.lean b/Proofs.lean
new file mode 100644
index 0000000..a0c5328
--- /dev/null
+++ b/Proofs.lean
@@ -0,0 +1,7 @@
+/-
+  The proofs, under the names the challenge file gives them. The
+  theorems themselves are in `Proofs/Main.lean`, from the lemmas in the
+  other files.
+-/
+
+import Proofs.Main
diff --git a/Proofs/Fixed.lean b/Proofs/Fixed.lean
new file mode 100644
index 0000000..6a186d8
--- /dev/null
+++ b/Proofs/Fixed.lean
@@ -0,0 +1,105 @@
+/-
+  Fixed-width values: `leValue` and `leBytes` in `Protobuf/Wire.lean`
+  are `Spec.leValue` and `Spec.leBytes`, `Spec.leBytes k n` has `k`
+  bytes, and the two are inverse: reading back `k` bytes of a number
+  below 256^k gives the number, and writing the value of a list of bytes
+  in as many bytes gives the list.
+-/
+
+import Protobuf
+import Spec.Defs
+
+namespace Protobuf.Proofs.Fixed
+
+open Protobuf
+
+/-! ## Cons formulas for the spec -/
+
+theorem sum_map_mul_left (l : List Nat) (g : Nat → Nat) (c : Nat) :
+    (l.map fun i => c * g i).sum = c * (l.map g).sum := by
+  induction l with
+  | nil => simp
+  | cons x xs ih => simp [List.sum_cons, ih, Nat.mul_add]
+
+theorem spec_leValue_nil : Spec.leValue [] = 0 := rfl
+
+theorem spec_leValue_cons (b : UInt8) (bs : List UInt8) :
+    Spec.leValue (b :: bs) = b.toNat + 256 * Spec.leValue bs := by
+  unfold Spec.leValue
+  rw [List.length_cons, List.range_succ_eq_map, List.map_cons, List.sum_cons, List.map_map]
+  have : ((fun i => ((b :: bs).getD i 0).toNat * 256 ^ i) ∘ Nat.succ) =
+      fun i => 256 * ((bs.getD i 0).toNat * 256 ^ i) := by
+    funext i
+    simp [Nat.pow_succ', Nat.mul_left_comm]
+  rw [this, sum_map_mul_left]
+  simp
+
+theorem spec_leBytes_zero (n : Nat) : Spec.leBytes 0 n = [] := rfl
+
+theorem spec_leBytes_succ (k n : Nat) :
+    Spec.leBytes (k + 1) n = (n % 256).toUInt8 :: Spec.leBytes k (n / 256) := by
+  unfold Spec.leBytes
+  rw [List.range_succ_eq_map, List.map_cons, List.map_map]
+  congr 1
+  · simp
+  · apply List.map_congr_left
+    intro i _
+    simp [Nat.pow_succ', Nat.div_div_eq_div_mul]
+
+/-! ## The code is the spec -/
+
+theorem leValue_cons (b : UInt8) (bs : List UInt8) :
+    leValue (b :: bs) = b.toNat + 256 * leValue bs := rfl
+
+theorem leValue_eq (bs : List UInt8) : leValue bs = Spec.leValue bs := by
+  induction bs with
+  | nil => rfl
+  | cons b bs ih => rw [leValue_cons, spec_leValue_cons, ih]
+
+theorem leBytes_eq (k n : Nat) : leBytes k n = Spec.leBytes k n := by
+  induction k generalizing n with
+  | zero => rfl
+  | succ k ih => rw [spec_leBytes_succ, ← ih]; rfl
+
+/-! ## Length, bounds and inverses -/
+
+theorem leBytes_length (k n : Nat) : (Spec.leBytes k n).length = k := by
+  simp [Spec.leBytes]
+
+theorem toNat_lt (b : UInt8) : b.toNat < 256 := UInt8.toNat_lt b
+
+theorem leValue_leBytes (k n : Nat) (h : n < 256 ^ k) : Spec.leValue (Spec.leBytes k n) = n := by
+  induction k generalizing n with
+  | zero =>
+    simp at h
+    subst h
+    rfl
+  | succ k ih =>
+    have hd : n / 256 < 256 ^ k := by
+      rw [Nat.div_lt_iff_lt_mul (by decide), ← Nat.pow_succ]
+      exact h
+    rw [spec_leBytes_succ, spec_leValue_cons, ih _ hd]
+    have : (n % 256).toUInt8.toNat = n % 256 := by simp
+    rw [this]
+    exact Nat.mod_add_div n 256
+
+theorem leValue_lt (bs : List UInt8) : Spec.leValue bs < 256 ^ bs.length := by
+  induction bs with
+  | nil => simp [spec_leValue_nil]
+  | cons b bs ih =>
+    rw [spec_leValue_cons, List.length_cons, Nat.pow_succ']
+    have := toNat_lt b
+    omega
+
+theorem leBytes_leValue (bs : List UInt8) : Spec.leBytes bs.length (Spec.leValue bs) = bs := by
+  induction bs with
+  | nil => rfl
+  | cons b bs ih =>
+    have hb := toNat_lt b
+    rw [List.length_cons, spec_leBytes_succ, spec_leValue_cons]
+    have hm : (b.toNat + 256 * Spec.leValue bs) % 256 = b.toNat := by omega
+    have hd : (b.toNat + 256 * Spec.leValue bs) / 256 = Spec.leValue bs := by omega
+    rw [hm, hd, ih]
+    simp
+
+end Protobuf.Proofs.Fixed
diff --git a/Proofs/Main.lean b/Proofs/Main.lean
new file mode 100644
index 0000000..e68bf18
--- /dev/null
+++ b/Proofs/Main.lean
@@ -0,0 +1,87 @@
+/-
+  The statements of `Spec.lean`, under the same names, from the lemmas
+  in the other files of `Proofs/`. The test vectors are checked by
+  evaluation.
+-/
+
+import Protobuf
+import Spec.Defs
+import Proofs.Varint
+import Proofs.Message
+
+open Protobuf
+open Protobuf.Proofs
+
+theorem Spec.varint_encode_eq (n : Nat) (h : n < 2 ^ 64) : Varint.encode n = Spec.varint n :=
+  Protobuf.Proofs.Varint.encode_eq n h
+
+theorem Spec.varint_decode_iff (bs : List UInt8) (v : Nat) (rest : List UInt8) :
+    Varint.decode bs = some (v, rest) ↔ ∃ pre, bs = pre ++ rest ∧ Spec.IsVarint pre v :=
+  Protobuf.Proofs.Varint.decode_iff bs v rest
+
+theorem Spec.varint_decode_encode (n : Nat) (rest : List UInt8) (h : n < 2 ^ 64) :
+    Varint.decode (Varint.encode n ++ rest) = some (n, rest) :=
+  Protobuf.Proofs.Varint.decode_encode n rest h
+
+theorem Spec.isValid_iff (f : Field) : f.isValid = true ↔ Spec.ValidField f :=
+  Protobuf.Proofs.Message.isValid_iff f
+
+theorem Spec.encode_eq (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) :
+    Protobuf.encode fs = Spec.encode fs :=
+  Protobuf.Proofs.Message.encode_eq fs h
+
+theorem Spec.decode_iff (bs : List UInt8) (fs : List Field) :
+    decode bs = some fs ↔ Spec.Message bs fs :=
+  Protobuf.Proofs.Message.decode_iff bs fs
+
+theorem Spec.decode_encode (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) :
+    decode (Protobuf.encode fs) = some fs :=
+  Protobuf.Proofs.Message.decode_encode fs h
+
+theorem Spec.decode_valid (bs : List UInt8) (fs : List Field) (h : decode bs = some fs) :
+    ∀ f ∈ fs, Spec.ValidField f :=
+  Protobuf.Proofs.Message.decode_valid bs fs h
+
+theorem Spec.guide_vectors :
+    Varint.encode 1 = [0x01] ∧
+    Varint.encode 150 = [0x96, 0x01] ∧
+    Varint.encode (2 ^ 64 - 2) = [0xfe, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0x01] ∧
+    decode [0x08, 0x96, 0x01] = some [⟨1, .varint 150⟩] ∧
+    decode [0x12, 0x07, 0x74, 0x65, 0x73, 0x74, 0x69, 0x6e, 0x67] =
+      some [⟨2, .len [0x74, 0x65, 0x73, 0x74, 0x69, 0x6e, 0x67]⟩] ∧
+    decode [0x1a, 0x03, 0x08, 0x96, 0x01] = some [⟨3, .len [0x08, 0x96, 0x01]⟩] ∧
+    decode [0x22, 0x05, 0x68, 0x65, 0x6c, 0x6c, 0x6f, 0x2a, 0x03, 0x01, 0x02, 0x03] =
+      some [⟨4, .len [0x68, 0x65, 0x6c, 0x6c, 0x6f]⟩, ⟨5, .len [0x01, 0x02, 0x03]⟩] ∧
+    Protobuf.encode [⟨1, .varint 150⟩, ⟨2, .len [0x74, 0x65, 0x73, 0x74, 0x69, 0x6e, 0x67]⟩] =
+      [0x08, 0x96, 0x01, 0x12, 0x07, 0x74, 0x65, 0x73, 0x74, 0x69, 0x6e, 0x67] := by
+  decide
+
+theorem Spec.edge_vectors :
+    Varint.encode (2 ^ 64 - 1) = [0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0x01] ∧
+    decode [0x0d, 0x01, 0x02, 0x03, 0x04] = some [⟨1, .i32 0x04030201⟩] ∧
+    decode [0x09, 0x01, 0x02, 0x03, 0x04, 0x05, 0x06, 0x07, 0x08] =
+      some [⟨1, .i64 0x0807060504030201⟩] ∧
+    decode [0x08, 0x80, 0x00] = some [⟨1, .varint 0⟩] ∧
+    decode [0x08, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0x7f] =
+      some [⟨1, .varint (2 ^ 64 - 1)⟩] ∧
+    decode [0xf8, 0xff, 0xff, 0xff, 0x0f, 0x01] = some [⟨2 ^ 29 - 1, .varint 1⟩] ∧
+    decode [] = some [] := by
+  decide
+
+theorem Spec.reject_vectors :
+    decode [0x08] = none ∧
+    decode [0x08, 0x80] = none ∧
+    decode [0x08, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x00] = none ∧
+    decode [0x00, 0x00] = none ∧
+    decode [0x0a, 0x04, 0x61, 0x62] = none ∧
+    decode [0x0d, 0x01, 0x02, 0x03] = none ∧
+    decode [0x09, 0x01, 0x02, 0x03, 0x04, 0x05, 0x06, 0x07] = none ∧
+    decode [0x0b, 0x0c] = none ∧
+    decode [0x0c] = none ∧
+    decode [0x0e, 0x00] = none ∧
+    decode [0x0f, 0x00] = none ∧
+    decode [0xf8, 0xff, 0xff, 0xff, 0x1f, 0x01] = none ∧
+    decode [0x80, 0x80, 0x80, 0x80, 0x10, 0x01] = none ∧
+    decode [0x88, 0x80, 0x80, 0x80, 0x80, 0x00, 0x01] = none ∧
+    decode [0x0a, 0x81, 0x80, 0x80, 0x80, 0x80, 0x00, 0x61] = none := by
+  decide
diff --git a/Proofs/Message.lean b/Proofs/Message.lean
new file mode 100644
index 0000000..cb65b96
--- /dev/null
+++ b/Proofs/Message.lean
@@ -0,0 +1,348 @@
+/-
+  Fields and messages against the spec: `Field.isValid` decides
+  `Spec.ValidField`, the encoder writes `Spec.encode`, `decodeField`
+  reads exactly one record (`Spec.FieldBytes`) from the front of its
+  input, `decode` reads exactly a `Spec.Message`, decoding what the
+  encoder wrote gives the fields back, and every field the decoder
+  returns is valid.
+-/
+
+import Protobuf
+import Spec.Defs
+import Proofs.Varint
+import Proofs.Fixed
+
+namespace Protobuf.Proofs.Message
+
+open Protobuf
+
+/-! ## Validity -/
+
+theorem isValid_iff (f : Field) : f.isValid = true ↔ Spec.ValidField f := by
+  obtain ⟨n, v⟩ := f
+  cases v <;> simp [Field.isValid, Spec.ValidField, and_assoc]
+
+/-! ## The encoder -/
+
+theorem field_encode_eq (f : Field) (h : Spec.ValidField f) : f.encode = Spec.fieldBytes f := by
+  obtain ⟨n, v⟩ := f
+  obtain ⟨h1, h2, h3⟩ := h
+  have h2 : n < 2 ^ 29 := h2
+  have hn : ∀ w, w < 8 → n * 8 + w < 2 ^ 64 := by intro w hw; omega
+  cases v with
+  | varint v =>
+    have h3 : v < 2 ^ 64 := h3
+    show Varint.encode (n * 8 + 0) ++ Varint.encode v = Spec.varint (n * 8 + 0) ++ Spec.varint v
+    rw [Proofs.Varint.encode_eq _ (hn 0 (by decide)), Proofs.Varint.encode_eq _ h3]
+  | i64 v =>
+    show Varint.encode (n * 8 + 1) ++ leBytes 8 v = Spec.varint (n * 8 + 1) ++ Spec.leBytes 8 v
+    rw [Proofs.Varint.encode_eq _ (hn 1 (by decide)), Proofs.Fixed.leBytes_eq]
+  | len d =>
+    have h3 : d.length < 2 ^ 31 - 16 := h3
+    show Varint.encode (n * 8 + 2) ++ (Varint.encode d.length ++ d) =
+      Spec.varint (n * 8 + 2) ++ Spec.varint d.length ++ d
+    rw [Proofs.Varint.encode_eq _ (hn 2 (by decide)), Proofs.Varint.encode_eq _ (by omega),
+      List.append_assoc]
+  | i32 v =>
+    show Varint.encode (n * 8 + 5) ++ leBytes 4 v = Spec.varint (n * 8 + 5) ++ Spec.leBytes 4 v
+    rw [Proofs.Varint.encode_eq _ (hn 5 (by decide)), Proofs.Fixed.leBytes_eq]
+
+theorem encode_cons (f : Field) (fs : List Field) : encode (f :: fs) = f.encode ++ encode fs := by
+  simp [encode]
+
+theorem spec_encode_cons (f : Field) (fs : List Field) :
+    Spec.encode (f :: fs) = Spec.fieldBytes f ++ Spec.encode fs := by
+  simp [Spec.encode]
+
+theorem encode_eq (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) : encode fs = Spec.encode fs := by
+  induction fs with
+  | nil => rfl
+  | cons f fs ih =>
+    rw [encode_cons, spec_encode_cons, field_encode_eq f (h f (by simp)),
+      ih (fun g hg => h g (by simp [hg]))]
+
+/-! ## One record -/
+
+/-- The length checks in `decodeField` look at no more than `k` bytes. -/
+theorem take_short (l : List UInt8) (k : Nat) : ((l.take k).length < k) = (l.length < k) := by
+  simp only [List.length_take]
+  apply propext
+  omega
+
+theorem decodeField_iff (bs : List UInt8) (f : Field) (rest : List UInt8) :
+    decodeField bs = some (f, rest) ↔
+      ∃ tag payload, bs = tag ++ payload ++ rest ∧ Spec.FieldBytes tag payload f := by
+  constructor
+  · intro h
+    unfold decodeField at h
+    simp only [take_short] at h
+    cases ht : Varint.decodeAux 5 bs with
+    | none => rw [ht] at h; exact absurd h (by simp)
+    | some p =>
+      obtain ⟨t, r⟩ := p
+      obtain ⟨tag, hbs, hshape, hg⟩ := (Proofs.Varint.decodeAux_iff 5 bs t r).mp ht
+      rw [ht] at h
+      simp only at h
+      by_cases hc : 2 ^ 32 ≤ t ∨ t / 8 = 0
+      · simp only [hc, ↓reduceIte] at h
+        exact absurd h (by simp)
+      · simp only [hc, ↓reduceIte] at h
+        have ht32 : t < 2 ^ 32 := by omega
+        have hn : 1 ≤ t / 8 := by omega
+        subst hbs
+        subst hg
+        split at h
+        · rename_i hw
+          split at h
+          · rename_i v r' hv
+            simp only [Option.some.injEq, Prod.mk.injEq] at h
+            obtain ⟨rfl, rfl⟩ := h
+            obtain ⟨pre, hr, hiv⟩ := (Proofs.Varint.decode_iff r v r').mp hv
+            refine ⟨tag, pre, by rw [hr, List.append_assoc], hshape, ht32, rfl, hn, ?_⟩
+            rw [hw]
+            exact hiv
+          · exact absurd h (by simp)
+        · rename_i hw
+          by_cases hl : r.length < 8
+          · simp only [hl, ↓reduceIte] at h
+            exact absurd h (by simp)
+          · simp only [hl, ↓reduceIte, Option.some.injEq, Prod.mk.injEq] at h
+            obtain ⟨rfl, rfl⟩ := h
+            refine ⟨tag, r.take 8, by rw [List.append_assoc, List.take_append_drop], hshape, ht32,
+              rfl, hn, ?_⟩
+            rw [hw]
+            exact ⟨by simp; omega, Proofs.Fixed.leValue_eq _⟩
+        · rename_i hw
+          split at h
+          · rename_i len r2 hv
+            obtain ⟨pre, hr, hps, hpv⟩ := (Proofs.Varint.decodeAux_iff 5 r len r2).mp hv
+            by_cases hl : 2 ^ 31 - 16 ≤ len ∨ r2.length < len
+            · simp only [hl, ↓reduceIte] at h
+              exact absurd h (by simp)
+            · simp only [hl, ↓reduceIte, Option.some.injEq, Prod.mk.injEq] at h
+              obtain ⟨rfl, rfl⟩ := h
+              have hlen : (r2.take len).length = len := by simp; omega
+              refine ⟨tag, pre ++ r2.take len, ?_, hshape, ht32, rfl, hn, ?_⟩
+              · rw [hr, List.append_assoc, List.append_assoc, List.take_append_drop]
+              · rw [hw]
+                exact ⟨pre, rfl, hps, by rw [hlen, hpv], by rw [hlen]; omega⟩
+          · exact absurd h (by simp)
+        · rename_i hw
+          by_cases hl : r.length < 4
+          · simp only [hl, ↓reduceIte] at h
+            exact absurd h (by simp)
+          · simp only [hl, ↓reduceIte, Option.some.injEq, Prod.mk.injEq] at h
+            obtain ⟨rfl, rfl⟩ := h
+            refine ⟨tag, r.take 4, by rw [List.append_assoc, List.take_append_drop], hshape, ht32,
+              rfl, hn, ?_⟩
+            rw [hw]
+            exact ⟨by simp; omega, Proofs.Fixed.leValue_eq _⟩
+        · exact absurd h (by simp)
+  · rintro ⟨tag, payload, rfl, hshape, ht32, hnum, hn, hm⟩
+    obtain ⟨num, val⟩ := f
+    have hd : Varint.decodeAux 5 (tag ++ payload ++ rest) =
+        some (Spec.groupsValue tag, payload ++ rest) :=
+      (Proofs.Varint.decodeAux_iff 5 _ _ _).mpr ⟨tag, List.append_assoc _ _ _, hshape, rfl⟩
+    have hc : ¬(2 ^ 32 ≤ Spec.groupsValue tag ∨ Spec.groupsValue tag / 8 = 0) := by
+      simp only at hnum hn
+      omega
+    have hnum' : num = Spec.groupsValue tag / 8 := hnum
+    unfold decodeField
+    simp only [take_short]
+    rw [hd]
+    simp only [hc, ↓reduceIte]
+    simp only at hm
+    split at hm
+    · rename_i v hw
+      rw [hw]
+      simp only
+      rw [(Proofs.Varint.decode_iff _ v rest).mpr ⟨payload, rfl, hm⟩, hnum']
+    · rename_i v hw
+      obtain ⟨hl, rfl⟩ := hm
+      have hl' : ¬(payload ++ rest).length < 8 := by simp; omega
+      rw [hw]
+      simp only [hl', ↓reduceIte]
+      rw [List.take_left' hl, List.drop_left' hl, Proofs.Fixed.leValue_eq, hnum']
+    · rename_i d hw
+      obtain ⟨pre, rfl, hps, hpv, hdl⟩ := hm
+      have hd2 : Varint.decodeAux 5 (pre ++ d ++ rest) = some (d.length, d ++ rest) :=
+        (Proofs.Varint.decodeAux_iff 5 _ _ _).mpr ⟨pre, List.append_assoc _ _ _, hps, hpv.symm⟩
+      have hl' : ¬(2 ^ 31 - 16 ≤ d.length ∨ (d ++ rest).length < d.length) := by simp; omega
+      rw [hw]
+      simp only
+      rw [hd2]
+      simp only [hl', ↓reduceIte]
+      rw [List.take_left' rfl, List.drop_left' rfl, hnum']
+    · rename_i v hw
+      obtain ⟨hl, rfl⟩ := hm
+      have hl' : ¬(payload ++ rest).length < 4 := by simp; omega
+      rw [hw]
+      simp only [hl', ↓reduceIte]
+      rw [List.take_left' hl, List.drop_left' hl, Proofs.Fixed.leValue_eq, hnum']
+    · exact hm.elim
+
+/-! ## Messages -/
+
+/-- Whatever `decodeAux` returns, with any fuel, is a message. -/
+theorem decodeAux_sound (fuel : Nat) :
+    ∀ bs fs, decodeAux fuel bs = some fs → Spec.Message bs fs := by
+  induction fuel with
+  | zero =>
+    intro bs fs h
+    cases bs with
+    | nil =>
+      simp only [decodeAux, Option.some.injEq] at h
+      subst h
+      exact .nil
+    | cons b bs => simp [decodeAux] at h
+  | succ fuel ih =>
+    intro bs fs h
+    cases bs with
+    | nil =>
+      simp only [decodeAux, Option.some.injEq] at h
+      subst h
+      exact .nil
+    | cons b bs =>
+      simp only [decodeAux] at h
+      split at h
+      · rename_i f rest hf
+        split at h
+        · rename_i fs' hfs
+          simp only [Option.some.injEq] at h
+          subst h
+          obtain ⟨tag, payload, hbs, hfb⟩ := (decodeField_iff _ f rest).mp hf
+          rw [hbs]
+          exact .cons hfb (ih rest fs' hfs)
+        · exact absurd h (by simp)
+      · exact absurd h (by simp)
+
+/-- A message is read whole by `decodeAux` with fuel at least its length:
+    each record takes at least one byte, since its tag does. -/
+theorem decodeAux_complete {bs : List UInt8} {fs : List Field} (h : Spec.Message bs fs) :
+    ∀ fuel, bs.length ≤ fuel → decodeAux fuel bs = some fs := by
+  induction h with
+  | nil => intro fuel _; cases fuel <;> rfl
+  | @cons tag payload rest f fs hfb _ ih =>
+    intro fuel hlen
+    obtain ⟨c, tag', rfl⟩ : ∃ c tag', tag = c :: tag' := by
+      cases tag with
+      | nil => exact absurd rfl hfb.1.1
+      | cons c tag' => exact ⟨c, tag', rfl⟩
+    simp only [List.cons_append, List.length_cons, List.length_append] at hlen ⊢
+    obtain ⟨fuel', rfl⟩ : ∃ k, fuel = k + 1 := ⟨fuel - 1, by omega⟩
+    have hd : decodeField (c :: (tag' ++ payload ++ rest)) = some (f, rest) :=
+      (decodeField_iff _ f rest).mpr ⟨c :: tag', payload, rfl, hfb⟩
+    simp only [decodeAux, hd]
+    rw [ih fuel' (by omega)]
+
+theorem decode_iff (bs : List UInt8) (fs : List Field) : decode bs = some fs ↔ Spec.Message bs fs :=
+  ⟨decodeAux_sound bs.length bs fs, fun h => decodeAux_complete h bs.length (Nat.le_refl _)⟩
+
+/-! ## Decoded fields are valid -/
+
+theorem fieldBytes_valid {tag payload : List UInt8} {f : Field} (h : Spec.FieldBytes tag payload f) :
+    Spec.ValidField f := by
+  obtain ⟨num, val⟩ := f
+  obtain ⟨_, ht, hnum, hn, hm⟩ := h
+  simp only at hnum hn hm
+  refine ⟨hn, show num < 2 ^ 29 by omega, ?_⟩
+  simp only
+  split at hm
+  · obtain ⟨_, rfl⟩ := hm
+    exact Nat.mod_lt _ (by decide)
+  · obtain ⟨hl, rfl⟩ := hm
+    have := Proofs.Fixed.leValue_lt payload
+    rw [hl] at this
+    exact this
+  · obtain ⟨_, _, _, _, hdl⟩ := hm
+    exact hdl
+  · obtain ⟨hl, rfl⟩ := hm
+    have := Proofs.Fixed.leValue_lt payload
+    rw [hl] at this
+    exact this
+  · exact hm.elim
+
+theorem message_valid {bs : List UInt8} {fs : List Field} (h : Spec.Message bs fs) :
+    ∀ f ∈ fs, Spec.ValidField f := by
+  induction h with
+  | nil => simp
+  | cons hfb _ ih =>
+    intro g hg
+    rcases List.mem_cons.mp hg with rfl | hg
+    · exact fieldBytes_valid hfb
+    · exact ih g hg
+
+theorem decode_valid (bs : List UInt8) (fs : List Field) (h : decode bs = some fs) :
+    ∀ f ∈ fs, Spec.ValidField f :=
+  message_valid ((decode_iff bs fs).mp h)
+
+/-! ## Round trip -/
+
+/-- The shortest varint of a valid tag has at most five bytes. -/
+theorem tag_bytes (n w : Nat) (hn : n < 2 ^ 29) (hw : w < 8) :
+    Spec.VarintShape 5 (Spec.varint (n * 8 + w)) ∧ Spec.groupsValue (Spec.varint (n * 8 + w)) = n * 8 + w := by
+  have hs := Proofs.Varint.varint_shape (n * 8 + w)
+  have h5 : (2 : Nat) ^ 32 ≤ 128 ^ 5 := by decide
+  exact ⟨Proofs.Varint.shape_mono hs.1 (Proofs.Varint.varint_length _ 5 (by decide) (by omega)), hs.2⟩
+
+/-- The bytes the encoder writes for a valid field are one record. -/
+theorem fieldBytes_split (f : Field) (h : Spec.ValidField f) :
+    ∃ tag payload, Spec.fieldBytes f = tag ++ payload ∧ Spec.FieldBytes tag payload f := by
+  obtain ⟨n, val⟩ := f
+  obtain ⟨h1, h2, h3⟩ := h
+  have h1 : 1 ≤ n := h1
+  have h2 : n < 2 ^ 29 := h2
+  cases val with
+  | varint v =>
+    have h3 : v < 2 ^ 64 := h3
+    obtain ⟨hs, hg⟩ := tag_bytes n 0 h2 (by decide)
+    refine ⟨Spec.varint (n * 8 + 0), Spec.varint v, rfl, hs, by rw [hg]; omega,
+      show n = _ by rw [hg]; omega, h1, ?_⟩
+    rw [hg, show (n * 8 + 0) % 8 = 0 by omega]
+    have hv := Proofs.Varint.varint_shape v
+    exact ⟨Proofs.Varint.shape_mono hv.1
+      (Proofs.Varint.varint_length v 10 (by decide) (Nat.lt_of_lt_of_le h3 Proofs.Varint.two_pow_le)),
+      by rw [hv.2, Nat.mod_eq_of_lt h3]⟩
+  | i64 v =>
+    have h3 : v < 2 ^ 64 := h3
+    obtain ⟨hs, hg⟩ := tag_bytes n 1 h2 (by decide)
+    refine ⟨Spec.varint (n * 8 + 1), Spec.leBytes 8 v, rfl, hs, by rw [hg]; omega,
+      show n = _ by rw [hg]; omega, h1, ?_⟩
+    rw [hg, show (n * 8 + 1) % 8 = 1 by omega]
+    exact ⟨Proofs.Fixed.leBytes_length 8 v,
+      (Proofs.Fixed.leValue_leBytes 8 v (by simpa using h3)).symm⟩
+  | len d =>
+    have h3 : d.length < 2 ^ 31 - 16 := h3
+    obtain ⟨hs, hg⟩ := tag_bytes n 2 h2 (by decide)
+    refine ⟨Spec.varint (n * 8 + 2), Spec.varint d.length ++ d, List.append_assoc _ _ _, hs,
+      by rw [hg]; omega, show n = _ by rw [hg]; omega, h1, ?_⟩
+    rw [hg, show (n * 8 + 2) % 8 = 2 by omega]
+    have hv := Proofs.Varint.varint_shape d.length
+    have h5 : (2 : Nat) ^ 31 ≤ 128 ^ 5 := by decide
+    exact ⟨Spec.varint d.length, rfl,
+      Proofs.Varint.shape_mono hv.1 (Proofs.Varint.varint_length _ 5 (by decide) (by omega)),
+      hv.2, h3⟩
+  | i32 v =>
+    have h3 : v < 2 ^ 32 := h3
+    obtain ⟨hs, hg⟩ := tag_bytes n 5 h2 (by decide)
+    refine ⟨Spec.varint (n * 8 + 5), Spec.leBytes 4 v, rfl, hs, by rw [hg]; omega,
+      show n = _ by rw [hg]; omega, h1, ?_⟩
+    rw [hg, show (n * 8 + 5) % 8 = 5 by omega]
+    exact ⟨Proofs.Fixed.leBytes_length 4 v,
+      (Proofs.Fixed.leValue_leBytes 4 v (by simpa using h3)).symm⟩
+
+theorem encode_message (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) :
+    Spec.Message (Spec.encode fs) fs := by
+  induction fs with
+  | nil => exact .nil
+  | cons f fs ih =>
+    obtain ⟨tag, payload, he, hfb⟩ := fieldBytes_split f (h f (by simp))
+    rw [spec_encode_cons, he]
+    exact .cons hfb (ih fun g hg => h g (by simp [hg]))
+
+theorem decode_encode (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) :
+    decode (encode fs) = some fs := by
+  rw [encode_eq fs h]
+  exact (decode_iff _ _).mpr (encode_message fs h)
+
+end Protobuf.Proofs.Message
diff --git a/Proofs/Varint.lean b/Proofs/Varint.lean
new file mode 100644
index 0000000..19655d5
--- /dev/null
+++ b/Proofs/Varint.lean
@@ -0,0 +1,288 @@
+/-
+  The varint encoder and decoder of `Protobuf/Varint.lean` against the
+  spec: `encode` writes `Spec.varint`, `decodeAux k` reads exactly one
+  varint of at most `k` bytes (shape `Spec.VarintShape k`, value
+  `Spec.groupsValue`), `decode` reads exactly a `Spec.IsVarint`, and
+  decoding what the encoder wrote gives the number back.
+-/
+
+import Protobuf
+import Spec.Defs
+
+namespace Protobuf.Proofs.Varint
+
+open Protobuf
+
+/-! ## Groups and shapes, one byte at a time -/
+
+theorem sum_map_mul (c : Nat) (g : Nat → Nat) (l : List Nat) :
+    (l.map fun i => c * g i).sum = c * (l.map g).sum := by
+  induction l with
+  | nil => simp
+  | cons a l ih => simp [List.sum_cons, ih, Nat.mul_add]
+
+theorem groupsValue_nil : Spec.groupsValue [] = 0 := rfl
+
+theorem groupsValue_cons (b : UInt8) (bs : List UInt8) :
+    Spec.groupsValue (b :: bs) = b.toNat % 128 + 128 * Spec.groupsValue bs := by
+  unfold Spec.groupsValue
+  rw [List.length_cons, List.range_succ_eq_map, List.map_cons, List.sum_cons, List.map_map,
+    ← sum_map_mul]
+  congr 1
+  · simp
+  · congr 1
+    apply List.map_congr_left
+    intro i _
+    simp only [Function.comp, Nat.succ_eq_add_one, List.getD_cons_succ, Nat.pow_succ]
+    rw [Nat.mul_comm (128 ^ i) 128, Nat.mul_left_comm]
+
+theorem shape_zero (bs : List UInt8) : ¬ Spec.VarintShape 0 bs := by
+  intro ⟨h1, h2, _⟩
+  exact h1 (List.eq_nil_of_length_eq_zero (Nat.le_zero.mp h2))
+
+theorem shape_nil (k : Nat) : ¬ Spec.VarintShape k [] := fun h => h.1 rfl
+
+theorem shape_cons (k : Nat) (b : UInt8) (bs : List UInt8) :
+    Spec.VarintShape (k + 1) (b :: bs) ↔
+      (b.toNat < 128 ∧ bs = []) ∨ (128 ≤ b.toNat ∧ Spec.VarintShape k bs) := by
+  cases bs with
+  | nil =>
+    simp [Spec.VarintShape]
+  | cons c cs =>
+    simp [Spec.VarintShape, List.dropLast_cons_cons, List.getLast?_cons_cons]
+    exact ⟨fun ⟨h1, ⟨h2, h3⟩, h4⟩ => ⟨h2, h1, h3, h4⟩, fun ⟨h2, h1, h3, h4⟩ => ⟨h1, ⟨h2, h3⟩, h4⟩⟩
+
+
+/-! ## The decoder -/
+
+/-- The right-hand side of `decodeAux_iff` at `k + 1`, one byte at a time. -/
+theorem split_cons (k : Nat) (b : UInt8) (bs : List UInt8) (v : Nat) (rest : List UInt8) :
+    (∃ pre, b :: bs = pre ++ rest ∧ Spec.VarintShape (k + 1) pre ∧ v = Spec.groupsValue pre) ↔
+      (b.toNat < 128 ∧ bs = rest ∧ v = b.toNat) ∨
+      (128 ≤ b.toNat ∧ ∃ v', (∃ pre, bs = pre ++ rest ∧ Spec.VarintShape k pre ∧
+        v' = Spec.groupsValue pre) ∧ v = b.toNat % 128 + 128 * v') := by
+  constructor
+  · rintro ⟨pre, h, hs, hv⟩
+    cases pre with
+    | nil => exact absurd hs (shape_nil _)
+    | cons c pre =>
+      simp only [List.cons_append, List.cons.injEq] at h
+      obtain ⟨hbc, rfl⟩ := h
+      rw [← hbc] at hs hv
+      rcases (shape_cons k b pre).mp hs with ⟨hc, rfl⟩ | ⟨hc, hs'⟩
+      · left
+        refine ⟨hc, by simp, ?_⟩
+        rw [hv, groupsValue_cons, groupsValue_nil]
+        omega
+      · right
+        exact ⟨hc, _, ⟨pre, rfl, hs', rfl⟩, by rw [hv, groupsValue_cons]⟩
+  · rintro (⟨hc, rfl, rfl⟩ | ⟨hc, v', ⟨pre, rfl, hs, rfl⟩, rfl⟩)
+    · refine ⟨[b], rfl, (shape_cons k b []).mpr (Or.inl ⟨hc, rfl⟩), ?_⟩
+      rw [groupsValue_cons, groupsValue_nil]
+      omega
+    · exact ⟨b :: pre, rfl, (shape_cons k b pre).mpr (Or.inr ⟨hc, hs⟩), by rw [groupsValue_cons]⟩
+
+theorem decodeAux_iff (k : Nat) (bs : List UInt8) (v : Nat) (rest : List UInt8) :
+    Varint.decodeAux k bs = some (v, rest) ↔
+      ∃ pre, bs = pre ++ rest ∧ Spec.VarintShape k pre ∧ v = Spec.groupsValue pre := by
+  induction k generalizing bs v with
+  | zero =>
+    simp only [Varint.decodeAux, reduceCtorEq, false_iff, not_exists, not_and]
+    intro pre _ h
+    exact absurd h (shape_zero pre)
+  | succ k ih =>
+    cases bs with
+    | nil =>
+      simp only [Varint.decodeAux, reduceCtorEq, false_iff, not_exists, not_and]
+      intro pre h hs _
+      have : pre = [] := (List.append_eq_nil_iff.mp h.symm).1
+      subst this
+      exact shape_nil _ hs
+    | cons b bs =>
+      have hb := UInt8.toNat_lt b
+      rw [split_cons]
+      simp only [← ih]
+      simp only [Varint.decodeAux]
+      by_cases hc : b.toNat < 128
+      · have hc' : ¬ 128 ≤ b.toNat := by omega
+        simp only [hc, hc', ite_true, false_and, or_false, Option.some.injEq, Prod.mk.injEq,
+          true_and]
+        exact ⟨fun ⟨h1, h2⟩ => ⟨h2, h1.symm⟩, fun ⟨h1, h2⟩ => ⟨h2.symm, h1⟩⟩
+      · cases h : Varint.decodeAux k bs with
+        | none => simp [hc]
+        | some p =>
+          obtain ⟨v0, r0⟩ := p
+          have hc' : 128 ≤ b.toNat := by omega
+          simp only [hc, hc', ite_false, Option.some.injEq, Prod.mk.injEq, true_and, false_and,
+            false_or]
+          constructor
+          · rintro ⟨h1, h2⟩
+            exact ⟨v0, ⟨rfl, h2⟩, by omega⟩
+          · rintro ⟨v', ⟨rfl, h2⟩, h3⟩
+            exact ⟨by omega, h2⟩
+
+
+theorem decode_iff (bs : List UInt8) (v : Nat) (rest : List UInt8) :
+    Varint.decode bs = some (v, rest) ↔ ∃ pre, bs = pre ++ rest ∧ Spec.IsVarint pre v := by
+  unfold Varint.decode
+  cases h : Varint.decodeAux 10 bs with
+  | none =>
+    simp only [reduceCtorEq, false_iff, not_exists, not_and]
+    intro pre hbs ⟨hs, _⟩
+    have h2 := (decodeAux_iff 10 bs _ rest).mpr ⟨pre, hbs, hs, rfl⟩
+    rw [h] at h2
+    exact absurd h2 (by simp)
+  | some p =>
+    obtain ⟨v0, r0⟩ := p
+    obtain ⟨pre0, hbs0, hs0, hv0⟩ := (decodeAux_iff 10 bs v0 r0).mp h
+    simp only [Option.some.injEq, Prod.mk.injEq]
+    constructor
+    · rintro ⟨rfl, rfl⟩
+      exact ⟨pre0, hbs0, hs0, by rw [hv0]⟩
+    · rintro ⟨pre, hbs, hs, hv⟩
+      have h2 := (decodeAux_iff 10 bs _ rest).mpr ⟨pre, hbs, hs, rfl⟩
+      rw [h] at h2
+      simp only [Option.some.injEq, Prod.mk.injEq] at h2
+      exact ⟨by rw [hv, h2.1], h2.2⟩
+
+/-! ## The shortest varint -/
+
+theorem toUInt8_toNat_of_lt (n : Nat) (h : n < 256) : n.toUInt8.toNat = n := by
+  simp
+  omega
+
+theorem varintAux_succ (f n : Nat) :
+    Spec.varintAux (f + 1) n =
+      if n < 128 then [n.toUInt8] else (n % 128 + 128).toUInt8 :: Spec.varintAux f (n / 128) :=
+  rfl
+
+theorem div_lt (n f : Nat) (h : n < 128 ^ (f + 1)) : n / 128 < 128 ^ f :=
+  (Nat.div_lt_iff_lt_mul (by decide)).mpr (by rw [← Nat.pow_succ]; exact h)
+
+theorem lt_pow (n : Nat) : n < 128 ^ (n + 1) :=
+  Nat.lt_of_lt_of_le (Nat.lt_pow_self (by decide)) (Nat.pow_le_pow_right (by decide) (by omega))
+
+theorem single_shape (n : Nat) (h : n < 128) :
+    Spec.VarintShape [n.toUInt8].length [n.toUInt8] ∧ Spec.groupsValue [n.toUInt8] = n := by
+  have h1 : n.toUInt8.toNat = n := toUInt8_toNat_of_lt n (by omega)
+  refine ⟨(shape_cons 0 _ []).mpr (Or.inl ⟨by omega, rfl⟩), ?_⟩
+  rw [groupsValue_cons, groupsValue_nil, h1]
+  omega
+
+theorem cons_shape (n : Nat) (rest : List UInt8)
+    (hr : Spec.VarintShape rest.length rest ∧ Spec.groupsValue rest = n / 128) :
+    Spec.VarintShape ((n % 128 + 128).toUInt8 :: rest).length ((n % 128 + 128).toUInt8 :: rest) ∧
+      Spec.groupsValue ((n % 128 + 128).toUInt8 :: rest) = n := by
+  have h1 : (n % 128 + 128).toUInt8.toNat = n % 128 + 128 := toUInt8_toNat_of_lt _ (by omega)
+  refine ⟨(shape_cons rest.length _ rest).mpr (Or.inr ⟨by omega, hr.1⟩), ?_⟩
+  rw [groupsValue_cons, hr.2, h1]
+  omega
+
+theorem varintAux_shape (f : Nat) : ∀ n, n < 128 ^ (f + 1) →
+    Spec.VarintShape (Spec.varintAux (f + 1) n).length (Spec.varintAux (f + 1) n) ∧
+      Spec.groupsValue (Spec.varintAux (f + 1) n) = n := by
+  induction f with
+  | zero =>
+    intro n hn
+    have h : n < 128 := by simpa using hn
+    rw [varintAux_succ]
+    simp only [h, ite_true]
+    exact single_shape n h
+  | succ f ih =>
+    intro n hn
+    rw [varintAux_succ]
+    by_cases h : n < 128
+    · simp only [h, ite_true]
+      exact single_shape n h
+    · simp only [h, ite_false]
+      exact cons_shape n _ (ih (n / 128) (div_lt n (f + 1) hn))
+
+theorem varint_shape (n : Nat) :
+    Spec.VarintShape (Spec.varint n).length (Spec.varint n) ∧ Spec.groupsValue (Spec.varint n) = n :=
+  varintAux_shape n n (lt_pow n)
+
+theorem varintAux_length (f : Nat) :
+    ∀ n k, 1 ≤ k → n < 128 ^ k → (Spec.varintAux f n).length ≤ k := by
+  induction f with
+  | zero =>
+    intro n k _ _
+    simp [Spec.varintAux]
+  | succ f ih =>
+    intro n k hk hn
+    rw [varintAux_succ]
+    by_cases h : n < 128
+    · simp only [h, ite_true, List.length_singleton]
+      exact hk
+    · simp only [h, ite_false, List.length_cons]
+      obtain ⟨j, rfl⟩ : ∃ j, k = j + 1 := ⟨k - 1, by omega⟩
+      have hj : 1 ≤ j := by
+        rcases Nat.eq_zero_or_pos j with rfl | hj
+        · simp at hn
+          omega
+        · exact hj
+      have := ih (n / 128) j hj (div_lt n j hn)
+      omega
+
+theorem varint_length (n k : Nat) (hk : 1 ≤ k) (h : n < 128 ^ k) : (Spec.varint n).length ≤ k :=
+  varintAux_length (n + 1) n k hk h
+
+theorem shape_mono {k k' : Nat} {bs : List UInt8} (h : Spec.VarintShape k bs) (hk : k ≤ k') :
+    Spec.VarintShape k' bs :=
+  ⟨h.1, Nat.le_trans h.2.1 hk, h.2.2⟩
+
+theorem decodeAux_varint (n k : Nat) (rest : List UInt8) (hk : 1 ≤ k) (h : n < 128 ^ k) :
+    Varint.decodeAux k (Spec.varint n ++ rest) = some (n, rest) := by
+  have hs := varint_shape n
+  exact (decodeAux_iff k _ n rest).mpr
+    ⟨Spec.varint n, rfl, shape_mono hs.1 (varint_length n k hk h), hs.2.symm⟩
+
+/-! ## The encoder -/
+
+theorem encodeAux_eq (f n : Nat) : Varint.encodeAux f n = Spec.varintAux f n := by
+  induction f generalizing n with
+  | zero => rfl
+  | succ f ih => simp only [Varint.encodeAux, Spec.varintAux, ih]
+
+/-- More fuel than the digits need changes nothing. -/
+theorem varintAux_add (f g : Nat) :
+    ∀ n, n < 128 ^ (f + 1) → Spec.varintAux (f + g + 1) n = Spec.varintAux (f + 1) n := by
+  induction f with
+  | zero =>
+    intro n hn
+    have h : n < 128 := by simpa using hn
+    rw [varintAux_succ, varintAux_succ]
+    simp only [h, ite_true]
+  | succ f ih =>
+    intro n hn
+    rw [varintAux_succ, varintAux_succ]
+    by_cases h : n < 128
+    · simp only [h, ite_true]
+    · simp only [h, ite_false]
+      rw [Nat.add_right_comm f 1 g, ih (n / 128) (div_lt n (f + 1) hn)]
+
+theorem varintAux_eq_varint (f n : Nat) (hf : 1 ≤ f) (h : n < 128 ^ f) :
+    Spec.varintAux f n = Spec.varint n := by
+  unfold Spec.varint
+  obtain ⟨f, rfl⟩ : ∃ j, f = j + 1 := ⟨f - 1, by omega⟩
+  rcases Nat.le_total f n with hle | hle
+  · have := varintAux_add f (n - f) n h
+    rw [show f + (n - f) + 1 = n + 1 by omega] at this
+    exact this.symm
+  · have := varintAux_add n (f - n) n (lt_pow n)
+    rw [show n + (f - n) + 1 = f + 1 by omega] at this
+    exact this
+
+theorem two_pow_le : 2 ^ 64 ≤ 128 ^ 10 := by decide
+
+theorem encode_eq (n : Nat) (h : n < 2 ^ 64) : Varint.encode n = Spec.varint n := by
+  unfold Varint.encode
+  rw [encodeAux_eq]
+  exact varintAux_eq_varint 10 n (by decide) (Nat.lt_of_lt_of_le h two_pow_le)
+
+theorem decode_encode (n : Nat) (rest : List UInt8) (h : n < 2 ^ 64) :
+    Varint.decode (Varint.encode n ++ rest) = some (n, rest) := by
+  unfold Varint.decode
+  rw [encode_eq n h, decodeAux_varint n 10 rest (by decide) (Nat.lt_of_lt_of_le h two_pow_le)]
+  simp [Nat.mod_eq_of_lt h]
+
+end Protobuf.Proofs.Varint
diff --git a/Protobuf.lean b/Protobuf.lean
new file mode 100644
index 0000000..e4cf139
--- /dev/null
+++ b/Protobuf.lean
@@ -0,0 +1,8 @@
+/-
+  The Protobuf wire format: varints, fields, and messages as lists of
+  raw fields.
+-/
+
+import Protobuf.Types
+import Protobuf.Varint
+import Protobuf.Wire
diff --git a/Protobuf/Types.lean b/Protobuf/Types.lean
new file mode 100644
index 0000000..dd42d06
--- /dev/null
+++ b/Protobuf/Types.lean
@@ -0,0 +1,32 @@
+/-
+  What a message is on the wire: a list of fields, each a field number
+  and a raw value of one of four wire types. Part of the approved
+  specification, with `Spec.lean` and `Spec/Defs.lean`, since every
+  statement is about these types.
+
+  Which values are in range is `Spec.ValidField`, in `Spec/Defs.lean`.
+-/
+
+namespace Protobuf
+
+/-- A field's value as the wire carries it, before any schema gives it
+    a meaning. Groups (wire types 3 and 4) are outside this library. -/
+inductive Value where
+  /-- Wire type 0, `VARINT`: an unsigned value below 2^64. -/
+  | varint (v : Nat)
+  /-- Wire type 1, `I64`: eight bytes, read as an unsigned value. -/
+  | i64 (v : Nat)
+  /-- Wire type 2, `LEN`: a length, then that many bytes. -/
+  | len (bytes : List UInt8)
+  /-- Wire type 5, `I32`: four bytes, read as an unsigned value. -/
+  | i32 (v : Nat)
+  deriving DecidableEq, Repr
+
+/-- One field of a message: its field number and its value. A message
+    may repeat a field number; the order of fields is kept. -/
+structure Field where
+  number : Nat
+  value : Value
+  deriving DecidableEq, Repr
+
+end Protobuf
diff --git a/Protobuf/Varint.lean b/Protobuf/Varint.lean
new file mode 100644
index 0000000..0804cd9
--- /dev/null
+++ b/Protobuf/Varint.lean
@@ -0,0 +1,38 @@
+/-
+  Varints: unsigned numbers seven bits to a byte, least significant
+  group first, with the high bit of each byte set when another byte
+  follows.
+-/
+
+namespace Protobuf.Varint
+
+/-- At most `fuel` bytes of the varint for `n`. -/
+def encodeAux : Nat → Nat → List UInt8
+  | 0, _ => []
+  | fuel + 1, n =>
+    if n < 128 then [n.toUInt8] else (n % 128 + 128).toUInt8 :: encodeAux fuel (n / 128)
+
+/-- The shortest varint for `n`. Ten bytes hold any value below 2^64. -/
+def encode (n : Nat) : List UInt8 := encodeAux 10 n
+
+/-- Reads a varint of at most `k` bytes from the front of the input: the
+    number its groups make, and the bytes after it. Fails when the input
+    ends first, or when byte `k` still has its high bit set. -/
+def decodeAux : Nat → List UInt8 → Option (Nat × List UInt8)
+  | 0, _ => none
+  | _ + 1, [] => none
+  | k + 1, b :: bs =>
+    if b.toNat < 128 then some (b.toNat, bs)
+    else
+      match decodeAux k bs with
+      | some (v, rest) => some (b.toNat - 128 + 128 * v, rest)
+      | none => none
+
+/-- Reads a varint of up to ten bytes. Bits above the 64th are dropped,
+    as the reference parsers drop them. -/
+def decode (bs : List UInt8) : Option (Nat × List UInt8) :=
+  match decodeAux 10 bs with
+  | some (v, rest) => some (v % 2 ^ 64, rest)
+  | none => none
+
+end Protobuf.Varint
diff --git a/Protobuf/Wire.lean b/Protobuf/Wire.lean
new file mode 100644
index 0000000..cac05a3
--- /dev/null
+++ b/Protobuf/Wire.lean
@@ -0,0 +1,103 @@
+/-
+  Fields and messages on the wire.
+-/
+
+import Protobuf.Types
+import Protobuf.Varint
+
+namespace Protobuf
+
+/-! ## Encoding -/
+
+/-- The low `k` bytes of `n`, least significant first. -/
+def leBytes : Nat → Nat → List UInt8
+  | 0, _ => []
+  | k + 1, n => (n % 256).toUInt8 :: leBytes k (n / 256)
+
+def Value.wireType : Value → Nat
+  | .varint _ => 0
+  | .i64 _ => 1
+  | .len _ => 2
+  | .i32 _ => 5
+
+def Value.encode : Value → List UInt8
+  | .varint v => Varint.encode v
+  | .i64 v => leBytes 8 v
+  | .len d => Varint.encode d.length ++ d
+  | .i32 v => leBytes 4 v
+
+/-- The tag, a varint of the field number and the wire type, then the
+    value. -/
+def Field.encode (f : Field) : List UInt8 :=
+  Varint.encode (f.number * 8 + f.value.wireType) ++ f.value.encode
+
+/-- A message: its fields, one after another, in order. -/
+def encode (fs : List Field) : List UInt8 :=
+  fs.flatMap Field.encode
+
+/-- Whether the field can be written: a field number from 1 to
+    2^29 - 1, values that fit their wire type, and bytes shorter than
+    2^31 - 16, the longest the C++ parser reads. -/
+def Field.isValid (f : Field) : Bool :=
+  1 ≤ f.number && f.number < 2 ^ 29 &&
+  match f.value with
+  | .varint v => v < 2 ^ 64
+  | .i64 v => v < 2 ^ 64
+  | .len d => d.length < 2 ^ 31 - 16
+  | .i32 v => v < 2 ^ 32
+
+/-! ## Decoding -/
+
+/-- Bytes read as a number, least significant first. -/
+def leValue (bs : List UInt8) : Nat :=
+  bs.foldr (fun b acc => b.toNat + 256 * acc) 0
+
+/-- Reads one field from the front of the input: the field, and the
+    bytes after it. Each length check looks at no more of the input than
+    the field needs, so reading a message takes time in proportion to
+    its length. -/
+def decodeField (bs : List UInt8) : Option (Field × List UInt8) :=
+  match Varint.decodeAux 5 bs with
+  | none => none
+  | some (t, rest) =>
+    if 2 ^ 32 ≤ t ∨ t / 8 = 0 then none
+    else
+      let n := t / 8
+      match t % 8 with
+      | 0 =>
+        match Varint.decode rest with
+        | some (v, rest) => some (⟨n, .varint v⟩, rest)
+        | none => none
+      | 1 =>
+        if (rest.take 8).length < 8 then none
+        else some (⟨n, .i64 (leValue (rest.take 8))⟩, rest.drop 8)
+      | 2 =>
+        match Varint.decodeAux 5 rest with
+        | some (len, rest) =>
+          if 2 ^ 31 - 16 ≤ len ∨ (rest.take len).length < len then none
+          else some (⟨n, .len (rest.take len)⟩, rest.drop len)
+        | none => none
+      | 5 =>
+        if (rest.take 4).length < 4 then none
+        else some (⟨n, .i32 (leValue (rest.take 4))⟩, rest.drop 4)
+      | _ => none
+
+/-- Reads fields until the input ends. Each field takes at least one
+    byte, so `fuel` equal to the input's length is enough. -/
+def decodeAux : Nat → List UInt8 → Option (List Field)
+  | _, [] => some []
+  | 0, _ :: _ => none
+  | fuel + 1, b :: bs =>
+    match decodeField (b :: bs) with
+    | some (f, rest) =>
+      match decodeAux fuel rest with
+      | some fs => some (f :: fs)
+      | none => none
+    | none => none
+
+/-- Reads a whole message. Fails on anything that is not a sequence of
+    well-formed fields, including input that ends inside a field. -/
+def decode (bs : List UInt8) : Option (List Field) :=
+  decodeAux bs.length bs
+
+end Protobuf
diff --git a/README.md b/README.md
index 09395a9..4c3886f 100644
--- a/README.md
+++ b/README.md
@@ -1,2 +1,95 @@
-# protobuf
-lean Protobuf wire format codec
+# protobuf: the Protobuf wire format, proved
+
+This library reads and writes the Protobuf wire format in Lean: varints, field tags, and messages as lists of raw fields. Machine-checked proofs show three things:
+
+- the decoder accepts exactly the messages that the rules in `SPEC.md` allow, and refuses everything else, including input cut short. Those rules are the encoding guide's, without groups, taking the stricter reading wherever Google's two parsers disagree;
+- for fields that `Field.isValid` accepts, the encoder writes what the guide describes;
+- for those fields, decoding what the encoder wrote gives the fields back.
+
+It is tested against Google's own parsers, upb and C++; `tests/TEST-RESULTS.md` has the record.
+
+It is a project of [Proven Commons](https://github.com/Proven-Commons/mission), built to the verified bar published there.
+
+Status: in progress. The specification has not yet been approved by a reviewer apart from its author, so this is not verified.
+
+## Use it
+
+From Lean:
+
+- `Protobuf.decode` reads a whole message as a list of fields, or fails.
+- `Protobuf.encode` writes a list of fields. It is specified only for fields that `Field.isValid` accepts, so check that first, as the command-line tool does. For a field out of range, it writes bytes that do not read back as that field.
+- `Field.isValid` says whether a field can be written.
+- `Varint.encode` and `Varint.decode` work on single varints. `Varint.encode` is specified for numbers below 2^64.
+
+`SPEC.md` says what each one does.
+
+## What is proved
+
+The statements are in `Spec.lean`. The definitions they use, written from the encoding guide, are in `Spec/Defs.lean`, and the types are in `Protobuf/Types.lean`. The proofs are in `Proofs/`.
+
+| Claim | Theorem |
+|-------|---------|
+| For numbers below 2^64, the encoder writes the shortest varint. | `Spec.varint_encode_eq` |
+| The varint decoder reads exactly one varint of up to ten bytes from the front of its input, leaves the rest untouched, and refuses everything else. That includes input that ends inside the varint, and an eleventh byte. | `Spec.varint_decode_iff` |
+| For numbers below 2^64, decoding a varint the encoder wrote gives the number back. | `Spec.varint_decode_encode` |
+| `isValid` decides exactly which fields can be written: field numbers 1 to 2^29 - 1, values that fit their wire type, and bytes shorter than 2^31 - 16. | `Spec.isValid_iff` |
+| For valid fields, the encoder writes each field as the guide describes: the tag, then the payload, every varint in its shortest form. | `Spec.encode_eq` |
+| `decode` returns a field list exactly when the bytes split into records, one per field, in order, by the rules in `SPEC.md`. So it reads every message made of `VARINT`, `I64`, `LEN` and `I32` records with field numbers from 1 to 2^29 - 1, and returns the fields as written. It refuses everything else: a record cut short, a length past the end, field number 0, a group, an unknown wire type, and an oversized tag or length. | `Spec.decode_iff` |
+| For valid fields, decoding what the encoder wrote gives the fields back. | `Spec.decode_encode` |
+| Every field the decoder returns can be written again. | `Spec.decode_valid` |
+| The guide's worked bytes (1, 150 and -2 as varints, and its messages `Test1` to `Test4`), and the edge and refusal cases listed in `SPEC.md`. | `Spec.guide_vectors`, `Spec.edge_vectors`, `Spec.reject_vectors` |
+
+The command-line tool in `Main.lean` calls these functions directly.
+
+## What is not proved
+
+- Reading requests and printing answers in `Main.lean`: the hex and decimal parsing and printing, and the request format. The differential tests cover them, with malformed requests and CR LF line endings.
+- Groups (wire types 3 and 4) are refused, although the encoding guide still describes them and both reference parsers read them. The guide calls them deprecated; they are left for a later slice.
+- Where the two reference parsers disagree, this decoder takes the stricter reading:
+  - it refuses field number 0, which upb reads; the guide does not forbid it, but the language guide's field numbers start at 1;
+  - it refuses a tag of 2^32 or more, which the C++ parser reads by dropping the high bits;
+  - it refuses a `LEN` length of 2^31 - 16 or more, which upb reads. The tests cannot reach this case, since it needs an input of 2 GiB, so it rests on the proof alone.
+- What fields mean. Schemas, `.proto` files, field types such as signed or zigzag integers, floats, strings, nested messages and packed repeated fields all sit above the wire format. A `LEN` field's bytes are returned as they are.
+- Limits on message size that a program may want. The decoder reads any input in memory.
+- Speed. The code works on lists of bytes, which suits proofs, not bulk data. Decoding takes time in proportion to the input's length.
+
+## What you must trust
+
+- The Lean kernel and the five external kernels shipped with Lean, which all check the proofs.
+- `lake comparator`, which builds the statements and the proofs in a sandbox, exports them, and checks that each proof proves exactly its statement.
+- bubblewrap and the Linux kernel's namespaces, which keep the untrusted build from tampering with that check.
+- The Lean compiler, with the C compiler and linker shipped with it, and the runtime, which turn the proved definitions into the program that runs.
+- Lean's core library, including the compiled code it puts in place of some definitions the proofs reason about (by `implemented_by` and `extern`), such as the arithmetic on natural numbers and the fixed-width byte type.
+- The operating system and hardware it runs on.
+- Python's `protobuf` and `grpcio-tools` packages, as the oracle in the differential tests. The record names their versions.
+
+This project has no dependencies beyond Lean itself.
+
+## Re-check it
+
+Needs Linux, [elan](https://github.com/leanprover/elan), bubblewrap (`apt install bubblewrap`), and Python 3.11 or later with `venv`, and network access for the oracle packages.
+
+```
+lake build
+lake comparator --paranoid
+python3 tests/run_tests.py
+```
+
+`lake comparator --paranoid` builds the statements and the proofs in a sandbox. It checks that each theorem in `Proofs/` proves exactly the statement in `Spec.lean`, using only the axioms `propext`, `Classical.choice`, and `Quot.sound`, and replays it through every kernel shipped with Lean.
+
+The test script installs the pinned oracle packages into `.lake/oracle-venv` when they are missing. It then compares the tool with upb and with the C++ parser on inputs from a recorded seed, and rewrites `tests/TEST-RESULTS.md`. `tests/planted_bugs.py` plants ten small bugs in a copy of the code, and `tests/PLANTED-BUGS.md` records that the tests catch nine; the tenth, a missing `LEN` length limit, needs a 2 GiB input to show, so it rests on `Spec.decode_iff`.
+
+## Layout
+
+- `Protobuf/Types.lean`: the field and value types. It is part of the specification.
+- `Protobuf/Varint.lean`, `Protobuf/Wire.lean`: the code under proof.
+- `Spec.lean`: the statements, with `sorry` for proofs. A reviewer approves this file.
+- `Spec/Defs.lean`: the definitions the statements use, written from the encoding guide, with checks against its worked bytes.
+- `Proofs.lean` and `Proofs/`: the proofs, under the same names.
+- `Main.lean`: the command-line tool the tests drive.
+- `lakefile.toml`: the build. It names the package and its version, its libraries and executable, and the default targets, and sets nothing else.
+- `comparator.json`: which theorems `lake comparator` checks, and which axioms it allows.
+- `bar.toml`: the record for the bar check: status, authors, approvals, and where things are.
+- `SPEC.md`: the specification in plain words.
+- `tests/run_tests.py`: the differential tests.
+- `tests/planted_bugs.py`: plants small bugs in a copy of the code, and records in `tests/PLANTED-BUGS.md` whether the tests catch each one.
diff --git a/SPEC.md b/SPEC.md
new file mode 100644
index 0000000..0ed95f4
--- /dev/null
+++ b/SPEC.md
@@ -0,0 +1,100 @@
+# Specification: protobuf
+
+This library implements the Protobuf wire format: varints, field tags, and messages as lists of raw fields. It is the layer under every `.proto` schema. It reads and writes the bytes without knowing what the fields mean. A reviewer who did not write this specification approves it. The approval also covers `Spec.lean`, `Spec/Defs.lean`, `Protobuf/Types.lean`, and the other files `bar.toml` lists.
+
+The source is the Protobuf encoding guide, <https://protobuf.dev/programming-guides/encoding/>. Where the guide leaves a choice, the source is the behaviour of Google's two parsers: upb, which Python's `protobuf` package uses, and the C++ parser behind `protoc --decode_raw`.
+
+Bytes are `List UInt8`. The command-line tool converts them at the edges.
+
+## Varints
+
+A varint carries an unsigned number seven bits to a byte, least significant group first. The high bit of each byte is set when another byte follows.
+
+- `Varint.encode` writes the shortest varint for a number below 2^64, from one to ten bytes.
+- `Varint.decode` reads one varint from the front of its input and returns its value and the rest of the input.
+  - It reads up to ten bytes.
+  - It fails when the input ends inside the varint, or when the tenth byte still has its high bit set.
+  - Any bits above the 64th are dropped, as both reference parsers drop them.
+  - A varint need not be in its shortest form: `80 00` reads as 0, as in both reference parsers.
+
+## Fields
+
+A message is a sequence of records. Each record is a tag, then a payload. The tag is a varint of `field_number * 8 + wire_type`.
+
+| Wire type | Name | Payload | Value here |
+|-----------|------|---------|------------|
+| 0 | `VARINT` | a varint | `.varint v`, below 2^64 |
+| 1 | `I64` | eight bytes | `.i64 v`, the bytes little-endian |
+| 2 | `LEN` | a varint length, then that many bytes | `.len bytes` |
+| 5 | `I32` | four bytes | `.i32 v`, the bytes little-endian |
+
+The decoder refuses everything else:
+
+- a tag longer than five bytes, or of 2^32 or more;
+- field number 0;
+- wire types 3 and 4, which are groups;
+- wire types 6 and 7, which do not exist;
+- a length longer than five bytes, of 2^31 - 16 or more, or running past the end of the input;
+- any record cut short.
+
+Groups are deprecated in the guide and outside this first slice.
+
+The two reference parsers differ in three places, and this library takes the stricter reading in each:
+
+- upb reads field number 0, which the C++ parser refuses. The encoding guide does not forbid field number 0, but the language guide's field numbers start at 1.
+- The C++ parser reads a five-byte tag of 2^32 or more by dropping its high bits, which upb refuses.
+- upb reads a `LEN` length up to 2^31 - 1, while the C++ parser refuses one of 2^31 - 16 or more. The encoding guide says a message must be smaller than 2 GiB.
+
+`Field.isValid` says which fields the encoder can write:
+
+- a field number from 1 to 2^29 - 1;
+- a `VARINT` or `I64` value below 2^64;
+- an `I32` value below 2^32;
+- `LEN` bytes shorter than 2^31 - 16.
+
+`encode` and `Varint.encode` are specified only for valid fields and for numbers below 2^64. For anything else they write bytes that do not read back as what was given, so a program checks `Field.isValid` first, as the command-line tool does.
+
+## Messages
+
+`encode` writes each field in turn: the shortest varint for its tag, then its payload, with any varint in its shortest form.
+
+`decode` reads records until the input ends and returns the fields in order. A field number may repeat, and the order is kept. The empty input is the empty message. If any record is malformed, the whole input is refused. `decode` never returns part of a message. Each length check looks at no more of the input than the field needs, so decoding takes time in proportion to the input's length.
+
+## The command-line tool
+
+`protowire serve`, in `Main.lean`, answers requests from the differential tests, one per line. Its header comment gives the protocol. Every answer comes from `decode`, `encode` and `Field.isValid`.
+
+## What must always hold
+
+Each property is a theorem in `Spec.lean`, under the name given. The definitions the statements use are in `Spec/Defs.lean`. They are written from the encoding guide and checked against its worked bytes.
+
+| Property | Theorem |
+|----------|---------|
+| For numbers below 2^64, the encoder writes the shortest varint. | `Spec.varint_encode_eq` |
+| The varint decoder reads exactly one varint of up to ten bytes from the front of its input, keeps the rest untouched, and refuses everything else. | `Spec.varint_decode_iff` |
+| For numbers below 2^64, decoding a varint the encoder wrote gives the number back. | `Spec.varint_decode_encode` |
+| `isValid` decides exactly which fields can be written. | `Spec.isValid_iff` |
+| For valid fields, the encoder writes each field as the guide describes. | `Spec.encode_eq` |
+| `decode` returns a field list exactly when the bytes split into records, one per field, in order, by the rules above. | `Spec.decode_iff` |
+| For valid fields, decoding what the encoder wrote gives the fields back. | `Spec.decode_encode` |
+| Every field the decoder returns can be written again. | `Spec.decode_valid` |
+| The guide's worked bytes: 1, 150 and -2 as varints, and its messages `Test1` to `Test4`. | `Spec.guide_vectors` |
+| 2^64 - 1 is ten bytes, fixed-width values are little-endian, varints need not be in shortest form, ten-byte varints drop bits past the 64th, the largest field number reads, and so does the empty message. | `Spec.edge_vectors` |
+| The decoder refuses each kind of malformed input listed above, except a length of 2^31 - 16 or more, which needs a 2 GiB input; `Spec.decode_iff` covers it. | `Spec.reject_vectors` |
+
+Together, these fix every output.
+
+- `decode` is fixed for every input.
+- `encode` and `Varint.encode` are fixed for every valid input.
+- A decoder that accepted nothing would meet `Spec.decode_valid`, but it would fail `Spec.decode_iff` and `Spec.decode_encode`.
+- `encode` is not fixed for fields that are not valid.
+- A decoder that accepted too much would fail `Spec.decode_iff`.
+
+## Oracle
+
+Google's Protobuf parsers, compared on every input:
+
+- upb, through Python's `protobuf` package, reading each message as `google.protobuf.Empty` so that every field is kept as an unknown field;
+- the C++ parser behind `protoc --decode_raw`, run in-process through `grpcio-tools`.
+
+The encoder is compared with `google.protobuf.internal.encoder`.
diff --git a/Spec.lean b/Spec.lean
new file mode 100644
index 0000000..135ee17
--- /dev/null
+++ b/Spec.lean
@@ -0,0 +1,122 @@
+/-
+  The specification as Lean statements: the challenge file.
+
+  A reviewer who did not write this file approves it, and `bar.toml`
+  records the hash it had then. The proofs live in `Proofs.lean`, under
+  the same names; `lake comparator` checks that each one proves exactly
+  the statement written here. The `sorry`s below are expected in this
+  file only.
+
+  The definitions the statements use, written from the Protobuf encoding
+  guide, are in `Spec/Defs.lean`, and the types in `Protobuf/Types.lean`.
+  Both are part of the specification too.
+-/
+
+import Protobuf
+import Spec.Defs
+
+open Protobuf
+
+/-! ## Varints -/
+
+/-- The encoder writes the shortest varint. -/
+theorem Spec.varint_encode_eq (n : Nat) (h : n < 2 ^ 64) : Varint.encode n = Spec.varint n := sorry
+
+/-- The decoder reads exactly one varint from the front of its input:
+    up to ten bytes, the last without its high bit, and returns its
+    value and the rest of the input untouched. Anything else, including
+    input that ends inside the varint and an eleventh byte, is
+    refused. -/
+theorem Spec.varint_decode_iff (bs : List UInt8) (v : Nat) (rest : List UInt8) :
+    Varint.decode bs = some (v, rest) ↔ ∃ pre, bs = pre ++ rest ∧ Spec.IsVarint pre v := sorry
+
+/-- Round trip: decoding what the encoder wrote gives the number back,
+    and leaves what follows untouched. -/
+theorem Spec.varint_decode_encode (n : Nat) (rest : List UInt8) (h : n < 2 ^ 64) :
+    Varint.decode (Varint.encode n ++ rest) = some (n, rest) := sorry
+
+/-! ## Messages -/
+
+/-- `isValid` decides exactly which fields can be written. -/
+theorem Spec.isValid_iff (f : Field) : f.isValid = true ↔ Spec.ValidField f := sorry
+
+/-- The encoder writes each field as the encoding guide describes, with
+    every varint in its shortest form. -/
+theorem Spec.encode_eq (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) :
+    Protobuf.encode fs = Spec.encode fs := sorry
+
+/-- `decode` returns `fs` exactly when the bytes split into records, one
+    per field of `fs`, in order, by the rules of `Spec.FieldBytes`. So it
+    reads every message made of `VARINT`, `I64`, `LEN` and `I32` records
+    with field numbers from 1 to 2^29 - 1, refuses everything else (a
+    record cut short, a length past the end, field number 0, a group, an
+    unknown wire type, an oversized tag or length), and returns the
+    fields as written. -/
+theorem Spec.decode_iff (bs : List UInt8) (fs : List Field) :
+    decode bs = some fs ↔ Spec.Message bs fs := sorry
+
+/-- Round trip: decoding what the encoder wrote gives the fields back. -/
+theorem Spec.decode_encode (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) :
+    decode (Protobuf.encode fs) = some fs := sorry
+
+/-- Every field the decoder returns can be written again. -/
+theorem Spec.decode_valid (bs : List UInt8) (fs : List Field) (h : decode bs = some fs) :
+    ∀ f ∈ fs, Spec.ValidField f := sorry
+
+/-! ## Test vectors -/
+
+/-- The encoding guide's worked bytes: 1 and 150 as varints, -2 as a
+    ten-byte varint (2^64 - 2 unsigned), and the messages `Test1` with
+    field 1 set to 150, `Test2` with field 2 set to "testing", `Test3`
+    holding the first message in field 3, and `Test4` with field 4 set
+    to "hello" and field 5 packed with 1, 2 and 3. -/
+theorem Spec.guide_vectors :
+    Varint.encode 1 = [0x01] ∧
+    Varint.encode 150 = [0x96, 0x01] ∧
+    Varint.encode (2 ^ 64 - 2) = [0xfe, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0x01] ∧
+    decode [0x08, 0x96, 0x01] = some [⟨1, .varint 150⟩] ∧
+    decode [0x12, 0x07, 0x74, 0x65, 0x73, 0x74, 0x69, 0x6e, 0x67] =
+      some [⟨2, .len [0x74, 0x65, 0x73, 0x74, 0x69, 0x6e, 0x67]⟩] ∧
+    decode [0x1a, 0x03, 0x08, 0x96, 0x01] = some [⟨3, .len [0x08, 0x96, 0x01]⟩] ∧
+    decode [0x22, 0x05, 0x68, 0x65, 0x6c, 0x6c, 0x6f, 0x2a, 0x03, 0x01, 0x02, 0x03] =
+      some [⟨4, .len [0x68, 0x65, 0x6c, 0x6c, 0x6f]⟩, ⟨5, .len [0x01, 0x02, 0x03]⟩] ∧
+    Protobuf.encode [⟨1, .varint 150⟩, ⟨2, .len [0x74, 0x65, 0x73, 0x74, 0x69, 0x6e, 0x67]⟩] =
+      [0x08, 0x96, 0x01, 0x12, 0x07, 0x74, 0x65, 0x73, 0x74, 0x69, 0x6e, 0x67] := sorry
+
+/-- Cases the guide does not work through: the largest 64-bit value is
+    ten bytes; fixed-width values are little-endian; the reference
+    parsers' readings of unusual varints, not in shortest form, and ten
+    bytes with bits past the 64th; the largest field number; and the
+    empty message. -/
+theorem Spec.edge_vectors :
+    Varint.encode (2 ^ 64 - 1) = [0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0x01] ∧
+    decode [0x0d, 0x01, 0x02, 0x03, 0x04] = some [⟨1, .i32 0x04030201⟩] ∧
+    decode [0x09, 0x01, 0x02, 0x03, 0x04, 0x05, 0x06, 0x07, 0x08] =
+      some [⟨1, .i64 0x0807060504030201⟩] ∧
+    decode [0x08, 0x80, 0x00] = some [⟨1, .varint 0⟩] ∧
+    decode [0x08, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0x7f] =
+      some [⟨1, .varint (2 ^ 64 - 1)⟩] ∧
+    decode [0xf8, 0xff, 0xff, 0xff, 0x0f, 0x01] = some [⟨2 ^ 29 - 1, .varint 1⟩] ∧
+    decode [] = some [] := sorry
+
+/-- Input the decoder refuses: a varint cut short, an eleventh varint
+    byte, field number 0, a length past the end, fixed-width values cut
+    short, a group start and a group end, wire types 6 and 7, a tag of
+    2^32 or more (from exactly 2^32, which would be field number 2^29),
+    and a tag or length longer than five bytes. -/
+theorem Spec.reject_vectors :
+    decode [0x08] = none ∧
+    decode [0x08, 0x80] = none ∧
+    decode [0x08, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x00] = none ∧
+    decode [0x00, 0x00] = none ∧
+    decode [0x0a, 0x04, 0x61, 0x62] = none ∧
+    decode [0x0d, 0x01, 0x02, 0x03] = none ∧
+    decode [0x09, 0x01, 0x02, 0x03, 0x04, 0x05, 0x06, 0x07] = none ∧
+    decode [0x0b, 0x0c] = none ∧
+    decode [0x0c] = none ∧
+    decode [0x0e, 0x00] = none ∧
+    decode [0x0f, 0x00] = none ∧
+    decode [0xf8, 0xff, 0xff, 0xff, 0x1f, 0x01] = none ∧
+    decode [0x80, 0x80, 0x80, 0x80, 0x10, 0x01] = none ∧
+    decode [0x88, 0x80, 0x80, 0x80, 0x80, 0x00, 0x01] = none ∧
+    decode [0x0a, 0x81, 0x80, 0x80, 0x80, 0x80, 0x00, 0x61] = none := sorry
diff --git a/Spec/Defs.lean b/Spec/Defs.lean
new file mode 100644
index 0000000..b7c213b
--- /dev/null
+++ b/Spec/Defs.lean
@@ -0,0 +1,153 @@
+/-
+  The definitions the specification uses, written from the Protobuf
+  encoding guide (https://protobuf.dev/programming-guides/encoding/)
+  independently of the code in `Protobuf/`. Part of the approved
+  specification, with `Spec.lean` and `Protobuf/Types.lean`.
+
+  Both the challenge file and the proofs import this file, so each
+  statement means the same thing on both sides. The `example`s check the
+  definitions against the guide's worked bytes.
+-/
+
+import Protobuf
+
+open Protobuf
+
+/-! ## Varints
+
+"Each byte in the varint has a continuation bit that indicates if the
+byte that follows it is part of the varint. This is the most significant
+bit (MSB) of the byte. The lower 7 bits of each byte are used to store
+the two's complement representation of the number in groups of 7 bits,
+least significant group first." Varints carry unsigned 64-bit values in
+one to ten bytes. -/
+
+/-- The number the low seven bits of each byte make, least significant
+    group first. -/
+def Spec.groupsValue (bs : List UInt8) : Nat :=
+  ((List.range bs.length).map fun i => (bs.getD i 0).toNat % 128 * 128 ^ i).sum
+
+/-- The shape of a varint of at most `k` bytes: at least one byte, every
+    byte but the last with its high bit set, the last without it. -/
+def Spec.VarintShape (k : Nat) (bs : List UInt8) : Prop :=
+  bs ≠ [] ∧ bs.length ≤ k ∧
+    (∀ b ∈ bs.dropLast, 128 ≤ b.toNat) ∧ (∀ b ∈ bs.getLast?, b.toNat < 128)
+
+/-- `bs` is a varint for `v`. The reference parsers read up to ten
+    bytes and drop any bits above the 64th, so a value is its groups
+    modulo 2^64. A varint need not be in its shortest form: the
+    reference parsers read `80 00` as 0. -/
+def Spec.IsVarint (bs : List UInt8) (v : Nat) : Prop :=
+  Spec.VarintShape 10 bs ∧ v = Spec.groupsValue bs % 2 ^ 64
+
+/-- The shortest varint for `n`, as an encoder writes it: seven bits at
+    a time, least significant first, with the high bit set on every
+    byte but the last. `fuel` bounds the number of bytes; `n + 1` is
+    always enough. -/
+def Spec.varintAux : Nat → Nat → List UInt8
+  | 0, _ => []
+  | fuel + 1, n =>
+    if n < 128 then [n.toUInt8] else (n % 128 + 128).toUInt8 :: Spec.varintAux fuel (n / 128)
+
+def Spec.varint (n : Nat) : List UInt8 := Spec.varintAux (n + 1) n
+
+-- The guide's examples: 1 is `01`, and 150 is `96 01`.
+example : Spec.varint 1 = [0x01] := by decide
+example : Spec.varint 150 = [0x96, 0x01] := by decide
+example : Spec.groupsValue [0x96, 0x01] = 150 := by decide
+example : Spec.VarintShape 10 [0x96, 0x01] := by unfold Spec.VarintShape; decide
+
+/-! ## Fixed-width values
+
+"Non-varint numeric types are simple. `double` and `fixed64` have wire
+type `I64`, which tells the parser to expect a fixed eight-byte lump of
+data. ... Similarly `float` and `fixed32` have wire type `I32`, which
+tells it to expect four bytes instead." The bytes are little-endian. -/
+
+/-- The bytes read as a number, least significant first. -/
+def Spec.leValue (bs : List UInt8) : Nat :=
+  ((List.range bs.length).map fun i => (bs.getD i 0).toNat * 256 ^ i).sum
+
+/-- `n` in `k` bytes, least significant first. -/
+def Spec.leBytes (k n : Nat) : List UInt8 :=
+  (List.range k).map fun i => (n / 256 ^ i % 256).toUInt8
+
+example : Spec.leValue [0x01, 0x02, 0x03, 0x04] = 0x04030201 := by decide
+example : Spec.leBytes 4 0x04030201 = [0x01, 0x02, 0x03, 0x04] := by decide
+
+/-! ## Fields and messages
+
+"A protocol buffer message is a series of key-value pairs." Each record
+is a tag, then its payload. "The 'tag' of a record is encoded as a
+varint formed from the field number and the wire type via the formula
+`(field_number << 3) | wire_type`." The wire types are 0 `VARINT`,
+1 `I64`, 2 `LEN`, 3 `SGROUP`, 4 `EGROUP` and 5 `I32`. "The `LEN` wire
+type has a dynamic length, specified by a varint immediately after the
+tag, which is followed by the payload as usual."
+
+The language guide gives field numbers from 1 to 2^29 - 1, and the
+encoding guide says "Protos must be smaller than 2 GiB when serialized".
+Both reference parsers read a tag or a length as a varint of at most
+five bytes. Where they disagree, this specification takes the stricter
+reading: upb reads field number 0 and the C++ parser refuses it; the C++
+parser reads a tag of 2^32 or more by dropping its high bits and upb
+refuses it; upb reads a length up to 2^31 - 1 and the C++ parser refuses
+one of 2^31 - 16 or more. Groups, wire types 3 and 4, are deprecated and
+outside this library; wire types 6 and 7 do not exist. -/
+
+/-- A field the encoder can write: a field number from 1 to 2^29 - 1,
+    and a value that fits its wire type, with bytes the C++ parser
+    reads. -/
+def Spec.ValidField (f : Field) : Prop :=
+  1 ≤ f.number ∧ f.number < 2 ^ 29 ∧
+  match f.value with
+  | .varint v => v < 2 ^ 64
+  | .i64 v => v < 2 ^ 64
+  | .len d => d.length < 2 ^ 31 - 16
+  | .i32 v => v < 2 ^ 32
+
+/-- `tag` then `payload` are the bytes of field `f`. -/
+def Spec.FieldBytes (tag payload : List UInt8) (f : Field) : Prop :=
+  Spec.VarintShape 5 tag ∧ Spec.groupsValue tag < 2 ^ 32 ∧
+  f.number = Spec.groupsValue tag / 8 ∧ 1 ≤ f.number ∧
+  match Spec.groupsValue tag % 8, f.value with
+  | 0, .varint v => Spec.IsVarint payload v
+  | 1, .i64 v => payload.length = 8 ∧ v = Spec.leValue payload
+  | 2, .len d =>
+    ∃ pre, payload = pre ++ d ∧ Spec.VarintShape 5 pre ∧ Spec.groupsValue pre = d.length ∧
+      d.length < 2 ^ 31 - 16
+  | 5, .i32 v => payload.length = 4 ∧ v = Spec.leValue payload
+  | _, _ => False
+
+/-- `bs` is a message whose fields, in order, are `fs`: the bytes split
+    into records, one per field. -/
+inductive Spec.Message : List UInt8 → List Field → Prop where
+  | nil : Spec.Message [] []
+  | cons {tag payload rest : List UInt8} {f : Field} {fs : List Field} :
+      Spec.FieldBytes tag payload f → Spec.Message rest fs →
+      Spec.Message (tag ++ payload ++ rest) (f :: fs)
+
+/-- The bytes an encoder writes for a field: the shortest varint for
+    the tag, then the payload, with any varint in its shortest form. -/
+def Spec.fieldBytes (f : Field) : List UInt8 :=
+  match f.value with
+  | .varint v => Spec.varint (f.number * 8 + 0) ++ Spec.varint v
+  | .i64 v => Spec.varint (f.number * 8 + 1) ++ Spec.leBytes 8 v
+  | .len d => Spec.varint (f.number * 8 + 2) ++ Spec.varint d.length ++ d
+  | .i32 v => Spec.varint (f.number * 8 + 5) ++ Spec.leBytes 4 v
+
+/-- The bytes an encoder writes for a message: its fields in order. -/
+def Spec.encode (fs : List Field) : List UInt8 :=
+  (fs.map Spec.fieldBytes).flatten
+
+-- The guide's examples: field 1 set to 150 is `08 96 01`, field 2 set
+-- to "testing" is `12 07 74 65 73 74 69 6e 67`, and field 3 holding the
+-- first message is `1a 03 08 96 01`.
+example : Spec.encode [⟨1, .varint 150⟩] = [0x08, 0x96, 0x01] := by decide
+example : Spec.encode [⟨2, .len [0x74, 0x65, 0x73, 0x74, 0x69, 0x6e, 0x67]⟩] =
+    [0x12, 0x07, 0x74, 0x65, 0x73, 0x74, 0x69, 0x6e, 0x67] := by decide
+example : Spec.encode [⟨3, .len [0x08, 0x96, 0x01]⟩] = [0x1a, 0x03, 0x08, 0x96, 0x01] := by decide
+example : Spec.FieldBytes [0x08] [0x96, 0x01] ⟨1, .varint 150⟩ := by
+  refine ⟨by unfold Spec.VarintShape; decide, by decide, by decide, by decide, ?_⟩
+  show Spec.IsVarint [0x96, 0x01] 150
+  exact ⟨by unfold Spec.VarintShape; decide, by decide⟩
diff --git a/bar.toml b/bar.toml
new file mode 100644
index 0000000..41dbccb
--- /dev/null
+++ b/bar.toml
@@ -0,0 +1,35 @@
+# Read by bar/check.py in Proven-Commons/mission.
+# See playbook/verified-bar.md there for what each field means.
+
+[project]
+name = "protobuf"
+# "in-progress" until every bar item passes, then "verified".
+status = "in-progress"
+page = "README.md"
+# GitHub handles of everyone who wrote the specification. It was drafted
+# by Claude, an AI agent, for the org.
+spec_authors = ["claude"]
+# The program people run. A change to it voids the approval.
+entry_points = ["Main.lean"]
+
+[spec]
+# Protobuf/Types.lean holds the types every statement is about, so it
+# is part of the specification.
+files = ["SPEC.md", "Spec.lean", "Spec/Defs.lean", "Protobuf/Types.lean"]
+# The code under proof: the functions the statements are about.
+code = [
+  "Protobuf.Varint.encode", "Protobuf.Varint.decode",
+  "Protobuf.encode", "Protobuf.decode", "Protobuf.Field.isValid",
+]
+
+# One entry per approval, added in a pull request the reviewer approves.
+# [[spec.approval]]
+# reviewer = "github-handle"
+# date = "2026-11-02"
+# sha256 = "..."
+# record = "https://github.com/Proven-Commons/protobuf/pull/<n>"
+
+[tests]
+results = "tests/TEST-RESULTS.md"
+command = "python3 tests/run_tests.py"
+files = ["tests/run_tests.py", "tests/planted_bugs.py"]
diff --git a/comparator.json b/comparator.json
new file mode 100644
index 0000000..da878b7
--- /dev/null
+++ b/comparator.json
@@ -0,0 +1,10 @@
+{
+  "challenge_module": "Spec",
+  "solution_module": "Proofs",
+  "theorem_names": [
+    "Spec.varint_encode_eq", "Spec.varint_decode_iff", "Spec.varint_decode_encode",
+    "Spec.isValid_iff", "Spec.encode_eq", "Spec.decode_iff", "Spec.decode_encode",
+    "Spec.decode_valid", "Spec.guide_vectors", "Spec.edge_vectors", "Spec.reject_vectors"
+  ],
+  "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"]
+}
diff --git a/lake-manifest.json b/lake-manifest.json
new file mode 100644
index 0000000..0bd7518
--- /dev/null
+++ b/lake-manifest.json
@@ -0,0 +1,6 @@
+{"version": "1.3.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "protobuf",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/lakefile.toml b/lakefile.toml
new file mode 100644
index 0000000..f65e4dc
--- /dev/null
+++ b/lakefile.toml
@@ -0,0 +1,16 @@
+name = "protobuf"
+version = "0.1.0"
+defaultTargets = ["Protobuf", "Spec", "Proofs", "protowire"]
+
+[[lean_lib]]
+name = "Protobuf"
+
+[[lean_lib]]
+name = "Spec"
+
+[[lean_lib]]
+name = "Proofs"
+
+[[lean_exe]]
+name = "protowire"
+root = "Main"
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000..a6aff06
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.35.0
diff --git a/tests/PLANTED-BUGS.md b/tests/PLANTED-BUGS.md
new file mode 100644
index 0000000..3cdb2e0
--- /dev/null
+++ b/tests/PLANTED-BUGS.md
@@ -0,0 +1,91 @@
+# Planted bugs
+
+Written by `python3 tests/planted_bugs.py`. Each row is one small change to the
+code, made in a copy. The tests ran on 20,000 inputs from their recorded seed
+against the changed tool. A bug is caught when they report failures.
+
+| Bug | File | Failures |
+|-----|------|----------|
+| Field number 0 read | `Protobuf/Wire.lean` | 170 |
+| Tags of 2^32 or more read | `Protobuf/Wire.lean` | 174 |
+| A tag of exactly 2^32 read | `Protobuf/Wire.lean` | 88 |
+| Six-byte tags read | `Protobuf/Wire.lean` | 133 |
+| Eleven-byte varints read | `Protobuf/Varint.lean` | 70 |
+| Bits past the 64th kept | `Protobuf/Varint.lean` | 23 |
+| No LEN length limit | `Protobuf/Wire.lean` | 0, not caught by the tests: it shows only when a length of 2^31 - 16 or more is followed by that many bytes, an input of about 2 GiB; a shorter input with such a length is refused for running out of input either way. `Spec.decode_iff` covers the limit. |
+| A group start tag read as an empty LEN field | `Protobuf/Wire.lean` | 150 |
+| isValid takes field number 2^29 | `Protobuf/Wire.lean` | 90 |
+| CR kept at the end of a CR LF request | `Main.lean` | 2856 |
+
+## The changes
+
+**Field number 0 read** in `Protobuf/Wire.lean`:
+
+```
+- if 2 ^ 32 ≤ t ∨ t / 8 = 0 then none
++ if 2 ^ 32 ≤ t then none
+```
+
+**Tags of 2^32 or more read** in `Protobuf/Wire.lean`:
+
+```
+- if 2 ^ 32 ≤ t ∨ t / 8 = 0 then none
++ if t / 8 = 0 then none
+```
+
+**A tag of exactly 2^32 read** in `Protobuf/Wire.lean`:
+
+```
+- if 2 ^ 32 ≤ t ∨ t / 8 = 0 then none
++ if 2 ^ 32 < t ∨ t / 8 = 0 then none
+```
+
+**Six-byte tags read** in `Protobuf/Wire.lean`:
+
+```
+-   match Varint.decodeAux 5 bs with
++   match Varint.decodeAux 6 bs with
+```
+
+**Eleven-byte varints read** in `Protobuf/Varint.lean`:
+
+```
+-   match decodeAux 10 bs with
++   match decodeAux 11 bs with
+```
+
+**Bits past the 64th kept** in `Protobuf/Varint.lean`:
+
+```
+- | some (v, rest) => some (v % 2 ^ 64, rest)
++ | some (v, rest) => some (v, rest)
+```
+
+**No LEN length limit** in `Protobuf/Wire.lean`:
+
+```
+- if 2 ^ 31 - 16 ≤ len ∨ (rest.take len).length < len then none
++ if (rest.take len).length < len then none
+```
+
+**A group start tag read as an empty LEN field** in `Protobuf/Wire.lean`:
+
+```
+-       | _ => none
++       | 3 => some (⟨n, .len []⟩, rest)
++       | _ => none
+```
+
+**isValid takes field number 2^29** in `Protobuf/Wire.lean`:
+
+```
+- 1 ≤ f.number && f.number < 2 ^ 29 &&
++ 1 ≤ f.number && f.number ≤ 2 ^ 29 &&
+```
+
+**CR kept at the end of a CR LF request** in `Main.lean`:
+
+```
+-     String.ofList (if cs.getLast? = some '\r' then cs.dropLast else cs)
++     String.ofList cs
+```
diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md
new file mode 100644
index 0000000..c3ee039
--- /dev/null
+++ b/tests/TEST-RESULTS.md
@@ -0,0 +1,16 @@
+# Test results
+
+Written by `tests/run_tests.py`. Rerun it to check these numbers.
+
+- Oracle: Python 3.13.17, protobuf 7.36.2 (upb), grpcio-tools 1.84.1 (protoc --decode_raw, C++)
+- Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release)
+- Seed: 20261025
+- Inputs: 200000
+- Mutated: 77017 of the inputs are mutated encodings
+- By kind: decode mutated 77017, decode random 18395, decode valid 46084, encode 46084, encode invalid 12402, error 18
+- Messages decoded: 141496, of which 73280 read by both reference parsers alike and 68216 refused
+- Refused although a reference parser reads them: a five-byte tag of 2^32 or more, which C++ reads and upb refuses 650, a group, which both read 981, field number 0, which upb reads and C++ refuses 1688
+- Malformed requests answered `error`: 18 of 18
+- Requests ending in CR LF: every seventh, 28571
+- Last lines sent alone, with no LF or with CR LF, answered right: 3 of 3
+- Failures: 0
diff --git a/tests/planted_bugs.py b/tests/planted_bugs.py
new file mode 100644
index 0000000..00431ee
--- /dev/null
+++ b/tests/planted_bugs.py
@@ -0,0 +1,140 @@
+#!/usr/bin/env python3
+"""Plant each bug below in a copy of the code, and check the tests catch it.
+
+A planted bug is a small change to the code, of a kind a person could
+make by mistake: to the code under proof, or to the request handling in
+Main.lean. For each one, this script copies the project into a temporary
+directory, makes the change there, builds the command-line tool, and
+runs the differential tests on a given number of inputs. The tests catch
+the bug when they report failures. A change that alters an answer of
+the code under proof also breaks the proofs, since that code no longer
+meets its statements; Main.lean is outside the proofs. This script checks the
+tests on their own, so it builds only the tool, not the proofs.
+
+The project itself is never changed. The script writes the results to
+tests/PLANTED-BUGS.md, and exits with 1 if a bug is not caught and its
+entry gives no reason. Some bugs no test here can catch: an equivalent
+change gives the same answer on every input, and some changes show only
+on an input too large to send. Such an entry says why the tests miss it.
+
+Usage: python3 tests/planted_bugs.py [--count N]
+"""
+
+import argparse
+import re
+import shutil
+import subprocess
+import sys
+import tempfile
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parent.parent
+EXE = "protowire"  # the lake target of the command-line tool
+COUNT = 20_000
+
+# (name, file, text to replace, replacement, why the tests cannot catch it or None)
+BUGS = [
+    ("Field number 0 read", "Protobuf/Wire.lean",
+     "if 2 ^ 32 ≤ t ∨ t / 8 = 0 then none",
+     "if 2 ^ 32 ≤ t then none", None),
+    ("Tags of 2^32 or more read", "Protobuf/Wire.lean",
+     "if 2 ^ 32 ≤ t ∨ t / 8 = 0 then none",
+     "if t / 8 = 0 then none", None),
+    ("A tag of exactly 2^32 read", "Protobuf/Wire.lean",
+     "if 2 ^ 32 ≤ t ∨ t / 8 = 0 then none",
+     "if 2 ^ 32 < t ∨ t / 8 = 0 then none", None),
+    ("Six-byte tags read", "Protobuf/Wire.lean",
+     "  match Varint.decodeAux 5 bs with",
+     "  match Varint.decodeAux 6 bs with", None),
+    ("Eleven-byte varints read", "Protobuf/Varint.lean",
+     "  match decodeAux 10 bs with",
+     "  match decodeAux 11 bs with", None),
+    ("Bits past the 64th kept", "Protobuf/Varint.lean",
+     "| some (v, rest) => some (v % 2 ^ 64, rest)",
+     "| some (v, rest) => some (v, rest)", None),
+    ("No LEN length limit", "Protobuf/Wire.lean",
+     "if 2 ^ 31 - 16 ≤ len ∨ (rest.take len).length < len then none",
+     "if (rest.take len).length < len then none",
+     "it shows only when a length of 2^31 - 16 or more is followed by that many bytes, "
+     "an input of about 2 GiB; a shorter input with such a length is refused for running "
+     "out of input either way. `Spec.decode_iff` covers the limit."),
+    ("A group start tag read as an empty LEN field", "Protobuf/Wire.lean",
+     "      | _ => none",
+     "      | 3 => some (⟨n, .len []⟩, rest)\n      | _ => none", None),
+    ("isValid takes field number 2^29", "Protobuf/Wire.lean",
+     "1 ≤ f.number && f.number < 2 ^ 29 &&",
+     "1 ≤ f.number && f.number ≤ 2 ^ 29 &&", None),
+    ("CR kept at the end of a CR LF request", "Main.lean",
+     "    String.ofList (if cs.getLast? = some '\\r' then cs.dropLast else cs)",
+     "    String.ofList cs", None),
+]
+
+
+def failures(out):
+    m = re.search(r"(\d+) failures?", out)
+    return int(m.group(1)) if m else None
+
+
+def run(count):
+    rows = []
+    with tempfile.TemporaryDirectory() as tmp:
+        work = Path(tmp) / "project"
+        shutil.copytree(ROOT, work, ignore=shutil.ignore_patterns(".git"))
+        for name, rel, old, new, missed in BUGS:
+            path = work / rel
+            original = (ROOT / rel).read_text()
+            if original.count(old) != 1:
+                sys.exit(f"{name}: the text to replace is not in {rel} exactly once")
+            path.write_text(original.replace(old, new))
+            build = subprocess.run(["lake", "build", EXE], cwd=work, capture_output=True, text=True)
+            if build.returncode != 0:
+                path.write_text(original)
+                sys.exit(f"{name}: the tool does not build with this change\n{build.stdout[-2000:]}")
+            test = subprocess.run([sys.executable, "tests/run_tests.py", "--count", str(count)],
+                                  cwd=work, capture_output=True, text=True)
+            path.write_text(original)
+            n = failures(test.stdout + test.stderr)
+            if n is None:
+                sys.exit(f"{name}: the tests gave no failure count\n{(test.stdout + test.stderr)[-2000:]}")
+            rows.append((name, rel, old, new, missed, n))
+            print(f"{name}: {n} failures", flush=True)
+    return rows
+
+
+def write(rows, count):
+    lines = [
+        "# Planted bugs",
+        "",
+        "Written by `python3 tests/planted_bugs.py`. Each row is one small change to the",
+        f"code, made in a copy. The tests ran on {count:,} inputs from their recorded seed",
+        "against the changed tool. A bug is caught when they report failures.",
+        "",
+        "| Bug | File | Failures |",
+        "|-----|------|----------|",
+    ]
+    for name, rel, _, _, missed, n in rows:
+        cell = str(n) if n else ("0, not caught by the tests: " + missed if missed
+                                 else "0, NOT CAUGHT")
+        lines.append(f"| {name} | `{rel}` | {cell} |")
+    lines += ["", "## The changes", ""]
+    for name, rel, old, new, _, _ in rows:
+        lines += [f"**{name}** in `{rel}`:", "", "```", "- " + old.replace("\n", "\n- "),
+                  "+ " + new.replace("\n", "\n+ "), "```", ""]
+    (ROOT / "tests" / "PLANTED-BUGS.md").write_text("\n".join(lines))
+
+
+def main():
+    ap = argparse.ArgumentParser(description=__doc__.splitlines()[0])
+    ap.add_argument("--count", type=int, default=COUNT)
+    args = ap.parse_args()
+    rows = run(args.count)
+    write(rows, args.count)
+    missed = [r[0] for r in rows if not r[5] and not r[4]]
+    caught = sum(1 for r in rows if r[5])
+    print(f"{caught} of {len(rows)} planted bugs caught; results in tests/PLANTED-BUGS.md")
+    if missed:
+        sys.exit("not caught: " + ", ".join(missed))
+
+
+if __name__ == "__main__":
+    main()
diff --git a/tests/run_tests.py b/tests/run_tests.py
new file mode 100644
index 0000000..7e0c85d
--- /dev/null
+++ b/tests/run_tests.py
@@ -0,0 +1,611 @@
+#!/usr/bin/env python3
+"""Differential tests: the Lean wire format codec against the reference
+Protobuf parsers.
+
+There are two oracles, both from Google's Protobuf releases:
+
+- upb, the parser behind Python's `protobuf` package. A message is read
+  as `google.protobuf.Empty`, so every field lands in its unknown field
+  set, which gives the field numbers, wire types and raw values.
+- The C++ parser behind `protoc --decode_raw`, run in-process through
+  `grpcio-tools`. It gives whether the bytes parse, and the top-level
+  field numbers and numeric values.
+
+The encoder is compared with `google.protobuf.internal.encoder`.
+
+Where the two parsers disagree, the Lean decoder must take the stricter
+reading and refuse the input. They differ in two known ways: upb reads
+field number 0, which the C++ parser refuses, and the C++ parser reads a
+five-byte tag of 2^32 or more by dropping the high bits, which upb
+refuses. Groups (wire types 3 and 4) are outside this library, so a
+message that both parsers read but that holds a group must be refused.
+The record counts each case.
+
+Inputs come from a recorded seed:
+
+- random field lists, weighted toward boundary field numbers and
+  values, encoded and decoded;
+- mutations of those encodings: a byte changed, dropped, added or
+  flipped, the message cut short or extended, a varint rewritten longer
+  than it needs to be (up to and past ten bytes), a tag with field
+  number 0, a group, wire type 6 or 7, or a tag of 2^32 or more;
+- random short byte strings;
+- field lists the encoder must refuse;
+- malformed requests, which the tool must answer with `error`.
+
+Every seventh request ends in CR LF. For every input the Lean answer
+must equal the oracle's, and the two parsers must disagree only in the
+known ways.
+
+    python3 tests/run_tests.py [--seed N] [--count N]
+
+It needs `protobuf` and `grpcio-tools` at the versions below, with
+protobuf on its upb backend. When they are missing it creates a virtual environment in `.lake/oracle-venv`,
+installs them there, and runs itself again with it; where Python cannot
+make one, it installs them into `.lake/oracle-packages` instead. It builds the
+executable, writes tests/TEST-RESULTS.md, and exits non-zero if any
+input disagrees.
+"""
+
+import argparse
+import itertools
+import os
+import platform
+import random
+import re
+import struct
+import subprocess
+import sys
+import tempfile
+import threading
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parent.parent
+EXE = ROOT / ".lake" / "build" / "bin" / "protowire"
+RESULTS = ROOT / "tests" / "TEST-RESULTS.md"
+VENV = ROOT / ".lake" / "oracle-venv"
+PKGS = ROOT / ".lake" / "oracle-packages"
+PINS = ["protobuf==7.36.2", "grpcio-tools==1.84.1"]
+TIMEOUT = 1800
+BUILD_TIMEOUT = 3600
+
+
+def ensure_oracles():
+    """Import the oracles. When this Python lacks them, install the pinned
+    versions into a virtual environment and run again with it; where a
+    virtual environment cannot be made, install them into a folder
+    instead and import them from there."""
+    if oracles_ready():
+        return
+    if os.environ.get("PROTOWIRE_ORACLE_VENV"):
+        sys.exit("the pinned oracle packages, with the upb backend, are not usable even in "
+                 ".lake/oracle-venv")
+    python = VENV / "bin" / "python"
+    made = python.exists() or subprocess.run(
+        [sys.executable, "-m", "venv", str(VENV)], capture_output=True).returncode == 0
+    if made and not os.environ.get("PROTOWIRE_NO_VENV"):
+        subprocess.run([str(python), "-m", "pip", "install", "--quiet", *PINS], check=True)
+        env = dict(os.environ, PROTOWIRE_ORACLE_VENV="1")
+        env.pop("PROTOCOL_BUFFERS_PYTHON_IMPLEMENTATION", None)
+        os.execve(str(python), [str(python), *sys.argv], env)
+    subprocess.run([sys.executable, "-m", "pip", "install", "--quiet", "--break-system-packages",
+                    "--target", str(PKGS), *PINS], check=True)
+    sys.path.insert(0, str(PKGS))
+    os.environ.pop("PROTOCOL_BUFFERS_PYTHON_IMPLEMENTATION", None)
+    for name in [m for m in sys.modules if m.startswith(("google", "grpc_tools"))]:
+        del sys.modules[name]
+    if not oracles_ready():
+        sys.exit("the pinned oracle packages, with the upb backend, are not usable")
+
+
+def oracles_ready():
+    """Whether the pinned oracle versions import, with protobuf on upb."""
+    from importlib.metadata import PackageNotFoundError, version
+    try:
+        import grpc_tools  # noqa: F401
+        from google.protobuf.internal import api_implementation
+        versions = [f"{p.split('==')[0]}=={version(p.split('==')[0])}" for p in PINS]
+    except (ImportError, PackageNotFoundError):
+        return False
+    return versions == PINS and api_implementation.Type() == "upb"
+
+
+# The oracles.
+
+def upb_decode(data):
+    """upb's reading: a list of (number, kind, value), or None."""
+    from google.protobuf import empty_pb2
+    from google.protobuf.message import DecodeError
+    from google.protobuf.unknown_fields import UnknownFieldSet
+    try:
+        msg = empty_pb2.Empty.FromString(data)
+    except DecodeError:
+        return None
+    fields = []
+    for f in UnknownFieldSet(msg):
+        kind = {0: "varint", 1: "i64", 2: "len", 3: "group", 5: "i32"}[f.wire_type]
+        value = f.data.hex() if kind == "len" else (None if kind == "group" else f.data)
+        fields.append((f.field_number, kind, value))
+    return fields
+
+
+def cpp_decode_raw(data):
+    """The C++ parser's reading through `protoc --decode_raw`: the text it
+    prints, or None when it refuses the input."""
+    from grpc_tools import _protoc_compiler
+    with tempfile.TemporaryFile() as fin, tempfile.TemporaryFile() as fout, \
+            tempfile.TemporaryFile() as ferr:
+        fin.write(data)
+        fin.flush()
+        fin.seek(0)
+        saved = [os.dup(0), os.dup(1), os.dup(2)]
+        try:
+            os.dup2(fin.fileno(), 0)
+            os.dup2(fout.fileno(), 1)
+            os.dup2(ferr.fileno(), 2)
+            code = _protoc_compiler.run_main([b"protoc", b"--decode_raw"])
+        finally:
+            for fd, s in zip((0, 1, 2), saved):
+                os.dup2(s, fd)
+                os.close(s)
+        fout.seek(0)
+        return fout.read().decode("utf-8", "backslashreplace") if code == 0 else None
+
+
+TOP_VALUE = re.compile(r"(\d+): (.*)")
+OPEN_LINE = re.compile(r" *\d+ \{")
+
+
+def cpp_top_level(text):
+    """The top-level (number, value text) pairs of `--decode_raw` output."""
+    out, depth = [], 0
+    for line in text.splitlines():
+        # A nested message opens with a line `N {` and closes with a
+        # line `}`; braces inside a quoted string are not structure.
+        opens = OPEN_LINE.fullmatch(line) is not None
+        if depth == 0:
+            m = TOP_VALUE.fullmatch(line)
+            if opens:
+                out.append((int(line.split(" ")[0]), "{"))
+            elif m:
+                out.append((int(m.group(1)), m.group(2)))
+        if opens:
+            depth += 1
+        elif line.strip() == "}":
+            depth -= 1
+    return out
+
+
+def cpp_agrees(fields, text):
+    """Whether the C++ reading has the same field numbers, in order, and
+    the same numeric values."""
+    top = cpp_top_level(text)
+    if [n for n, _ in top] != [n for n, _, _ in fields]:
+        return False
+    for (n, kind, value), (_, shown) in zip(fields, top):
+        if kind == "varint" and shown != str(value):
+            return False
+        if kind == "i32" and shown != f"0x{value:08x}":
+            return False
+        if kind == "i64" and shown != f"0x{value:016x}":
+            return False
+    return True
+
+
+def oracle_encode(fields):
+    from google.protobuf.internal import encoder
+    out = b""
+    for n, kind, value in fields:
+        wt = {"varint": 0, "i64": 1, "len": 2, "i32": 5}[kind]
+        out += encoder.TagBytes(n, wt)
+        if kind == "varint":
+            out += encoder._VarintBytes(value)
+        elif kind == "i64":
+            out += struct.pack("<Q", value)
+        elif kind == "i32":
+            out += struct.pack("<I", value)
+        else:
+            data = bytes.fromhex(value)
+            out += encoder._VarintBytes(len(data)) + data
+    return out
+
+
+def show(fields):
+    return "\t".join(["OK"] + [f"{n}:{k}:{v}" for n, k, v in fields])
+
+
+# Four bytes with the high bit set, then a last byte with bits above the
+# 32nd: a five-byte varint of 2^32 or more.
+BIG_TAG = re.compile(rb"[\x80-\xff]{4}[\x10-\x7f]")
+
+
+def expected_decode(data, tally):
+    """The answer the Lean decoder must give, and why, by the rule in the
+    module comment."""
+    u = upb_decode(data)
+    c = cpp_decode_raw(data)
+    if u is None and c is None:
+        return "REJECT", "both refuse"
+    if u is None or c is None:
+        if c is None:
+            reason = ("field number 0, which upb reads and C++ refuses"
+                      if any(n == 0 for n, _, _ in u) else "other inputs upb reads and C++ refuses")
+        else:
+            reason = ("a five-byte tag of 2^32 or more, which C++ reads and upb refuses"
+                      if BIG_TAG.search(data) else "other inputs C++ reads and upb refuses")
+        tally[reason] = tally.get(reason, 0) + 1
+        return "REJECT", reason
+    if any(k == "group" for _, k, _ in u):
+        tally["a group, which both read"] = tally.get("a group, which both read", 0) + 1
+        return "REJECT", "group"
+    if not cpp_agrees(u, c):
+        tally["C++ and upb read different fields"] = \
+            tally.get("C++ and upb read different fields", 0) + 1
+        return "REJECT", "references differ"
+    return show(u), "both read"
+
+
+# Generators.
+
+def varint(n):
+    out = bytearray()
+    while True:
+        b = n & 0x7F
+        n >>= 7
+        if n:
+            out.append(b | 0x80)
+        else:
+            out.append(b)
+            return bytes(out)
+
+
+def long_varint(n, size):
+    """`n` as a varint of exactly `size` bytes, padded with zero groups."""
+    groups = []
+    for _ in range(size):
+        groups.append(n & 0x7F)
+        n >>= 7
+    return bytes([g | 0x80 for g in groups[:-1]] + [groups[-1]])
+
+
+def random_number(rng):
+    r = rng.random()
+    if r < 0.6:
+        return rng.randint(1, 15)
+    if r < 0.8:
+        return rng.choice([1, 15, 16, 2047, 2048, 262143, 262144, 2 ** 29 - 1, 19000, 19999])
+    return rng.randint(1, 2 ** 29 - 1)
+
+
+def random_u(rng, bits):
+    r = rng.random()
+    if r < 0.3:
+        return rng.randint(0, 300)
+    if r < 0.6:
+        k = rng.randint(1, bits)
+        return rng.choice([2 ** k - 1, 2 ** (k - 1), 2 ** k - 2]) % 2 ** bits
+    return rng.getrandbits(bits)
+
+
+def random_field(rng):
+    kind = rng.choice(["varint", "varint", "len", "len", "i64", "i32"])
+    n = random_number(rng)
+    if kind == "varint":
+        return (n, kind, random_u(rng, 64))
+    if kind == "i64":
+        return (n, kind, random_u(rng, 64))
+    if kind == "i32":
+        return (n, kind, random_u(rng, 32))
+    size = rng.choice([0, 1, 3, 7, rng.randint(0, 40), rng.randint(0, 40), rng.randint(120, 300)])
+    return (n, kind, bytes(rng.getrandbits(8) for _ in range(size)).hex())
+
+
+def random_fields(rng):
+    return [random_field(rng) for _ in range(rng.choice([0, 1, 1, 2, 3, 5, 8]))]
+
+
+def mutate(rng, data):
+    b = bytearray(data)
+    op = rng.randrange(11)
+    if op == 0 and b:
+        b[rng.randrange(len(b))] = rng.getrandbits(8)
+    elif op == 1 and b:
+        del b[rng.randrange(len(b))]
+    elif op == 2:
+        b.insert(rng.randint(0, len(b)), rng.getrandbits(8))
+    elif op == 3 and b:
+        b[rng.randrange(len(b))] ^= 1 << rng.randrange(8)
+    elif op == 4 and b:
+        b = b[: rng.randrange(len(b))]
+    elif op == 5:
+        b += bytes(rng.getrandbits(8) for _ in range(rng.randint(1, 4)))
+    elif op == 6:
+        # A record whose tag is longer than it needs to be, up to and
+        # past five bytes, in front.
+        n, wt = random_number(rng), rng.choice([0, 0, 2, 5])
+        payload = {0: varint(rng.randint(0, 300)), 2: b"\x01a", 5: b"\x00" * 4}[wt]
+        size = rng.randint(len(varint(n * 8 + wt)), 7)
+        b = bytearray(long_varint(n * 8 + wt, size) + payload) + b
+    elif op == 7:
+        # A varint value longer than it needs to be, up to and past ten bytes.
+        size = rng.randint(1, 12)
+        v = rng.getrandbits(min(64, 7 * size))
+        b += varint(random_number(rng) * 8) + long_varint(v, size)
+        if rng.random() < 0.3:
+            b[-1] = rng.choice([0x01, 0x02, 0x7F, 0x80])
+    elif op == 8:
+        # Field number 0, a group, or wire type 6 or 7.
+        wt = rng.choice([0, 3, 4, 6, 7])
+        n = 0 if wt == 0 else random_number(rng)
+        rec = varint(n * 8 + wt) + (varint(1) if wt == 0 else b"")
+        if wt == 3 and rng.random() < 0.7:
+            rec += varint(random_number(rng) * 8) + varint(5) + varint(n * 8 + 4)
+        b = bytearray(rec) + b
+    elif op == 9:
+        # A five-byte tag of 2^32 or more, often exactly 2^32 plus a wire
+        # type: field number 2^29, one past the largest.
+        t = rng.choice([2 ** 32 + rng.choice([0, 1, 2, 5]), rng.randint(2 ** 32, 2 ** 35 - 1)])
+        b = bytearray(long_varint(t, 5) + varint(1)) + b
+    else:
+        # A length varint longer than it needs to be, or past the end.
+        data_ = bytes(rng.getrandbits(8) for _ in range(rng.randint(0, 5)))
+        size = rng.randint(1, 7)
+        claimed = len(data_) + rng.choice([0, 0, 1, -1 if data_ else 0, 2 ** 31])
+        b += varint(random_number(rng) * 8 + 2) + long_varint(claimed, max(size, len(varint(claimed)))) + data_
+    return bytes(b)
+
+
+def invalid_fields(rng):
+    fields = random_fields(rng) or [random_field(rng)]
+    i = rng.randrange(len(fields))
+    n, kind, value = fields[i]
+    which = rng.randrange(4)
+    if which == 0:
+        n = 0
+    elif which == 1:
+        n = rng.choice([2 ** 29, 2 ** 29 + 1, 2 ** 29 + rng.randint(0, 1000), 2 ** 32])
+    elif kind == "varint" or kind == "i64":
+        value = rng.choice([2 ** 64, 2 ** 64 + 1, 2 ** 64 + rng.randint(0, 2 ** 20)])
+    elif kind == "i32":
+        value = rng.choice([2 ** 32, 2 ** 32 + 1, 2 ** 32 + rng.randint(0, 2 ** 20)])
+    else:
+        n = 0
+    fields[i] = (n, kind, value)
+    return fields
+
+
+MALFORMED = [
+    ("frob 00", "unknown operation"),
+    ("DECODE 00", "operations are lower case"),
+    ("decode", "no argument"),
+    ("decode 0", "an odd number of hex digits"),
+    ("decode 0g", "not a hex digit"),
+    ("decode 0A", "hex digits are lower case"),
+    ("decode 00 00", "two arguments"),
+    ("encode", "no argument"),
+    ("encode 1:varint", "a field item without a value"),
+    ("encode 1:float:1", "an unknown kind"),
+    ("encode 1:varint:-1", "a negative number"),
+    ("encode 1:varint:1,", "an empty item"),
+    ("encode 1:len:0", "odd hex in a len value"),
+    ("encode x:varint:1", "a field number that is not a number"),
+    (" decode 00", "a leading space"),
+    ("", "an empty line"),
+    ("decode 0896\r01", "a CR inside the request"),
+    ("encode 1:varint:" + "1" * 31, "a number of more than 30 digits"),
+]
+
+AT_EOF = [("decode 089601", "OK\t1:varint:150"), ("encode 1:varint:150", "089601"),
+          ("decode 089601\r\n", "OK\t1:varint:150")]
+
+
+def fields_text(fields):
+    return ",".join(f"{n}:{k}:{v}" for n, k, v in fields) if fields else "-"
+
+
+def cases(seed, count, tally):
+    """(label, request, expected answer, mutated) for each input."""
+    rng = random.Random(seed)
+    made = 0
+    for req, _ in MALFORMED:
+        if made < count:
+            yield ("error", req, "error", False)
+            made += 1
+    while made < count:
+        r = rng.random()
+        if r < 0.3:
+            fields = random_fields(rng)
+            data = oracle_encode(fields)
+            yield ("encode", f"encode {fields_text(fields)}", data.hex(), False)
+            want, _ = expected_decode(data, tally)
+            yield ("decode valid", f"decode {data.hex()}", want, False)
+            made += 2
+        elif r < 0.8:
+            base = oracle_encode(random_fields(rng))
+            data = mutate(rng, base)
+            while data == base:
+                data = mutate(rng, base)
+            want, _ = expected_decode(data, tally)
+            yield ("decode mutated", f"decode {data.hex()}", want, True)
+            made += 1
+        elif r < 0.92:
+            data = bytes(rng.getrandbits(8) for _ in range(rng.randint(0, 12)))
+            want, _ = expected_decode(data, tally)
+            yield ("decode random", f"decode {data.hex()}", want, False)
+            made += 1
+        else:
+            yield ("encode invalid", f"encode {fields_text(invalid_fields(rng))}", "INVALID", False)
+            made += 1
+
+
+def run_tool(data, timeout=TIMEOUT):
+    """The tool's answer lines for `data`, and a note on how the run
+    failed, or None."""
+    raw = data.encode("utf-8")
+    limit = 2 * len(raw) + 64 * (data.count("\n") + 1)
+    try:
+        proc = subprocess.Popen([str(EXE), "serve"], stdin=subprocess.PIPE,
+                                stdout=subprocess.PIPE, stderr=subprocess.PIPE)
+    except OSError as e:
+        return [], f"could not run {EXE.relative_to(ROOT)}: {e.strerror or e}"
+    out, err = bytearray(), bytearray()
+
+    def feed():
+        try:
+            proc.stdin.write(raw)
+            proc.stdin.close()
+        except (BrokenPipeError, ValueError):
+            pass
+
+    def drain(stream, buf, cap):
+        while chunk := stream.read1(1 << 16):
+            buf += chunk
+            if len(buf) > cap:
+                proc.kill()
+                return
+
+    threads = [threading.Thread(target=feed),
+               threading.Thread(target=drain, args=(proc.stdout, out, limit)),
+               threading.Thread(target=drain, args=(proc.stderr, err, 1 << 20))]
+    for t in threads:
+        t.start()
+    problem = None
+    try:
+        proc.wait(timeout=timeout)
+    except subprocess.TimeoutExpired:
+        proc.kill()
+        problem = f"no end after {timeout} seconds"
+    for t in threads:
+        t.join()
+    proc.wait()
+    if len(out) > limit:
+        problem = problem or f"more than {limit} bytes of output, stopped"
+    elif proc.returncode != 0 and not problem:
+        tail = " / ".join(err.decode("utf-8", "backslashreplace").splitlines()[-3:])
+        problem = f"exit status {proc.returncode}: {tail}"
+    text = bytes(out).decode("utf-8", "backslashreplace")
+    if text and not text.endswith("\n"):
+        problem = problem or "the last answer has no LF"
+    lines = text.split("\n")
+    if lines and lines[-1] == "":
+        lines.pop()
+    return lines, problem
+
+
+def oracle():
+    from importlib.metadata import version
+    from google.protobuf.internal import api_implementation
+    return (f"Python {platform.python_version()}, protobuf {version('protobuf')} "
+            f"({api_implementation.Type()}), "
+            f"grpcio-tools {version('grpcio-tools')} (protoc --decode_raw, C++)")
+
+
+def lean_version():
+    try:
+        out = subprocess.run(["lake", "env", "lean", "--version"], cwd=ROOT,
+                             capture_output=True, text=True, errors="backslashreplace",
+                             timeout=300)
+        first = out.stdout.strip().splitlines()[:1]
+        return first[0] if first else "unknown"
+    except (OSError, subprocess.TimeoutExpired):
+        return "unknown"
+
+
+def count(text):
+    n = int(text)
+    if n < 1:
+        raise argparse.ArgumentTypeError("the count must be at least 1")
+    return n
+
+
+def write(lines):
+    RESULTS.write_text("\n".join(lines), encoding="utf-8")
+
+
+def main():
+    ap = argparse.ArgumentParser()
+    ap.add_argument("--seed", type=int, default=20261025)
+    ap.add_argument("--count", type=count, default=200_000)
+    args = ap.parse_args()
+    ensure_oracles()
+
+    try:
+        build = subprocess.run(["lake", "build", "protowire"], cwd=ROOT, capture_output=True,
+                               text=True, errors="backslashreplace", timeout=BUILD_TIMEOUT)
+        built, log = build.returncode == 0, build.stdout + build.stderr
+    except (OSError, subprocess.TimeoutExpired) as e:
+        built, log = False, str(e)
+    if not built:
+        write(["# Test results", "", f"- Oracle: {oracle()}", f"- Seed: {args.seed}",
+               "- Inputs: 0", "- Failures: 1 (`lake build protowire` failed)", ""])
+        sys.exit("lake build protowire failed:\n" + log)
+
+    tally = {}
+    items = list(cases(args.seed, args.count, tally))
+    # Every seventh request ends in CR LF, which the tool must take as LF.
+    out, problem = run_tool("".join(req + ("\r\n" if i % 7 == 6 else "\n")
+                                    for i, (_, req, _, _) in enumerate(items)))
+    failures = [("(whole run)", "a clean run", problem)] if problem else []
+    for item, got in itertools.zip_longest(items, out):
+        if item is None:
+            failures.append(("(no request)", "nothing", got))
+        elif got != item[2]:
+            failures.append((item[1], item[2], "(no answer)" if got is None else got))
+    # The two parsers may disagree only in the ways the module comment
+    # names; any other disagreement means an oracle changed.
+    for reason, n in tally.items():
+        if reason.startswith("other") or reason.startswith("C++ and upb read different"):
+            failures.append((f"{n} inputs", "only the known disagreements", reason))
+
+    eof_right = 0
+    for req, want in AT_EOF:
+        got, problem = run_tool(req, timeout=60)
+        if got == [want] and not problem:
+            eof_right += 1
+        else:
+            failures.append((req + " (at end of input)", want, f"{got} {problem or ''}".strip()))
+
+    by_label = {}
+    for label, _, _, _ in items:
+        by_label[label] = by_label.get(label, 0) + 1
+    decodes = [want for label, req, want, _ in items if label.startswith("decode")]
+    accepted = sum(1 for w in decodes if w.startswith("OK"))
+    mutated = sum(1 for item in items if item[3])
+    malformed = [got for item, got in zip(items, out) if item[0] == "error"]
+
+    lines = [
+        "# Test results",
+        "",
+        "Written by `tests/run_tests.py`. Rerun it to check these numbers.",
+        "",
+        f"- Oracle: {oracle()}",
+        f"- Lean: {lean_version()}",
+        f"- Seed: {args.seed}",
+        f"- Inputs: {len(items)}",
+        f"- Mutated: {mutated} of the inputs are mutated encodings",
+        "- By kind: " + ", ".join(f"{k} {v}" for k, v in sorted(by_label.items())),
+        f"- Messages decoded: {len(decodes)}, of which {accepted} read by both reference "
+        f"parsers alike and {len(decodes) - accepted} refused",
+        "- Refused although a reference parser reads them: " +
+        (", ".join(f"{k} {v}" for k, v in sorted(tally.items())) or "none"),
+        f"- Malformed requests answered `error`: {malformed.count('error')} of "
+        f"{by_label.get('error', 0)}",
+        f"- Requests ending in CR LF: every seventh, {len(items) // 7}",
+        f"- Last lines sent alone, with no LF or with CR LF, answered right: {eof_right} of "
+        f"{len(AT_EOF)}",
+        f"- Failures: {len(failures)}",
+        "",
+    ]
+    if failures:
+        lines += ["## Failures", ""]
+        lines += [f"- `{req[:160]!r}`: expected `{want[:120]!r}`, got `{got[:120]!r}`"
+                  for req, want, got in failures[:50]]
+        lines.append("")
+    write(lines)
+    agree = sum(1 for item, got in zip(items, out) if got == item[2])
+    print(f"{agree}/{len(items)} inputs agree, {len(failures)} failures; results in {RESULTS}")
+    return 1 if failures else 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())