diff --git a/README.md b/README.md
index 61d80b973..4595db3af 100644
--- a/README.md
+++ b/README.md
@@ -129,13 +129,13 @@ yours to keep:
 
 <td>✅</td>
 
-<td>❌</td>
+<td>✅ SHA extensions, AVX2, BMI1, BMI2</td>
 
-<td>❌</td>
+<td>✅ SHA extensions</td>
 
-<td>❌</td>
+<td>✅</td>
 
-<td>❌</td>
+<td>✅</td>
 
 </tr>
 
diff --git a/bench/benches/primitives/main.rs b/bench/benches/primitives/main.rs
index 787c57cc9..1955098e5 100644
--- a/bench/benches/primitives/main.rs
+++ b/bench/benches/primitives/main.rs
@@ -40,6 +40,7 @@ mod poly1305;
 mod rc2_cbc;
 mod scrypt;
 mod sha1;
+mod sha224;
 mod sha256;
 mod sha3;
 mod sha512;
@@ -211,6 +212,7 @@ const BENCHES: &[Bench] = &[
     (rc2_cbc::USES, rc2_cbc::bench),
     (scrypt::USES, scrypt::bench),
     (sha1::USES, sha1::bench),
+    (sha224::USES, sha224::bench),
     (sha256::USES, sha256::bench),
     (sha3::USES, sha3::bench),
     (sha512::USES, sha512::bench),
diff --git a/bench/benches/primitives/sha224.rs b/bench/benches/primitives/sha224.rs
new file mode 100644
index 000000000..67000f877
--- /dev/null
+++ b/bench/benches/primitives/sha224.rs
@@ -0,0 +1,15 @@
+//! SHA-224.
+
+use criterion::Criterion;
+use openssl::hash::MessageDigest;
+use verified_garbage::hashes::sha224::Sha224;
+
+use crate::hash_group;
+
+/// The library modules whose code these benchmarks run (see
+/// `ci/bench_arches.py`).
+pub const USES: &[&str] = &["sha224", "sha256"];
+
+pub fn bench(c: &mut Criterion) {
+    hash_group(c, "sha224", Sha224::digest, MessageDigest::sha224());
+}
diff --git a/lean/VerifiedGarbage/Artifacts/Sha224/AArch64.lean b/lean/VerifiedGarbage/Artifacts/Sha224/AArch64.lean
new file mode 100644
index 000000000..7ea87cf7b
--- /dev/null
+++ b/lean/VerifiedGarbage/Artifacts/Sha224/AArch64.lean
@@ -0,0 +1,32 @@
+import VerifiedGarbage.TCB.AArch64.Target
+import VerifiedGarbage.Proof.Sha256.AArch64.Shared
+
+/-!
+# SHA-224 (FIPS 180-4) on AArch64
+
+A registration file (see `TCB/Emit.lean`): the artifacts it lists are
+emitted. **Review note**: `sig` and `doc` are trusted, as they tie the Rust
+caller to the contract; check them against the contract's `pre`/`post`. An
+artifact made from a function's `Api` (in `Spec/`, reviewed with the
+contract) takes them from there, and this file adds only notes on the
+implementation. The emitter adds the `# Safety` items that depend on the
+target (`Sig.layoutDoc`), from `stack` and `writeArgs`, which `ofSig` checks
+against the contract.
+
+SHA-224 is SHA-256 from another initial hash value: only its `init` is its
+own, and it continues with SHA-256's `update` and `finalize`
+(`Artifacts/Sha256/`).
+-/
+
+namespace VG.Artifacts.Sha224.AArch64
+
+def artifacts : List Artifact := [
+  { Spec.Sha256.init224Api with
+    target := AArch64.target
+    doc := Spec.Sha256.init224Api.doc
+    code := Impl.Sha256.AArch64.Stream.init224
+    contract := Spec.Sha256.init224Contract AArch64.abi
+    verified := Proof.Sha256.AArch64.Shared.init224
+    spSafe := Code.all_of_forall (fun _ => rfl) _ }]
+
+end VG.Artifacts.Sha224.AArch64
diff --git a/lean/VerifiedGarbage/Artifacts/Sha224/Arm.lean b/lean/VerifiedGarbage/Artifacts/Sha224/Arm.lean
new file mode 100644
index 000000000..7d0bc7d3c
--- /dev/null
+++ b/lean/VerifiedGarbage/Artifacts/Sha224/Arm.lean
@@ -0,0 +1,32 @@
+import VerifiedGarbage.TCB.Arm.Target
+import VerifiedGarbage.Proof.Sha256.Arm.Shared
+
+/-!
+# SHA-224 (FIPS 180-4) on ARMv7
+
+A registration file (see `TCB/Emit.lean`): the artifacts it lists are
+emitted. **Review note**: `sig` and `doc` are trusted, as they tie the Rust
+caller to the contract; check them against the contract's `pre`/`post`. An
+artifact made from a function's `Api` (in `Spec/`, reviewed with the
+contract) takes them from there, and this file adds only notes on the
+implementation. The emitter adds the `# Safety` items that depend on the
+target (`Sig.layoutDoc`), from `stack` and `writeArgs`, which `ofSig` checks
+against the contract.
+
+SHA-224 is SHA-256 from another initial hash value: only its `init` is its
+own, and it continues with SHA-256's `update` and `finalize`
+(`Artifacts/Sha256/`).
+-/
+
+namespace VG.Artifacts.Sha224.Arm
+
+def artifacts : List Artifact := [
+  { Spec.Sha256.init224Api with
+    target := Arm.target
+    doc := Spec.Sha256.init224Api.doc
+    code := Impl.Sha256.Arm.Stream.init224
+    contract := Spec.Sha256.init224Contract Arm.abi
+    verified := Proof.Sha256.Arm.Shared.init224
+    spSafe := Code.all_of_forall (fun _ => rfl) _ }]
+
+end VG.Artifacts.Sha224.Arm
diff --git a/lean/VerifiedGarbage/Artifacts/Sha224/X86.lean b/lean/VerifiedGarbage/Artifacts/Sha224/X86.lean
new file mode 100644
index 000000000..f76753663
--- /dev/null
+++ b/lean/VerifiedGarbage/Artifacts/Sha224/X86.lean
@@ -0,0 +1,32 @@
+import VerifiedGarbage.TCB.X86.Target
+import VerifiedGarbage.Proof.Sha256.X86.Shared
+
+/-!
+# SHA-224 (FIPS 180-4) on x86 (32-bit)
+
+A registration file (see `TCB/Emit.lean`): the artifacts it lists are
+emitted. **Review note**: `sig` and `doc` are trusted, as they tie the Rust
+caller to the contract; check them against the contract's `pre`/`post`. An
+artifact made from a function's `Api` (in `Spec/`, reviewed with the
+contract) takes them from there, and this file adds only notes on the
+implementation. The emitter adds the `# Safety` items that depend on the
+target (`Sig.layoutDoc`), from `stack` and `writeArgs`, which `ofSig` checks
+against the contract.
+
+SHA-224 is SHA-256 from another initial hash value: only its `init` is its
+own, and it continues with SHA-256's `update` and `finalize`
+(`Artifacts/Sha256/`).
+-/
+
+namespace VG.Artifacts.Sha224.X86
+
+def artifacts : List Artifact := [
+  { Spec.Sha256.init224Api with
+    target := X86.target
+    doc := Spec.Sha256.init224Api.doc
+    code := Impl.Sha256.X86.Stream.init224
+    contract := Spec.Sha256.init224Contract X86.abi
+    verified := Proof.Sha256.X86.Shared.init224
+    spSafe := Code.all_of_allInstrs (by lit_decide) }]
+
+end VG.Artifacts.Sha224.X86
diff --git a/lean/VerifiedGarbage/Artifacts/Sha224/X86_64.lean b/lean/VerifiedGarbage/Artifacts/Sha224/X86_64.lean
new file mode 100644
index 000000000..a81acd919
--- /dev/null
+++ b/lean/VerifiedGarbage/Artifacts/Sha224/X86_64.lean
@@ -0,0 +1,32 @@
+import VerifiedGarbage.TCB.X86_64.Target
+import VerifiedGarbage.Proof.Sha256.X86_64.Shared
+
+/-!
+# SHA-224 (FIPS 180-4) on x86-64
+
+A registration file (see `TCB/Emit.lean`): the artifacts it lists are
+emitted. **Review note**: `sig` and `doc` are trusted, as they tie the Rust
+caller to the contract; check them against the contract's `pre`/`post`. An
+artifact made from a function's `Api` (in `Spec/`, reviewed with the
+contract) takes them from there, and this file adds only notes on the
+implementation. The emitter adds the `# Safety` items that depend on the
+target (`Sig.layoutDoc`), from `stack` and `writeArgs`, which `ofSig` checks
+against the contract.
+
+SHA-224 is SHA-256 from another initial hash value: only its `init` is its
+own, and it continues with SHA-256's `update` and `finalize`
+(`Artifacts/Sha256/`).
+-/
+
+namespace VG.Artifacts.Sha224.X86_64
+
+def artifacts : List Artifact := [
+  { Spec.Sha256.init224Api with
+    target := X86_64.target
+    doc := Spec.Sha256.init224Api.doc
+    code := Impl.Sha256.X86_64.Stream.init224
+    contract := Spec.Sha256.init224Contract X86_64.abi
+    verified := Proof.Sha256.X86_64.Shared.init224
+    spSafe := Code.all_of_allInstrs (by lit_decide) }]
+
+end VG.Artifacts.Sha224.X86_64
diff --git a/lean/VerifiedGarbage/Impl/Sha256/AArch64/Stream.lean b/lean/VerifiedGarbage/Impl/Sha256/AArch64/Stream.lean
index 7f0b4de97..faaa88c17 100644
--- a/lean/VerifiedGarbage/Impl/Sha256/AArch64/Stream.lean
+++ b/lean/VerifiedGarbage/Impl/Sha256/AArch64/Stream.lean
@@ -7,7 +7,7 @@ import VerifiedGarbage.Impl.MdStream.AArch64
 The streaming state (96 bytes at `state`) is the hash value followed by a
 64-byte buffer (see `VG.Spec.Sha256.Repr`).
 
-* `init(state = x0)` stores `H⁽⁰⁾`.
+* `init(state = x0)` stores `H⁽⁰⁾` (`init224`, SHA-224's).
 * `update` and `finalize` are the generic streaming code
   (`Impl/MdStream/AArch64.lean`), calling the compression function
   (`vg_sha256_compress`) with `scratch[0..112)` as its scratch space, and
@@ -25,12 +25,19 @@ open VG.Impl.Sha256.AArch64 (compress)
 /-- `mov d, n` (as `add d, n, #0`). -/
 def mov (d n : Reg) : Instr := .addImm .x d n 0
 
-def init : Prog isa :=
+/-- Stores the initial hash value `iv`. -/
+def initWith (iv : Spec.Sha256.HashValue) : Prog isa :=
   .block ((List.range 8).flatMap fun k =>
-    [.movz .w .x9 (Spec.Sha256.H0[k]!.extractLsb' 0 16) 0,
-     .movk .w .x9 (Spec.Sha256.H0[k]!.extractLsb' 16 16) 1,
+    [.movz .w .x9 (iv[k]!.extractLsb' 0 16) 0,
+     .movk .w .x9 (iv[k]!.extractLsb' 16 16) 1,
      .str .w .x9 .x0 (4 * k)])
 
+/-- `vg_sha256_init`. -/
+def init : Prog isa := initWith Spec.Sha256.H0
+
+/-- `vg_sha224_init`. -/
+def init224 : Prog isa := initWith Spec.Sha256.H0_224
+
 /-- The callee-saved registers we use, and where they are saved in `scratch`. -/
 def saved : List (Reg × Nat) :=
   [(.x19, 112), (.x20, 120), (.x21, 128), (.x22, 136), (.x23, 144), (.x24, 152)]
diff --git a/lean/VerifiedGarbage/Impl/Sha256/Arm/Stream.lean b/lean/VerifiedGarbage/Impl/Sha256/Arm/Stream.lean
index d09d79ccd..43c515dd3 100644
--- a/lean/VerifiedGarbage/Impl/Sha256/Arm/Stream.lean
+++ b/lean/VerifiedGarbage/Impl/Sha256/Arm/Stream.lean
@@ -7,7 +7,7 @@ import VerifiedGarbage.Impl.MdStream.Arm
 The streaming state (96 bytes at `state`) is the hash value followed by a
 64-byte buffer (see `VG.Spec.Sha256.Repr`).
 
-* `init(state = r0)` stores the initial hash value.
+* `init(state = r0)` stores the initial hash value (`init224`, SHA-224's).
 * `update` and `finalize` are the generic streaming code
   (`Impl/MdStream/Arm.lean`), calling the compression function
   (`vg_sha256_compress`) with `scratch[0..112)` as its scratch space, and saving our
@@ -22,12 +22,19 @@ namespace VG.Impl.Sha256.Arm.Stream
 open VG.Arm
 open VG.Impl.Sha256.Arm (compress)
 
-def init : Prog isa :=
+/-- Stores the initial hash value `iv`. -/
+def initWith (iv : Spec.Sha256.HashValue) : Prog isa :=
   .block ((List.range 8).flatMap fun k =>
-    [.movw .r12 (Spec.Sha256.H0[k]!.extractLsb' 0 16),
-     .movt .r12 (Spec.Sha256.H0[k]!.extractLsb' 16 16),
+    [.movw .r12 (iv[k]!.extractLsb' 0 16),
+     .movt .r12 (iv[k]!.extractLsb' 16 16),
      .str .r12 .r0 (4 * k)])
 
+/-- `vg_sha256_init`. -/
+def init : Prog isa := initWith Spec.Sha256.H0
+
+/-- `vg_sha224_init`. -/
+def init224 : Prog isa := initWith Spec.Sha256.H0_224
+
 /-- The callee-saved registers we use (and `lr`), and where they are saved in `scratch`. -/
 def saved : List (Reg × Nat) :=
   [(.r4, 112), (.r5, 116), (.r6, 120), (.r7, 124), (.r8, 128), (.r9, 132), (.r10, 136), (.r11, 140),
diff --git a/lean/VerifiedGarbage/Impl/Sha256/X86/Stream.lean b/lean/VerifiedGarbage/Impl/Sha256/X86/Stream.lean
index 41e1c3f15..e4f755809 100644
--- a/lean/VerifiedGarbage/Impl/Sha256/X86/Stream.lean
+++ b/lean/VerifiedGarbage/Impl/Sha256/X86/Stream.lean
@@ -8,7 +8,7 @@ The streaming state (96 bytes at `state`) is the hash value followed by a
 64-byte buffer (see `VG.Spec.Sha256.Repr`). Every argument is on the stack
 (cdecl).
 
-* `init(state)` stores `H⁽⁰⁾`.
+* `init(state)` stores `H⁽⁰⁾` (`init224`, SHA-224's).
 * `update(state, count, data, len, scratch)` is the generic streaming code
   (`Impl/MdStream/X86.lean`): it compresses every whole block left in `data`
   with one call if the buffer is empty, and otherwise copies bytes into the
@@ -33,10 +33,17 @@ namespace VG.Impl.Sha256.X86.Stream
 open VG.X86
 open VG.Impl.Sha256.X86 (at_ compress)
 
-def init : Prog isa :=
+/-- Stores the initial hash value `iv`. -/
+def initWith (iv : Spec.Sha256.HashValue) : Prog isa :=
   .seq (.block [.mov .eax (.mem (at_ .esp 4))])
     (.block ((List.range 8).flatMap fun k =>
-      [.mov .ecx (.imm Spec.Sha256.H0[k]!), .store (at_ .eax (4 * k)) .ecx]))
+      [.mov .ecx (.imm iv[k]!), .store (at_ .eax (4 * k)) .ecx]))
+
+/-- `vg_sha256_init`. -/
+def init : Prog isa := initWith Spec.Sha256.H0
+
+/-- `vg_sha224_init`. -/
+def init224 : Prog isa := initWith Spec.Sha256.H0_224
 
 /-- The callee-saved registers, and where they are saved in `scratch`. -/
 def saved : List (Reg × Nat) := [(.ebx, 112), (.esi, 116), (.edi, 120), (.ebp, 124)]
diff --git a/lean/VerifiedGarbage/Impl/Sha256/X86_64/Stream.lean b/lean/VerifiedGarbage/Impl/Sha256/X86_64/Stream.lean
index cd982f3d8..ac17f576d 100644
--- a/lean/VerifiedGarbage/Impl/Sha256/X86_64/Stream.lean
+++ b/lean/VerifiedGarbage/Impl/Sha256/X86_64/Stream.lean
@@ -9,7 +9,7 @@ import VerifiedGarbage.Impl.MdStream.X86_64
 The streaming state (96 bytes at `state`) is the hash value followed by a
 64-byte buffer (see `VG.Spec.Sha256.Repr`).
 
-* `init(state = rdi)` stores `H⁽⁰⁾`.
+* `init(state = rdi)` stores `H⁽⁰⁾` (`init224`, SHA-224's).
 * `update(state = rdi, count = rsi, data = rdx, len = rcx, scratch = r8)`
   processes one block per iteration: straight from `data` while the buffer is
   empty and a whole block remains, otherwise by copying bytes into the buffer,
@@ -42,9 +42,16 @@ def Callee.scalar : Callee := ⟨"vg_sha256_compress", compress⟩
 def Callee.shani : Callee := ⟨"vg_sha256_compress_shani", ShaNi.compress⟩
 def Callee.avx2 : Callee := ⟨"vg_sha256_compress_avx2", Avx2.compress⟩
 
-def init : Prog isa :=
+/-- Stores the initial hash value `iv`. -/
+def initWith (iv : Spec.Sha256.HashValue) : Prog isa :=
   .block ((List.range 8).flatMap fun k =>
-    [.mov32 .rax (.imm Spec.Sha256.H0[k]!), .store32 (at_ .rdi (4 * k)) .rax])
+    [.mov32 .rax (.imm iv[k]!), .store32 (at_ .rdi (4 * k)) .rax])
+
+/-- `vg_sha256_init`. -/
+def init : Prog isa := initWith Spec.Sha256.H0
+
+/-- `vg_sha224_init`. -/
+def init224 : Prog isa := initWith Spec.Sha256.H0_224
 
 /-- The callee-saved registers, and where they are saved in `scratch`. -/
 def saved : List (Reg × Nat) := [(.rbx, 560), (.rbp, 568), (.r12, 576), (.r13, 584), (.r14, 592), (.r15, 600)]
diff --git a/lean/VerifiedGarbage/Proof/Sha256/AArch64/Contract.lean b/lean/VerifiedGarbage/Proof/Sha256/AArch64/Contract.lean
index 8666c554a..63b8f8f35 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/AArch64/Contract.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/AArch64/Contract.lean
@@ -41,15 +41,16 @@ def compressAArch64 : Contract AArch64.isa where
     s₁.gpr .x2 = s₂.gpr .x2 ∧ s₁.gpr .x3 = s₂.gpr .x3 ∧ s₁.sp = s₂.sp
 
 open AArch64 in
-/-- AArch64 contract for `vg_sha256_init(state: *mut [u8; 96])`: makes the
-streaming state at `state` represent the empty message.
+/-- AArch64 contract for `vg_sha256_init(state: *mut [u8; 96])` and
+`vg_sha224_init`, which store the initial hash value `iv`: makes the
+streaming state at `state` represent the empty message, hashed from `iv`.
 
 The code may write `state` (96 bytes). The pointer is public. -/
-def initAArch64 : Contract AArch64.isa where
+def initAArch64 (iv : HashValue) : Contract AArch64.isa where
   pre s :=
     let state : Region := ⟨s.gpr .x0, 96⟩
     s.rd = [] ∧ s.wr = [state]
-  post s s' := Repr s'.mem (s.gpr .x0) []
+  post s s' := ReprFrom iv s'.mem (s.gpr .x0) []
   pub s₁ s₂ := s₁.gpr .x0 = s₂.gpr .x0 ∧ s₁.sp = s₂.sp
 
 open AArch64 in
diff --git a/lean/VerifiedGarbage/Proof/Sha256/AArch64/Shared.lean b/lean/VerifiedGarbage/Proof/Sha256/AArch64/Shared.lean
index 8bcb452c4..24bbb714a 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/AArch64/Shared.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/AArch64/Shared.lean
@@ -117,6 +117,13 @@ theorem init :
       AArch64.abi, AArch64.argRegs]
       [Proof.Sha256.AArch64.Stream.initSat] using Proof.Sha256.AArch64.Stream.initSat)
 
+theorem init224 :
+    Verified AArch64.target Impl.Sha256.AArch64.Stream.init224 (Spec.Sha256.init224Contract AArch64.abi) :=
+  Proof.Sha256.AArch64.Stream.init224_verified.of_implies (by
+    contract_implies [Spec.Sha256.init224Contract, Spec.Sha256.initSig, Proof.Sha256.initAArch64,
+      AArch64.abi, AArch64.argRegs]
+      [Proof.Sha256.AArch64.Stream.initSat] using Proof.Sha256.AArch64.Stream.initSat)
+
 theorem update_of {code : Prog isa} (hv : Verified AArch64.target code Proof.Sha256.updateAArch64) :
     Verified AArch64.target code (Spec.Sha256.updateContract AArch64.abi 16) := by
   have hi : updateWide.Implies (Spec.Sha256.updateContract AArch64.abi 16) := by
diff --git a/lean/VerifiedGarbage/Proof/Sha256/AArch64/Stream/Init.lean b/lean/VerifiedGarbage/Proof/Sha256/AArch64/Stream/Init.lean
index d13000f82..60a77b3bb 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/AArch64/Stream/Init.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/AArch64/Stream/Init.lean
@@ -18,8 +18,10 @@ open VG.Spec.Sha256 (stateAt H0)
 def word (x : BitVec 32) (off : Nat) : List Instr :=
   [.movz .w .x9 (x.extractLsb' 0 16) 0, .movk .w .x9 (x.extractLsb' 16 16) 1, .str .w .x9 .x0 off]
 
-theorem init_eq : init = .block (word H0[0] 0 ++ word H0[1] 4 ++ word H0[2] 8 ++ word H0[3] 12 ++
-    word H0[4] 16 ++ word H0[5] 20 ++ word H0[6] 24 ++ word H0[7] 28) := rfl
+variable (iv : Spec.Sha256.HashValue)
+
+theorem initWith_eq : initWith iv = .block (word iv[0] 0 ++ word iv[1] 4 ++ word iv[2] 8 ++ word iv[3] 12 ++
+    word iv[4] 16 ++ word iv[5] 20 ++ word iv[6] 24 ++ word iv[7] 28) := rfl
 
 /-- `movz` of the low half then `movk` of the high half, then a 32-bit store. -/
 theorem movzk (x : BitVec 32) :
@@ -49,13 +51,13 @@ theorem word_ok {x : BitVec 32} {off : Nat} (ho : off % 4 = 0 ∧ off < 16384) {
     congr 1
     exact movzk x
 
-theorem init_correct {s₀ : State} (hp : Proof.Sha256.initAArch64.pre s₀) :
-    WP isa init s₀ fun s' => abiPreserved s₀ s' ∧ Proof.Sha256.initAArch64.post s₀ s' := by
-  apply WP.withPreservedV (hc := by decide +kernel)
+theorem init_correct {s₀ : State} (hp : (Proof.Sha256.initAArch64 iv).pre s₀) :
+    WP isa (initWith iv) s₀ fun s' => abiPreserved s₀ s' ∧ (Proof.Sha256.initAArch64 iv).post s₀ s' := by
+  apply WP.withPreservedV (hc := by rw [initWith_eq]; rfl)
   obtain ⟨-, hwr⟩ := hp
   have o : ∀ k, k < 8 → InRegions s₀.wr (s₀.gpr .x0 + BitVec.ofNat 64 (4 * k)) 4 :=
     fun k hk => ⟨⟨s₀.gpr .x0, 96⟩, by simp [hwr], contains_offset (by omega) (by omega)⟩
-  rw [init_eq, ← List.append_nil (_ ++ word H0[7] 28)]
+  rw [initWith_eq, ← List.append_nil (_ ++ word iv[7] 28)]
   simp only [List.append_assoc]
   refine word_ok (by decide) (o 0 (by omega)) fun s1 g1 _ wr1 sp1 m1 => ?_
   refine word_ok (by decide) (by rw [wr1, g1 _ (by decide)]; exact o 1 (by omega))
@@ -80,7 +82,7 @@ theorem init_correct {s₀ : State} (hp : Proof.Sha256.initAArch64.pre s₀) :
     WP.block_nil ?_
   have k8 : ∀ r, r ≠ .x9 → s8.gpr r = s₀.gpr r := fun r h => by
     rw [g8 r h, g7 r h, g6 r h, g5 r h, k4 r h]
-  have hm : s8.mem = writeState s₀.mem (s₀.gpr .x0) H0 := by
+  have hm : s8.mem = writeState s₀.mem (s₀.gpr .x0) iv := by
     rw [m8, m7, m6, m5, m4, m3, m2, m1]
     simp only [g7 _ (show Reg.x0 ≠ .x9 by decide), g6 _ (show Reg.x0 ≠ .x9 by decide),
       g5 _ (show Reg.x0 ≠ .x9 by decide), k4 _ (show Reg.x0 ≠ .x9 by decide),
@@ -90,9 +92,9 @@ theorem init_correct {s₀ : State} (hp : Proof.Sha256.initAArch64.pre s₀) :
   refine ⟨⟨fun r hr => k8 r ?_, by rw [sp8, sp7, sp6, sp5, sp4, sp3, sp2, sp1]⟩, ?_⟩
   · simp only [preserved, List.mem_cons, List.not_mem_nil, or_false] at hr
     rcases hr with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
-  · show Spec.Sha256.Repr s8.mem (s₀.gpr .x0) []
+  · show Spec.Sha256.ReprFrom iv s8.mem (s₀.gpr .x0) []
     rw [hm]
-    exact Proof.Sha256.Stream.repr_nil (stateAt_writeState _ _ _)
+    exact Proof.Sha256.Stream.reprFrom_nil (stateAt_writeState _ _ _)
 
 /-- A state satisfying the precondition. -/
 def initSat : State where
@@ -103,14 +105,23 @@ def initSat : State where
   rd := []
   wr := [⟨0x1000, 96⟩]
 
-theorem init_verified : Verified AArch64.target init Proof.Sha256.initAArch64 := by
+/-- `initWith iv` is verified, given that the taint analysis, which the
+kernel can only run on a literal `iv`, accepts it. -/
+theorem initWith_verified {hc} (hct : (taint.check (Taint.ofRegs [.x0]) (initWith iv) hc).isSome = true) :
+    Verified AArch64.target (initWith iv) (Proof.Sha256.initAArch64 iv) := by
   refine ⟨fun s hs => ?_, ?_, ⟨initSat, rfl, rfl⟩⟩
-  · obtain ⟨t, s', he, h⟩ := init_correct hs
+  · obtain ⟨t, s', he, h⟩ := init_correct iv hs
     exact ⟨t, s', he, h⟩
-  · refine VG.Taint.constantTime (A := taint) (Taint.ofRegs [.x0]) ?_ (by taint_decide)
+  · refine VG.Taint.constantTime (A := taint) (Taint.ofRegs [.x0]) ?_ hct
     intro s₁ s₂ _ _ h
     refine ⟨h.2, fun r hr => ?_⟩
     simp only [VG.AArch64.Taint.mem_ofRegs, List.mem_cons, List.not_mem_nil, or_false] at hr
     subst hr; exact h.1
 
+theorem init_verified : Verified AArch64.target init (Proof.Sha256.initAArch64 H0) :=
+  initWith_verified _ (hct := by taint_decide)
+
+theorem init224_verified : Verified AArch64.target init224 (Proof.Sha256.initAArch64 Spec.Sha256.H0_224) :=
+  initWith_verified _ (hct := by taint_decide)
+
 end VG.Proof.Sha256.AArch64.Stream
diff --git a/lean/VerifiedGarbage/Proof/Sha256/Arm/Contract.lean b/lean/VerifiedGarbage/Proof/Sha256/Arm/Contract.lean
index 883dc5d61..d6709668a 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/Arm/Contract.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/Arm/Contract.lean
@@ -49,16 +49,17 @@ low word in `r2`). -/
 def countArm (s : Arm.State) : BitVec 64 := s.gpr .r3 ++ s.gpr .r2
 
 open Arm in
-/-- 32-bit ARM contract for `vg_sha256_init(state: *mut [u8; 96])`: makes the
-streaming state at `state` represent the empty message.
+/-- 32-bit ARM contract for `vg_sha256_init(state: *mut [u8; 96])` and
+`vg_sha224_init`, which store the initial hash value `iv`: makes the
+streaming state at `state` represent the empty message, hashed from `iv`.
 
 The code may write `state` (96 bytes), which may not wrap around the end of
 the (32-bit) address space. The pointer is public. -/
-def initArm : Contract Arm.isa where
+def initArm (iv : HashValue) : Contract Arm.isa where
   pre s :=
     let state : Region := ⟨State.addr (s.gpr .r0), 96⟩
     s.rd = [] ∧ s.wr = [state] ∧ (s.gpr .r0).toNat + 96 ≤ 2 ^ 32
-  post s s' := Repr s'.mem (State.addr (s.gpr .r0)) []
+  post s s' := ReprFrom iv s'.mem (State.addr (s.gpr .r0)) []
   pub s₁ s₂ := s₁.gpr .r0 = s₂.gpr .r0
 
 open Arm in
diff --git a/lean/VerifiedGarbage/Proof/Sha256/Arm/Shared.lean b/lean/VerifiedGarbage/Proof/Sha256/Arm/Shared.lean
index 5fa4e06aa..d849b9a3f 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/Arm/Shared.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/Arm/Shared.lean
@@ -151,6 +151,13 @@ theorem init : Verified Arm.target Impl.Sha256.Arm.Stream.init (Spec.Sha256.init
       [Proof.Sha256.Arm.Stream.initSat, Arm.stackArg, Arm.stackArgAddr, Mem.readW,
       Mem.read] using Proof.Sha256.Arm.Stream.initSat)
 
+theorem init224 : Verified Arm.target Impl.Sha256.Arm.Stream.init224 (Spec.Sha256.init224Contract Arm.abi) :=
+  Proof.Sha256.Arm.Stream.init224_verified.of_implies (by
+    contract_implies [Spec.Sha256.init224Contract, Spec.Sha256.initSig, Proof.Sha256.initArm, Arm.abi,
+      Arm.argRegs, Arm.reduceClassify, Arm.Loc.val, Arm.State.addr]
+      [Proof.Sha256.Arm.Stream.initSat, Arm.stackArg, Arm.stackArgAddr, Mem.readW,
+      Mem.read] using Proof.Sha256.Arm.Stream.initSat)
+
 theorem updateWide_implies : updateWide.Implies (Spec.Sha256.updateContract Arm.abi) := by
   contract_implies [Spec.Sha256.updateContract, Spec.Sha256.updateSig, updateWide,
     Proof.Sha256.updateArm, Proof.Sha256.countArm, Arm.abi, Arm.argRegs, Arm.reduceClassify,
diff --git a/lean/VerifiedGarbage/Proof/Sha256/Arm/Stream/Init.lean b/lean/VerifiedGarbage/Proof/Sha256/Arm/Stream/Init.lean
index 49dc003a3..4edfd7276 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/Arm/Stream/Init.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/Arm/Stream/Init.lean
@@ -19,8 +19,10 @@ open VG.Spec.Sha256 (stateAt H0)
 def word (x : BitVec 32) (off : Nat) : List Instr :=
   [.movw .r12 (x.extractLsb' 0 16), .movt .r12 (x.extractLsb' 16 16), .str .r12 .r0 off]
 
-theorem init_eq : init = .block (word H0[0] 0 ++ word H0[1] 4 ++ word H0[2] 8 ++ word H0[3] 12 ++
-    word H0[4] 16 ++ word H0[5] 20 ++ word H0[6] 24 ++ word H0[7] 28) := rfl
+variable (iv : Spec.Sha256.HashValue)
+
+theorem initWith_eq : initWith iv = .block (word iv[0] 0 ++ word iv[1] 4 ++ word iv[2] 8 ++ word iv[3] 12 ++
+    word iv[4] 16 ++ word iv[5] 20 ++ word iv[6] 24 ++ word iv[7] 28) := rfl
 
 theorem word_ok {x : BitVec 32} {off : Nat} (ho : off < 4096) {rest : List Instr}
     {s : State} {Q : State → Prop} (hfit : (s.gpr .r0).toNat + off < 2 ^ 32)
@@ -35,12 +37,12 @@ theorem word_ok {x : BitVec 32} {off : Nat} (ho : off < 4096) {rest : List Instr
   rw [u.mem]
   simp only [State.setReg, ite_true, movw_movt]
 
-theorem init_correct {s₀ : State} (hp : Proof.Sha256.initArm.pre s₀) :
-    WP isa init s₀ fun s' => abiPreserved s₀ s' ∧ Proof.Sha256.initArm.post s₀ s' := by
+theorem init_correct {s₀ : State} (hp : (Proof.Sha256.initArm iv).pre s₀) :
+    WP isa (initWith iv) s₀ fun s' => abiPreserved s₀ s' ∧ (Proof.Sha256.initArm iv).post s₀ s' := by
   obtain ⟨-, hwr, hfit⟩ := hp
   have o : ∀ k, k < 8 → InRegions s₀.wr (State.addr (s₀.gpr .r0) + BitVec.ofNat 64 (4 * k)) 4 :=
     fun k hk => ⟨⟨State.addr (s₀.gpr .r0), 96⟩, by simp [hwr], contains_offset (by omega) (by omega)⟩
-  rw [init_eq, ← List.append_nil (_ ++ word H0[7] 28)]
+  rw [initWith_eq, ← List.append_nil (_ ++ word iv[7] 28)]
   simp only [List.append_assoc]
   refine word_ok (by decide) (by omega) (o 0 (by omega)) fun s1 g1 _ wr1 sp1 m1 => ?_
   have k1 : s1.gpr .r0 = s₀.gpr .r0 := g1 _ (by decide)
@@ -71,15 +73,15 @@ theorem init_correct {s₀ : State} (hp : Proof.Sha256.initArm.pre s₀) :
     fun s8 g8 _ _ sp8 m8 => WP.block_nil ?_
   have k8 : ∀ r, r ≠ .r12 → s8.gpr r = s₀.gpr r := fun r h => by
     rw [g8 r h, g7 r h, g6 r h, g5 r h, g4 r h, g3 r h, g2 r h, g1 r h]
-  have hm : s8.mem = Proof.Sha256.StateMem.writeState s₀.mem (State.addr (s₀.gpr .r0)) H0 := by
+  have hm : s8.mem = Proof.Sha256.StateMem.writeState s₀.mem (State.addr (s₀.gpr .r0)) iv := by
     rw [m8, m7, m6, m5, m4, m3, m2, m1, k7, k6, k5, k4, k3, k2, k1]
     rfl
   refine ⟨⟨fun r hr => k8 r ?_, by rw [sp8, sp7, sp6, sp5, sp4, sp3, sp2, sp1]⟩, ?_⟩
   · simp only [preserved, List.mem_cons, List.not_mem_nil, or_false] at hr
     rcases hr with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
-  · show Spec.Sha256.Repr s8.mem (State.addr (s₀.gpr .r0)) []
+  · show Spec.Sha256.ReprFrom iv s8.mem (State.addr (s₀.gpr .r0)) []
     rw [hm]
-    exact Proof.Sha256.Stream.repr_nil (Proof.Sha256.StateMem.stateAt_writeState _ _ _)
+    exact Proof.Sha256.Stream.reprFrom_nil (Proof.Sha256.StateMem.stateAt_writeState _ _ _)
 
 /-- A state satisfying the precondition. -/
 def initSat : State where
@@ -94,11 +96,20 @@ def initSat : State where
   rd := []
   wr := [⟨0x1000, 96⟩]
 
-theorem init_verified : Verified Arm.target init Proof.Sha256.initArm := by
+/-- `initWith iv` is verified, given that the taint analysis, which the
+kernel can only run on a literal `iv`, accepts it. -/
+theorem initWith_verified {hc} (hct : (taint.check (Taint.ofRegs [.r0]) (initWith iv) hc).isSome = true) :
+    Verified Arm.target (initWith iv) (Proof.Sha256.initArm iv) := by
   refine ⟨fun s hs => ?_, ?_, ⟨initSat, rfl, rfl, by decide⟩⟩
-  · obtain ⟨t, s', he, h⟩ := init_correct hs
+  · obtain ⟨t, s', he, h⟩ := init_correct iv hs
     exact ⟨t, s', he, h⟩
-  · refine VG.Taint.constantTime (A := taint) (Taint.ofRegs [.r0]) (fun _ _ _ _ hp => ?_) (by taint_decide)
+  · refine VG.Taint.constantTime (A := taint) (Taint.ofRegs [.r0]) (fun _ _ _ _ hp => ?_) hct
     exact Taint.agree_ofRegs fun r hr => by simp only [List.mem_singleton] at hr; subst hr; exact hp
 
+theorem init_verified : Verified Arm.target init (Proof.Sha256.initArm H0) :=
+  initWith_verified _ (hct := by taint_decide)
+
+theorem init224_verified : Verified Arm.target init224 (Proof.Sha256.initArm Spec.Sha256.H0_224) :=
+  initWith_verified _ (hct := by taint_decide)
+
 end VG.Proof.Sha256.Arm.Stream
diff --git a/lean/VerifiedGarbage/Proof/Sha256/Stream.lean b/lean/VerifiedGarbage/Proof/Sha256/Stream.lean
index b1fa38fe3..e48b706b0 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/Stream.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/Stream.lean
@@ -113,8 +113,12 @@ theorem bytesAt_writeBytes (m : Mem) (p : Addr) (r : Nat) (xs : List Byte) (h :
 
 /-! ## `Repr` -/
 
-theorem repr_nil {mem : Mem} {p : Addr} (h : stateAt mem p = H0) : Spec.Sha256.Repr mem p [] := by
-  simp [Spec.Sha256.Repr, Spec.Sha256.ReprFrom, h, compressList_zero, bytesAt]
+theorem reprFrom_nil {iv : HashValue} {mem : Mem} {p : Addr} (h : stateAt mem p = iv) :
+    Spec.Sha256.ReprFrom iv mem p [] := by
+  simp [Spec.Sha256.ReprFrom, h, compressList_zero, bytesAt]
+
+theorem repr_nil {mem : Mem} {p : Addr} (h : stateAt mem p = H0) : Spec.Sha256.Repr mem p [] :=
+  reprFrom_nil h
 
 /-- Appending bytes that stay within the buffer. -/
 theorem repr_append_buf {mem mem' : Mem} {p : Addr} {m xs : List Byte} (hr : Spec.Sha256.Repr mem p m)
diff --git a/lean/VerifiedGarbage/Proof/Sha256/X86/Contract.lean b/lean/VerifiedGarbage/Proof/Sha256/X86/Contract.lean
index 9e9b7e509..b7f6a4c3c 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/X86/Contract.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/X86/Contract.lean
@@ -60,22 +60,23 @@ and 2 (cdecl: the low word first). -/
 def countX86 (s : X86.State) : BitVec 64 := arg s 2 ++ arg s 1
 
 open X86 in
-/-- x86 (32-bit) contract for `vg_sha256_init(state: *mut [u8; 96])`, whose
+/-- x86 (32-bit) contract for `vg_sha256_init(state: *mut [u8; 96])` and
+`vg_sha224_init`, which store the initial hash value `iv`, whose
 argument is on the stack (cdecl): makes the streaming state at `state`
-represent the empty message.
+represent the empty message, hashed from `iv`.
 
 The code may read the argument (4 bytes above the return address) and write
 `state` (96 bytes), which may not overlap the argument or the return address;
 nothing may wrap around the end of the (32-bit) address space. `esp` and the
 pointer are public. -/
-def initX86 : Contract X86.isa where
+def initX86 (iv : HashValue) : Contract X86.isa where
   pre s :=
     let state : Region := ⟨(arg s 0).setWidth 64, 96⟩
     let args : Region := ⟨argAddr s 0, 4⟩
     let ret : Region := ⟨(s.gpr .esp).setWidth 64, 4⟩
     s.rd = [args] ∧ s.wr = [state] ∧ args.Disjoint state ∧ ret.Disjoint state ∧
     (arg s 0).toNat + 96 ≤ 2 ^ 32 ∧ (s.gpr .esp).toNat + 8 ≤ 2 ^ 32
-  post s s' := Repr s'.mem ((arg s 0).setWidth 64) []
+  post s s' := ReprFrom iv s'.mem ((arg s 0).setWidth 64) []
   pub s₁ s₂ := s₁.gpr .esp = s₂.gpr .esp ∧ arg s₁ 0 = arg s₂ 0
 
 open X86 in
diff --git a/lean/VerifiedGarbage/Proof/Sha256/X86/Shared.lean b/lean/VerifiedGarbage/Proof/Sha256/X86/Shared.lean
index d15d84ac9..706316ad0 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/X86/Shared.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/X86/Shared.lean
@@ -27,9 +27,11 @@ open VG.Spec.Sha256 (stateAt H0)
 /-- The two instructions storing the word `x` at `[eax + 4 * k]`. -/
 def word (x : BitVec 32) (k : Nat) : List Instr := [.mov .ecx (.imm x), .store (at_ .eax (4 * k)) .ecx]
 
-theorem init_eq : init = .seq (.block [.mov .eax (.mem (at_ .esp 4))])
-    (.block (word H0[0] 0 ++ word H0[1] 1 ++ word H0[2] 2 ++ word H0[3] 3 ++ word H0[4] 4 ++
-      word H0[5] 5 ++ word H0[6] 6 ++ word H0[7] 7)) := rfl
+variable (iv : Spec.Sha256.HashValue)
+
+theorem initWith_eq : initWith iv = .seq (.block [.mov .eax (.mem (at_ .esp 4))])
+    (.block (word iv[0] 0 ++ word iv[1] 1 ++ word iv[2] 2 ++ word iv[3] 3 ++ word iv[4] 4 ++
+      word iv[5] 5 ++ word iv[6] 6 ++ word iv[7] 7)) := rfl
 
 theorem word_ok {x : BitVec 32} {k : Nat} {rest : List Instr} {s : State} {Q : State → Prop}
     {st : BitVec 32} (heax : s.gpr .eax = st) (hout : InRegions s.wr (addr st (4 * k)) 4)
@@ -43,18 +45,18 @@ theorem word_ok {x : BitVec 32} {k : Nat} {rest : List Instr} {s : State} {Q : S
     (by rw [u₂.rd, u₁.rd]) (by rw [u₂.wr, u₁.wr]) ?_
   rw [u₂.mem, u₁.gpr, u₁.mem]
 
-theorem init_correct {s₀ : State} (hp : Proof.Sha256.initX86.pre s₀) :
-    WP isa init s₀ fun s' => abiPreserved s₀ s' ∧ Proof.Sha256.initX86.post s₀ s' := by
+theorem init_correct {s₀ : State} (hp : (Proof.Sha256.initX86 iv).pre s₀) :
+    WP isa (initWith iv) s₀ fun s' => abiPreserved s₀ s' ∧ (Proof.Sha256.initX86 iv).post s₀ s' := by
   obtain ⟨hrd, hwr, hargs, hret, hfit, hsp⟩ := hp
   set st := arg s₀ 0 with hst
   have o : ∀ k, k < 8 → InRegions s₀.wr (addr st (4 * k)) 4 :=
     fun k hk => ⟨⟨st.setWidth 64, 96⟩, by simp [hwr], contains_addr (by omega) (by omega) hfit⟩
-  rw [init_eq]
+  rw [initWith_eq]
   refine WP.seq (wp_movm (a := addr (s₀.gpr .esp) 4) (ea_at _ _ _)
     ⟨⟨argAddr s₀ 0, 4⟩, by simp [hrd], Region.contains_self _ _⟩ fun s₁ u₁ => WP.block_nil ?_)
   have e1 : s₁.gpr .eax = st := u₁.gpr
   have w1 : s₁.wr = s₀.wr := u₁.wr
-  rw [← List.append_nil (_ ++ word H0[7] 7)]
+  rw [← List.append_nil (_ ++ word iv[7] 7)]
   simp only [List.append_assoc]
   refine word_ok e1 (by rw [w1]; exact o 0 (by omega)) fun s2 a2 g2 _ wr2 m2 => ?_
   refine word_ok a2 (by rw [wr2, w1]; exact o 1 (by omega)) fun s3 a3 g3 _ wr3 m3 => ?_
@@ -71,7 +73,7 @@ theorem init_correct {s₀ : State} (hp : Proof.Sha256.initX86.pre s₀) :
     rw [g9 r h, g8 r h, g7 r h, g6 r h, g5 r h, g4 r h, g3 r h, g2 r h, u₁.other r h']
   have ha : ∀ k, k < 8 → addr st (4 * k) = st.setWidth 64 + BitVec.ofNat 64 (4 * k) :=
     fun k hk => addr_eq (by omega)
-  have hm : s9.mem = Proof.Sha256.StateMem.writeState s₀.mem (st.setWidth 64) H0 := by
+  have hm : s9.mem = Proof.Sha256.StateMem.writeState s₀.mem (st.setWidth 64) iv := by
     rw [m9, m8, m7, m6, m5, m4, m3, m2, u₁.mem, ha 0 (by omega), ha 1 (by omega), ha 2 (by omega),
       ha 3 (by omega), ha 4 (by omega), ha 5 (by omega), ha 6 (by omega), ha 7 (by omega)]
     rfl
@@ -91,9 +93,9 @@ theorem init_correct {s₀ : State} (hp : Proof.Sha256.initX86.pre s₀) :
   · simp only [calleeSaved, List.mem_cons, List.not_mem_nil, or_false] at hr
     rcases hr with rfl | rfl | rfl | rfl | rfl <;> decide
   · exact hf.readW (Region.contains_self _ _) (by simpa using hret) (by decide)
-  · show Spec.Sha256.Repr s9.mem (st.setWidth 64) []
+  · show Spec.Sha256.ReprFrom iv s9.mem (st.setWidth 64) []
     rw [hm]
-    exact Proof.Sha256.Stream.repr_nil (Proof.Sha256.StateMem.stateAt_writeState _ _ _)
+    exact Proof.Sha256.Stream.reprFrom_nil (Proof.Sha256.StateMem.stateAt_writeState _ _ _)
 
 /-- Memory holding the argument `0x1000` at `0x4004`. -/
 def initSatMem : Mem := fun a => if a = 0x4005 then 0x10 else 0
@@ -110,7 +112,7 @@ def initSat : State where
   rd := [⟨0x4004, 4⟩]
   wr := [⟨0x1000, 96⟩]
 
-theorem initSat_pre : Proof.Sha256.initX86.pre initSat := by
+theorem initSat_pre : (Proof.Sha256.initX86 iv).pre initSat := by
   have a0 : arg initSat 0 = 0x1000 := by decide
   have e : argAddr initSat 0 = 0x4004 := by decide
   simp only [Proof.Sha256.initX86, a0, e]
@@ -120,10 +122,11 @@ theorem initSat_pre : Proof.Sha256.initX86.pre initSat := by
 is the base address of the writable region. -/
 def initτ₀ : VG.X86.Taint.T := { regs := .ofList [.esp], flags := false, argLen := 8 }
 
-theorem init_agree₀ {s₁ s₂ : State} (h₁ : Proof.Sha256.initX86.pre s₁) (h₂ : Proof.Sha256.initX86.pre s₂)
-    (hpub : Proof.Sha256.initX86.pub s₁ s₂) : VG.X86.Taint.Agree initτ₀ s₁ s₂ := by
+theorem init_agree₀ {s₁ s₂ : State} (h₁ : (Proof.Sha256.initX86 iv).pre s₁)
+    (h₂ : (Proof.Sha256.initX86 iv).pre s₂) (hpub : (Proof.Sha256.initX86 iv).pub s₁ s₂) :
+    VG.X86.Taint.Agree initτ₀ s₁ s₂ := by
   obtain ⟨hesp, a0⟩ := hpub
-  have wf : ∀ s, Proof.Sha256.initX86.pre s → VG.X86.Taint.Wf initτ₀ s := by
+  have wf : ∀ s, (Proof.Sha256.initX86 iv).pre s → VG.X86.Taint.Wf initτ₀ s := by
     intro s hs
     obtain ⟨-, hw, hd, hr, -, hsp⟩ := hs
     refine VG.X86.Taint.Wf.entry rfl rfl ⟨fun h => absurd rfl h, fun _ h => (List.not_mem_nil h).elim,
@@ -143,12 +146,20 @@ theorem init_agree₀ {s₁ s₂ : State} (h₁ : Proof.Sha256.initX86.pre s₁)
       show (k - 4) / 4 = 0 by omega]
     exact congrArg _ a0
 
-theorem init_verified : Verified X86.target init Proof.Sha256.initX86 := by
-  refine ⟨fun s hs => ?_, ?_, ⟨initSat, initSat_pre⟩⟩
-  · obtain ⟨t, s', he, h⟩ := init_correct hs
+/-- `initWith iv` is verified, given that the taint analysis, which the
+kernel can only run on a literal `iv`, accepts it. -/
+theorem initWith_verified {hc} (hct : (taint.check initτ₀ (initWith iv) hc).isSome = true) :
+    Verified X86.target (initWith iv) (Proof.Sha256.initX86 iv) := by
+  refine ⟨fun s hs => ?_, ?_, ⟨initSat, initSat_pre iv⟩⟩
+  · obtain ⟨t, s', he, h⟩ := init_correct iv hs
     exact ⟨t, s', he, h⟩
-  · exact VG.Taint.constantTime (A := taint) initτ₀ (fun _ _ h₁ h₂ hp => init_agree₀ h₁ h₂ hp)
-      (by taint_decide)
+  · exact VG.Taint.constantTime (A := taint) initτ₀ (fun _ _ h₁ h₂ hp => init_agree₀ iv h₁ h₂ hp) hct
+
+theorem init_verified : Verified X86.target init (Proof.Sha256.initX86 H0) :=
+  initWith_verified _ (hct := by taint_decide)
+
+theorem init224_verified : Verified X86.target init224 (Proof.Sha256.initX86 Spec.Sha256.H0_224) :=
+  initWith_verified _ (hct := by taint_decide)
 
 end VG.Proof.Sha256.X86.Stream
 
@@ -419,6 +430,13 @@ theorem init :
       X86.abi, X86.argSlots, X86.argVal, X86.argBytes]
       [Proof.Sha256.X86.Stream.initSat, Proof.Sha256.X86.Stream.initSatMem, X86.arg, X86.argAddr, Mem.readW, Mem.read] using Proof.Sha256.X86.Stream.initSat)
 
+theorem init224 :
+    Verified X86.target Impl.Sha256.X86.Stream.init224 (Spec.Sha256.init224Contract X86.abi) :=
+  Proof.Sha256.X86.Stream.init224_verified.of_implies (by
+    contract_implies [Spec.Sha256.init224Contract, Spec.Sha256.initSig, Proof.Sha256.initX86,
+      X86.abi, X86.argSlots, X86.argVal, X86.argBytes]
+      [Proof.Sha256.X86.Stream.initSat, Proof.Sha256.X86.Stream.initSatMem, X86.arg, X86.argAddr, Mem.readW, Mem.read] using Proof.Sha256.X86.Stream.initSat)
+
 theorem updateWide_implies : updateWide.Implies (Spec.Sha256.updateContract X86.abi 20) := by
   contract_implies [Spec.Sha256.updateContract, Spec.Sha256.updateSig, updateWide,
     Proof.Sha256.updateX86, Proof.Sha256.countX86, X86.abi, X86.argSlots, X86.argVal, X86.argBytes]
diff --git a/lean/VerifiedGarbage/Proof/Sha256/X86_64/Contract.lean b/lean/VerifiedGarbage/Proof/Sha256/X86_64/Contract.lean
index 36584fdad..e77d6b7b9 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/X86_64/Contract.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/X86_64/Contract.lean
@@ -39,17 +39,18 @@ def compressX86_64 : Contract X86_64.isa where
     s₁.gpr .rdx = s₂.gpr .rdx ∧ s₁.gpr .rcx = s₂.gpr .rcx
 
 open X86_64 in
-/-- x86-64 contract for `vg_sha256_init(state: *mut [u8; 96])`: makes the
-streaming state at `state` represent the empty message.
+/-- x86-64 contract for `vg_sha256_init(state: *mut [u8; 96])` and
+`vg_sha224_init`, which store the initial hash value `iv`: makes the
+streaming state at `state` represent the empty message, hashed from `iv`.
 
 The code may write `state` (96 bytes), which may not overlap the return
 address on the stack. The pointer is public. -/
-def initX86_64 : Contract X86_64.isa where
+def initX86_64 (iv : HashValue) : Contract X86_64.isa where
   pre s :=
     let state : Region := ⟨s.gpr .rdi, 96⟩
     let ret : Region := ⟨s.gpr .rsp, 8⟩
     s.rd = [] ∧ s.wr = [state] ∧ ret.Disjoint state
-  post s s' := Repr s'.mem (s.gpr .rdi) []
+  post s s' := ReprFrom iv s'.mem (s.gpr .rdi) []
   pub s₁ s₂ := s₁.gpr .rdi = s₂.gpr .rdi
 
 open X86_64 in
diff --git a/lean/VerifiedGarbage/Proof/Sha256/X86_64/Shared.lean b/lean/VerifiedGarbage/Proof/Sha256/X86_64/Shared.lean
index 06aedb831..52fc0d22b 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/X86_64/Shared.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/X86_64/Shared.lean
@@ -21,23 +21,25 @@ open VG.Proof.Sha256.X86_64 (ea_at contains_offset' writeState stateAt_writeStat
 
 /-! ## `init` -/
 
-theorem init_eq : init = .block [
-    .mov32 .rax (.imm 0x6a09e667), .store32 (at_ .rdi (4 * 0)) .rax,
-    .mov32 .rax (.imm 0xbb67ae85), .store32 (at_ .rdi (4 * 1)) .rax,
-    .mov32 .rax (.imm 0x3c6ef372), .store32 (at_ .rdi (4 * 2)) .rax,
-    .mov32 .rax (.imm 0xa54ff53a), .store32 (at_ .rdi (4 * 3)) .rax,
-    .mov32 .rax (.imm 0x510e527f), .store32 (at_ .rdi (4 * 4)) .rax,
-    .mov32 .rax (.imm 0x9b05688c), .store32 (at_ .rdi (4 * 5)) .rax,
-    .mov32 .rax (.imm 0x1f83d9ab), .store32 (at_ .rdi (4 * 6)) .rax,
-    .mov32 .rax (.imm 0x5be0cd19), .store32 (at_ .rdi (4 * 7)) .rax] := rfl
+variable (iv : Spec.Sha256.HashValue)
+
+theorem initWith_eq : initWith iv = .block [
+    .mov32 .rax (.imm iv[0]), .store32 (at_ .rdi (4 * 0)) .rax,
+    .mov32 .rax (.imm iv[1]), .store32 (at_ .rdi (4 * 1)) .rax,
+    .mov32 .rax (.imm iv[2]), .store32 (at_ .rdi (4 * 2)) .rax,
+    .mov32 .rax (.imm iv[3]), .store32 (at_ .rdi (4 * 3)) .rax,
+    .mov32 .rax (.imm iv[4]), .store32 (at_ .rdi (4 * 4)) .rax,
+    .mov32 .rax (.imm iv[5]), .store32 (at_ .rdi (4 * 5)) .rax,
+    .mov32 .rax (.imm iv[6]), .store32 (at_ .rdi (4 * 6)) .rax,
+    .mov32 .rax (.imm iv[7]), .store32 (at_ .rdi (4 * 7)) .rax] := rfl
 
 theorem init_post {s₀ : State}
     (hret : Region.Disjoint ⟨s₀.gpr .rsp, 8⟩ ⟨s₀.gpr .rdi, 96⟩) (g : Reg → BitVec 64)
     (hg : ∀ r, r ≠ .rax → g r = s₀.gpr r) :
-    gprPreserved s₀ { s₀ with gpr := g, mem := writeState s₀.mem (s₀.gpr .rdi) Spec.Sha256.H0 } ∧
-      Proof.Sha256.initX86_64.post s₀
-        { s₀ with gpr := g, mem := writeState s₀.mem (s₀.gpr .rdi) Spec.Sha256.H0 } := by
-  have hf : Frame [⟨s₀.gpr .rdi, 96⟩] s₀.mem (writeState s₀.mem (s₀.gpr .rdi) Spec.Sha256.H0) := by
+    gprPreserved s₀ { s₀ with gpr := g, mem := writeState s₀.mem (s₀.gpr .rdi) iv } ∧
+      (Proof.Sha256.initX86_64 iv).post s₀
+        { s₀ with gpr := g, mem := writeState s₀.mem (s₀.gpr .rdi) iv } := by
+  have hf : Frame [⟨s₀.gpr .rdi, 96⟩] s₀.mem (writeState s₀.mem (s₀.gpr .rdi) iv) := by
     have c : ∀ k, k < 8 → (⟨s₀.gpr .rdi, 96⟩ : Region).Contains
         (s₀.gpr .rdi + BitVec.ofInt 64 ((4 * k : Nat) : Int)) (32 / 8) :=
       fun k hk => contains_offset' (by omega) (by omega)
@@ -45,27 +47,30 @@ theorem init_post {s₀ : State}
     refine (((((((((Frame.refl _ _).writeW ?_ _ (c 0 ?_)).writeW ?_ _ (c 1 ?_)).writeW ?_ _
       (c 2 ?_)).writeW ?_ _ (c 3 ?_)).writeW ?_ _ (c 4 ?_)).writeW ?_ _ (c 5 ?_)).writeW ?_ _
       (c 6 ?_)).writeW ?_ _ (c 7 ?_)) <;> simp
-  refine ⟨⟨fun r hr => hg r ?_, ?_⟩, Stream.repr_nil (stateAt_writeState _ _ _)⟩
+  refine ⟨⟨fun r hr => hg r ?_, ?_⟩, Stream.reprFrom_nil (stateAt_writeState _ _ _)⟩
   · simp only [calleeSaved, List.mem_cons, List.not_mem_nil, or_false] at hr
     rcases hr with rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
   · exact hf.readW (Region.contains_self _ _) (by simpa using hret) (by decide)
 
+theorem setWidth_32_64 (x : BitVec 32) : (x.setWidth 64).setWidth 32 = x :=
+  BitVec.eq_of_toNat_eq (by simp)
+
 set_option simprocs false in
-theorem init_correct {s₀ : State} (hp : Proof.Sha256.initX86_64.pre s₀) :
-    WP isa init s₀ fun s' => gprPreserved s₀ s' ∧ Proof.Sha256.initX86_64.post s₀ s' := by
+theorem init_correct {s₀ : State} (hp : (Proof.Sha256.initX86_64 iv).pre s₀) :
+    WP isa (initWith iv) s₀ fun s' => gprPreserved s₀ s' ∧ (Proof.Sha256.initX86_64 iv).post s₀ s' := by
   obtain ⟨hrd, hwr, hret⟩ := hp
   have o : ∀ k, k < 8 → InRegions s₀.wr (s₀.gpr .rdi + BitVec.ofInt 64 ((4 * k : Nat) : Int)) 4 :=
     fun k hk => ⟨⟨s₀.gpr .rdi, 96⟩, by simp [hwr], contains_offset' (by omega) (by omega)⟩
   have o0 := o 0 (by omega); have o1 := o 1 (by omega); have o2 := o 2 (by omega)
   have o3 := o 3 (by omega); have o4 := o 4 (by omega); have o5 := o 5 (by omega)
   have o6 := o 6 (by omega); have o7 := o 7 (by omega)
-  rw [init_eq]
+  rw [initWith_eq]
   apply WP.of_runBlock
   simp (config := {decide := true}) only [runBlock_cons, runStep_some,
     runBlock_nil, exec, readSrc32, isa, ea_at, State.store32,
     State.setReg32, State.setReg, o0, o1, o2, o3, o4, o5, o6, o7, ite_true, ite_false,
-    Option.map_some, Option.some.injEq, exists_eq_left']
-  exact init_post hret _ fun r hr => by simp [hr]
+    Option.map_some, Option.some.injEq, exists_eq_left', setWidth_32_64]
+  exact init_post iv hret _ fun r hr => by simp [hr]
 
 /-- A state satisfying the precondition. -/
 def initSat : State where
@@ -79,15 +84,26 @@ def initSat : State where
   rd := []
   wr := [⟨0x1000, 96⟩]
 
-theorem init_verified : Verified X86_64.target init Proof.Sha256.initX86_64 := by
+/-- `initWith iv` is verified, given the checks that evaluate its code
+(which the kernel can only run on a literal `iv`): it never loads MXCSR, and
+the taint analysis accepts it. -/
+theorem initWith_verified (hm : (initWith iv).allInstrs (fun i => !loadsMxcsr i) = true)
+    {hc} (hct : (taint.check (Taint.ofRegs [.rdi]) (initWith iv) hc).isSome = true) :
+    Verified X86_64.target (initWith iv) (Proof.Sha256.initX86_64 iv) := by
   refine ⟨fun s hs => ?_, ?_, ⟨initSat, rfl, rfl, ?_⟩⟩
-  · obtain ⟨t, s', he, h⟩ := init_correct hs
-    exact ⟨t, s', he, abiPreserved_of_exec (by decide +kernel) he h.1, h.2⟩
-  · refine VG.Taint.constantTime (A := taint) (Taint.ofRegs [.rdi]) ?_ (by taint_decide)
+  · obtain ⟨t, s', he, h⟩ := init_correct iv hs
+    exact ⟨t, s', he, abiPreserved_of_exec hm he h.1, h.2⟩
+  · refine VG.Taint.constantTime (A := taint) (Taint.ofRegs [.rdi]) ?_ hct
     intro s₁ s₂ _ _ h
     exact Taint.agree_ofRegs fun r hr => by simp at hr; subst hr; exact h
   · exact Region.Disjoint.symm (Offset.disjoint_of_le (by decide) (by decide))
 
+theorem init_verified : Verified X86_64.target init (Proof.Sha256.initX86_64 Spec.Sha256.H0) :=
+  initWith_verified _ (by decide +kernel) (hct := by taint_decide)
+
+theorem init224_verified : Verified X86_64.target init224 (Proof.Sha256.initX86_64 Spec.Sha256.H0_224) :=
+  initWith_verified _ (by decide +kernel) (hct := by taint_decide)
+
 end VG.Proof.Sha256.X86_64.Stream
 
 /-!
@@ -130,6 +146,13 @@ theorem init :
       X86_64.abi, X86_64.argRegs]
       [Proof.Sha256.X86_64.Stream.initSat] using Proof.Sha256.X86_64.Stream.initSat)
 
+theorem init224 :
+    Verified X86_64.target Impl.Sha256.X86_64.Stream.init224 (Spec.Sha256.init224Contract X86_64.abi) :=
+  Proof.Sha256.X86_64.Stream.init224_verified.of_implies (by
+    contract_implies [Spec.Sha256.init224Contract, Spec.Sha256.initSig, Proof.Sha256.initX86_64,
+      X86_64.abi, X86_64.argRegs]
+      [Proof.Sha256.X86_64.Stream.initSat] using Proof.Sha256.X86_64.Stream.initSat)
+
 open VG.Impl.Sha256.X86_64.Stream (Callee) in
 /-- `update`, for any compression function `f` (see `Variant.lean`). -/
 theorem update {f : Callee} (hf : f.Ok)
diff --git a/lean/VerifiedGarbageTest/Sha224.lean b/lean/VerifiedGarbageTest/Sha224.lean
new file mode 100644
index 000000000..455bec9d8
--- /dev/null
+++ b/lean/VerifiedGarbageTest/Sha224.lean
@@ -0,0 +1,33 @@
+import VerifiedGarbageTest.Sha256
+
+/-!
+# Known-answer tests for the SHA-224 specification
+
+Two of the NIST CAVP SHA-224 vectors, read from the vendored response file
+`vectors/nist-cavp/sha224/SHA224ShortMsg.rsp` (see `vectors/sources/`)
+when this file is built and checked against `VG.Spec.Sha256.sha224`, so that
+a transcription error in its initial hash value fails the build. (As for
+SHA-256, the Rust tests run every CAVP vector against the implementation.)
+-/
+
+namespace VG.Test.Sha224
+
+open Lean Elab Command
+open VG.Test.Sha256 (vectors lengths)
+
+run_cmd do
+  -- This file is `lean/VerifiedGarbageTest/Sha224.lean`.
+  let file ← IO.FS.realPath (← getFileName)
+  let some root := file.parent >>= (·.parent) >>= (·.parent)
+    | throwError "no repository root above {file}"
+  let text ← IO.FS.readFile (root / "vectors" / "nist-cavp" / "sha224" / "SHA224ShortMsg.rsp")
+  let vs ← match vectors text with
+    | .ok vs => pure vs
+    | .error e => throwError "SHA224ShortMsg.rsp: {e}"
+  unless vs.length == 65 do throwError "expected 65 vectors, got {vs.length}"
+  for n in lengths do
+    let some (msg, md) := vs.find? (·.1.length == n)
+      | throwError "no {n}-byte vector"
+    unless Spec.Sha256.sha224 msg == md do throwError "SHA-224 of the {n}-byte CAVP vector is wrong"
+
+end VG.Test.Sha224
diff --git a/src/asm/aarch64/sha256.rs b/src/asm/aarch64/sha256.rs
index f632e6240..099344a30 100644
--- a/src/asm/aarch64/sha256.rs
+++ b/src/asm/aarch64/sha256.rs
@@ -2,6 +2,45 @@
 //! Verified `sha256` functions for `aarch64`.
 #![allow(dead_code)]
 
+/// Starts a SHA-224 computation: makes the SHA-256 streaming state `*state` represent the empty message, hashed from the initial hash value of SHA-224 (`VG.Spec.Sha256.H0_224`). Continue with `vg_sha256_update` and `vg_sha256_finalize`, and take the first 28 bytes of the final hash value as the digest.
+///
+/// Contract: `VG.Spec.Sha256.init224Contract`. The streaming state is the hash value followed by a buffered partial block (`VG.Spec.Sha256.ReprFrom`).
+///
+/// # Safety
+///
+/// * `state` must be valid for reads and writes of 96 bytes.
+/// * `state` must not wrap around the end of the address space (no Rust object does).
+#[unsafe(naked)]
+pub(crate) unsafe extern "C" fn vg_sha224_init(state: *mut [u8; 96]) {
+    core::arch::naked_asm!(
+        "movz w9, #40664, lsl #0",
+        "movk w9, #49413, lsl #16",
+        "str w9, [x0, #0]",
+        "movz w9, #54535, lsl #0",
+        "movk w9, #13948, lsl #16",
+        "str w9, [x0, #4]",
+        "movz w9, #56599, lsl #0",
+        "movk w9, #12400, lsl #16",
+        "str w9, [x0, #8]",
+        "movz w9, #22841, lsl #0",
+        "movk w9, #63246, lsl #16",
+        "str w9, [x0, #12]",
+        "movz w9, #2865, lsl #0",
+        "movk w9, #65472, lsl #16",
+        "str w9, [x0, #16]",
+        "movz w9, #5393, lsl #0",
+        "movk w9, #26712, lsl #16",
+        "str w9, [x0, #20]",
+        "movz w9, #36775, lsl #0",
+        "movk w9, #25849, lsl #16",
+        "str w9, [x0, #24]",
+        "movz w9, #20388, lsl #0",
+        "movk w9, #48890, lsl #16",
+        "str w9, [x0, #28]",
+        "ret",
+    )
+}
+
 /// The SHA-256 compression function (FIPS 180-4 §6.2.2): updates the hash value `*state` with the `n` 64-byte blocks starting at `blocks`, in order.
 ///
 /// Contract: `VG.Spec.Sha256.compressContract`. Constant time: only the pointers and `n` may affect timing, not the hash value or the blocks.
diff --git a/src/asm/arm/sha256.rs b/src/asm/arm/sha256.rs
index ce598e523..9de762bf7 100644
--- a/src/asm/arm/sha256.rs
+++ b/src/asm/arm/sha256.rs
@@ -2,6 +2,45 @@
 //! Verified `sha256` functions for `arm`.
 #![allow(dead_code)]
 
+/// Starts a SHA-224 computation: makes the SHA-256 streaming state `*state` represent the empty message, hashed from the initial hash value of SHA-224 (`VG.Spec.Sha256.H0_224`). Continue with `vg_sha256_update` and `vg_sha256_finalize`, and take the first 28 bytes of the final hash value as the digest.
+///
+/// Contract: `VG.Spec.Sha256.init224Contract`. The streaming state is the hash value followed by a buffered partial block (`VG.Spec.Sha256.ReprFrom`).
+///
+/// # Safety
+///
+/// * `state` must be valid for reads and writes of 96 bytes.
+/// * `state` must not wrap around the end of the address space (no Rust object does).
+#[unsafe(naked)]
+pub(crate) unsafe extern "C" fn vg_sha224_init(state: *mut [u8; 96]) {
+    core::arch::naked_asm!(
+        "movw r12, #40664",
+        "movt r12, #49413",
+        "str r12, [r0, #0]",
+        "movw r12, #54535",
+        "movt r12, #13948",
+        "str r12, [r0, #4]",
+        "movw r12, #56599",
+        "movt r12, #12400",
+        "str r12, [r0, #8]",
+        "movw r12, #22841",
+        "movt r12, #63246",
+        "str r12, [r0, #12]",
+        "movw r12, #2865",
+        "movt r12, #65472",
+        "str r12, [r0, #16]",
+        "movw r12, #5393",
+        "movt r12, #26712",
+        "str r12, [r0, #20]",
+        "movw r12, #36775",
+        "movt r12, #25849",
+        "str r12, [r0, #24]",
+        "movw r12, #20388",
+        "movt r12, #48890",
+        "str r12, [r0, #28]",
+        "bx lr",
+    )
+}
+
 /// The SHA-256 compression function (FIPS 180-4 §6.2.2): updates the hash value `*state` with the `n` 64-byte blocks starting at `blocks`, in order.
 ///
 /// Contract: `VG.Spec.Sha256.compressContract`. Constant time: only the pointers and `n` may affect timing, not the hash value or the blocks.
diff --git a/src/asm/x86/sha256.rs b/src/asm/x86/sha256.rs
index 73703777b..4b3fdb184 100644
--- a/src/asm/x86/sha256.rs
+++ b/src/asm/x86/sha256.rs
@@ -2,6 +2,39 @@
 //! Verified `sha256` functions for `x86`.
 #![allow(dead_code)]
 
+/// Starts a SHA-224 computation: makes the SHA-256 streaming state `*state` represent the empty message, hashed from the initial hash value of SHA-224 (`VG.Spec.Sha256.H0_224`). Continue with `vg_sha256_update` and `vg_sha256_finalize`, and take the first 28 bytes of the final hash value as the digest.
+///
+/// Contract: `VG.Spec.Sha256.init224Contract`. The streaming state is the hash value followed by a buffered partial block (`VG.Spec.Sha256.ReprFrom`).
+///
+/// # Safety
+///
+/// * `state` must be valid for reads and writes of 96 bytes.
+/// * `state` must not overlap the arguments on the stack (distinct Rust objects never do).
+/// * `state` must not overlap the return address on the stack, or wrap around the end of the address space (no Rust object does).
+#[unsafe(naked)]
+pub(crate) unsafe extern "C" fn vg_sha224_init(state: *mut [u8; 96]) {
+    core::arch::naked_asm!(
+        "mov eax, DWORD PTR [esp+4]",
+        "mov ecx, -1056596264",
+        "mov DWORD PTR [eax], ecx",
+        "mov ecx, 914150663",
+        "mov DWORD PTR [eax+4], ecx",
+        "mov ecx, 812702999",
+        "mov DWORD PTR [eax+8], ecx",
+        "mov ecx, -150054599",
+        "mov DWORD PTR [eax+12], ecx",
+        "mov ecx, -4191439",
+        "mov DWORD PTR [eax+16], ecx",
+        "mov ecx, 1750603025",
+        "mov DWORD PTR [eax+20], ecx",
+        "mov ecx, 1694076839",
+        "mov DWORD PTR [eax+24], ecx",
+        "mov ecx, -1090891868",
+        "mov DWORD PTR [eax+28], ecx",
+        "ret",
+    )
+}
+
 /// Starts a SHA-256 computation: makes the streaming state `*state` represent the empty message.
 ///
 /// Contract: `VG.Spec.Sha256.initContract`. The streaming state is the hash value followed by a buffered partial block (`VG.Spec.Sha256.Repr`).
diff --git a/src/asm/x86_64/sha256.rs b/src/asm/x86_64/sha256.rs
index 3a8af49b2..6ad068da0 100644
--- a/src/asm/x86_64/sha256.rs
+++ b/src/asm/x86_64/sha256.rs
@@ -2,6 +2,37 @@
 //! Verified `sha256` functions for `x86_64`.
 #![allow(dead_code)]
 
+/// Starts a SHA-224 computation: makes the SHA-256 streaming state `*state` represent the empty message, hashed from the initial hash value of SHA-224 (`VG.Spec.Sha256.H0_224`). Continue with `vg_sha256_update` and `vg_sha256_finalize`, and take the first 28 bytes of the final hash value as the digest.
+///
+/// Contract: `VG.Spec.Sha256.init224Contract`. The streaming state is the hash value followed by a buffered partial block (`VG.Spec.Sha256.ReprFrom`).
+///
+/// # Safety
+///
+/// * `state` must be valid for reads and writes of 96 bytes.
+/// * `state` must not overlap the return address on the stack, or wrap around the end of the address space (no Rust object does).
+#[unsafe(naked)]
+pub(crate) unsafe extern "sysv64" fn vg_sha224_init(state: *mut [u8; 96]) {
+    core::arch::naked_asm!(
+        "mov eax, -1056596264",
+        "mov DWORD PTR [rdi], eax",
+        "mov eax, 914150663",
+        "mov DWORD PTR [rdi+4], eax",
+        "mov eax, 812702999",
+        "mov DWORD PTR [rdi+8], eax",
+        "mov eax, -150054599",
+        "mov DWORD PTR [rdi+12], eax",
+        "mov eax, -4191439",
+        "mov DWORD PTR [rdi+16], eax",
+        "mov eax, 1750603025",
+        "mov DWORD PTR [rdi+20], eax",
+        "mov eax, 1694076839",
+        "mov DWORD PTR [rdi+24], eax",
+        "mov eax, -1090891868",
+        "mov DWORD PTR [rdi+28], eax",
+        "ret",
+    )
+}
+
 /// The SHA-256 compression function (FIPS 180-4 §6.2.2): updates the hash value `*state` with the `n` 64-byte blocks starting at `blocks`, in order.
 ///
 /// Contract: `VG.Spec.Sha256.compressContract`. Constant time: only the pointers and `n` may affect timing, not the hash value or the blocks.
diff --git a/src/hashes/mod.rs b/src/hashes/mod.rs
index eb112b194..ccb5ce3a6 100644
--- a/src/hashes/mod.rs
+++ b/src/hashes/mod.rs
@@ -21,6 +21,7 @@ pub mod blake2b;
 pub mod blake2s;
 pub mod md5;
 pub mod sha1;
+pub mod sha224;
 pub mod sha256;
 pub mod sha3;
 pub mod sha512;
diff --git a/src/hashes/sha224.rs b/src/hashes/sha224.rs
new file mode 100644
index 000000000..fae080103
--- /dev/null
+++ b/src/hashes/sha224.rs
@@ -0,0 +1,124 @@
+//! SHA-224 (FIPS 180-4).
+//!
+//! SHA-224 is SHA-256 from another initial hash value, with its digest the
+//! first 28 bytes of the final hash value. `vg_sha224_init` (contract
+//! `VG.Spec.Sha256.init224Contract`) makes a SHA-256 streaming state
+//! represent the empty message, hashed from SHA-224's initial hash value
+//! (`VG.Spec.Sha256.ReprFrom`); SHA-256's `vg_sha256_update` and
+//! `vg_sha256_finalize` (`updateContract` and `finalizeContract`, which hold
+//! for any initial hash value) then absorb the message and output the final
+//! hash value.
+//!
+//! The implementations of `update` and `finalize` are SHA-256's, chosen the
+//! same way (see `super::sha256`).
+
+#![cfg(any(
+    target_arch = "x86_64",
+    target_arch = "aarch64",
+    target_arch = "arm",
+    target_arch = "x86"
+))]
+
+#[cfg(target_arch = "x86_64")]
+use crate::arch::sha256::{
+    VG_SHA256_FINALIZE_AVX2_FEATURES, VG_SHA256_FINALIZE_SHANI_FEATURES,
+    VG_SHA256_UPDATE_AVX2_FEATURES, VG_SHA256_UPDATE_SHANI_FEATURES, vg_sha256_finalize_avx2,
+    vg_sha256_finalize_shani, vg_sha256_update_avx2, vg_sha256_update_shani,
+};
+#[cfg(target_arch = "aarch64")]
+use crate::arch::sha256::{
+    VG_SHA256_FINALIZE_SHA2_FEATURES, VG_SHA256_UPDATE_SHA2_FEATURES, vg_sha256_finalize_sha2,
+    vg_sha256_update_sha2,
+};
+use crate::arch::sha256::{vg_sha224_init, vg_sha256_finalize, vg_sha256_update};
+
+super::streaming_hash!(
+    /// An incremental SHA-224 computation (FIPS 180-4 §6.3).
+    Sha224 {
+        state: 96,
+        scratch: 76,
+        block: 64,
+        output: 28,
+        final_hash: 32,
+        init: vg_sha224_init,
+        backends: Sha224Backend {
+            Scalar => (vg_sha256_update, vg_sha256_finalize),
+            #[cfg(target_arch = "aarch64")]
+            Sha2 if [VG_SHA256_UPDATE_SHA2_FEATURES, VG_SHA256_FINALIZE_SHA2_FEATURES] =>
+                (vg_sha256_update_sha2, vg_sha256_finalize_sha2),
+            #[cfg(target_arch = "x86_64")]
+            ShaNi if [VG_SHA256_UPDATE_SHANI_FEATURES, VG_SHA256_FINALIZE_SHANI_FEATURES] =>
+                (vg_sha256_update_shani, vg_sha256_finalize_shani),
+            #[cfg(target_arch = "x86_64")]
+            Avx2 if [VG_SHA256_UPDATE_AVX2_FEATURES, VG_SHA256_FINALIZE_AVX2_FEATURES] =>
+                (vg_sha256_update_avx2, vg_sha256_finalize_avx2),
+        },
+    }
+);
+
+#[cfg(test)]
+mod tests {
+    use super::{Sha224, Sha224Backend};
+    use crate::cpu::{Features, detected};
+    use crate::hashes::sha256::Sha256Backend;
+
+    /// Every way of splitting a message into two updates gives the same
+    /// digest, for every length around the padding boundaries.
+    #[test]
+    fn incremental() {
+        let msg: [u8; 200] = core::array::from_fn(|i| (i * 7 + 3) as u8);
+        for len in 0..msg.len() {
+            let expected = Sha224::digest(&msg[..len]);
+            for split in 0..=len {
+                let mut h = Sha224::default();
+                h.update(&msg[..split]);
+                let copy = h.clone();
+                h.update(&msg[split..len]);
+                assert_eq!(h.finalize(), expected);
+                let mut h = copy;
+                for byte in &msg[split..len] {
+                    h.update(core::slice::from_ref(byte));
+                }
+                assert_eq!(h.finalize(), expected);
+            }
+        }
+    }
+
+    /// The implementation chosen for each set of features is SHA-256's.
+    #[test]
+    fn select() {
+        for bits in 0..(1 << crate::cpu::NAMES.len()) {
+            let f = Features(bits);
+            let expected = match Sha256Backend::select(f) {
+                Sha256Backend::Scalar => Sha224Backend::Scalar,
+                #[cfg(target_arch = "aarch64")]
+                Sha256Backend::Sha2 => Sha224Backend::Sha2,
+                #[cfg(target_arch = "x86_64")]
+                Sha256Backend::ShaNi => Sha224Backend::ShaNi,
+                #[cfg(target_arch = "x86_64")]
+                Sha256Backend::Avx2 => Sha224Backend::Avx2,
+            };
+            assert_eq!(Sha224Backend::select(f), expected, "{bits:#b}");
+        }
+        assert_eq!(Sha224::new().backend, Sha224Backend::select(detected()));
+    }
+
+    /// The `HashFunction` implementation is the inherent functions.
+    #[test]
+    fn hash_function() {
+        use crate::hashes::HashFunction;
+        let msg = [0x5a; 300];
+        let mut h = <Sha224 as HashFunction>::new();
+        HashFunction::update(&mut h, &msg[..100]);
+        HashFunction::update(&mut h, &msg[100..]);
+        assert_eq!(HashFunction::finalize(h), Sha224::digest(&msg));
+        assert_eq!(<Sha224 as HashFunction>::digest(&msg), Sha224::digest(&msg));
+        assert_eq!(
+            (
+                <Sha224 as HashFunction>::OUTPUT_SIZE,
+                <Sha224 as HashFunction>::BLOCK_SIZE
+            ),
+            (28, 64)
+        );
+    }
+}
diff --git a/tests/cavp/main.rs b/tests/cavp/main.rs
index 98a9c7226..59211fdce 100644
--- a/tests/cavp/main.rs
+++ b/tests/cavp/main.rs
@@ -16,6 +16,7 @@
 mod aes_gcm;
 mod rc2_cbc;
 mod sha1;
+mod sha224;
 mod sha256;
 mod sha3;
 mod sha512;
diff --git a/tests/cavp/sha224.rs b/tests/cavp/sha224.rs
new file mode 100644
index 000000000..8d201290e
--- /dev/null
+++ b/tests/cavp/sha224.rs
@@ -0,0 +1,33 @@
+//! SHA-224: every message length from 0 to 64 bytes, 64 long messages and the
+//! Monte Carlo test.
+
+use super::{check_messages, check_monte_carlo};
+use verified_garbage::hashes::sha224::Sha224;
+
+/// Every message length from 0 to 64 bytes.
+#[test]
+fn short_messages() {
+    let n = check_messages(
+        include_str!("../../vectors/nist-cavp/sha224/SHA224ShortMsg.rsp"),
+        Sha224::digest,
+    );
+    assert_eq!(n, 65);
+}
+
+#[test]
+fn long_messages() {
+    let n = check_messages(
+        include_str!("../../vectors/nist-cavp/sha224/SHA224LongMsg.rsp"),
+        Sha224::digest,
+    );
+    assert_eq!(n, 64);
+}
+
+/// The SHAVS Monte Carlo test.
+#[test]
+fn monte_carlo() {
+    check_monte_carlo(
+        include_str!("../../vectors/nist-cavp/sha224/SHA224Monte.rsp"),
+        Sha224::digest,
+    );
+}