diff --git a/Arm/Insts/DPSFP/Crypto_aes.lean b/Arm/Insts/DPSFP/Crypto_aes.lean
index 406674e9..c6cff4e3 100644
--- a/Arm/Insts/DPSFP/Crypto_aes.lean
+++ b/Arm/Insts/DPSFP/Crypto_aes.lean
@@ -52,8 +52,7 @@ def FFmul02 (b : BitVec 8) : BitVec 8 :=
     ]
   let lo := b.toNat * 8
   let hi := lo + 7
-  have h : hi - lo + 1 = 8 := by omega
-  h ▸ extractLsb hi lo $ BitVec.flatten FFmul_02
+  BitVec.cast (by omega) $ extractLsb hi lo $ BitVec.flatten FFmul_02
 
 def FFmul03 (b : BitVec 8) : BitVec 8 :=
   let FFmul_03 :=
@@ -77,8 +76,7 @@ def FFmul03 (b : BitVec 8) : BitVec 8 :=
     ]
   let lo := b.toNat * 8
   let hi := lo + 7
-  have h : hi - lo + 1 = 8 := by omega
-  h ▸ extractLsb hi lo $ BitVec.flatten FFmul_03
+  BitVec.cast (by omega) $ extractLsb hi lo $ BitVec.flatten FFmul_03
 
 def AESMixColumns (op : BitVec 128) : BitVec 128 :=
   AESCommon.MixColumns op FFmul02 FFmul03
diff --git a/Specs/AES.lean b/Specs/AES.lean
index 21f7958e..7eb13640 100644
--- a/Specs/AES.lean
+++ b/Specs/AES.lean
@@ -23,7 +23,7 @@ import Specs.AESCommon
 -- ShiftRows
 -- AddRoundKey key10
 --
--- The Arm implementation has an optimization that shifts the rounds:
+-- The Arm implementation has an optimization that commute intermediate steps:
 --
 -- for k in key0 to key8
 --   AddRoundKey + ShiftRows + SubBytes (AESE k)
@@ -43,8 +43,9 @@ open BitVec
 def WordSize := 32
 def BlockSize := 128
 
--- Maybe consider Lists vs Vectors?
+-- General comment: Maybe consider Lists vs Vectors?
 -- https://github.com/joehendrix/lean-crypto/blob/323ee9b1323deed5240762f4029700a246ecd9d5/lib/Crypto/Vector.lean#L96
+
 def Rcon : List (BitVec WordSize) :=
 [ 0x00000001#32,
   0x00000002#32,
@@ -96,7 +97,7 @@ def sbox (ind : BitVec 8) : BitVec 8 :=
       (x.toNat * 128 + y.toNat * 8) $ BitVec.flatten AESCommon.SBOX
   | _ => ind -- unreachable case
 
--- Little endian
+-- Note: The RotWord function is written in little endian
 def RotWord (w : BitVec WordSize) : BitVec WordSize :=
   match_bv w with
   | [a3:8, a2:8, a1:8, a0:8] => a0 ++ a3 ++ a2 ++ a1
@@ -154,8 +155,8 @@ def ShiftRows {Param : KBR} (state : BitVec Param.block_size)
   h ▸ AESCommon.ShiftRows (h ▸ state)
 
 def XTimes (bv : BitVec 8) : BitVec 8 :=
-  let res := extractLsb 6 0 bv ++ 0b0#1
-  if extractLsb 7 7 bv == 0b0#1 then res else res ^^^ 0b00011011#8
+  let res := truncate 7 bv ++ 0b0#1
+  if getLsb bv 7 then res ^^^ 0b00011011#8 else res
 
 def MixColumns {Param : KBR} (state : BitVec Param.block_size)
   : BitVec Param.block_size :=
@@ -164,25 +165,25 @@ def MixColumns {Param : KBR} (state : BitVec Param.block_size)
   let FFmul03 := fun (x : BitVec 8) => x ^^^ XTimes x
   h ▸ AESCommon.MixColumns (h ▸ state) FFmul02 FFmul03
 
--- TODO : Prove the following lemma
+-- TODO: looks like a SAT/SMT problem
+protected theorem FFmul02_equiv : (fun x => XTimes x) = DPSFP.FFmul02 := by
+  funext x
+  simp only [XTimes, DPSFP.FFmul02]
+  sorry
+
+-- TODO: looks like a SAT/SMT problem
+protected theorem FFmul03_equiv : (fun x => x ^^^ XTimes x) = DPSFP.FFmul03 := by
+  funext x
+  simp only [XTimes, DPSFP.FFmul03]
+  sorry
+
+
 theorem MixColumns_table_lookup_equiv {Param : KBR}
   (state : BitVec Param.block_size):
   have h : Param.block_size = 128 := by simp only [Param.h, BlockSize]
   MixColumns (Param := Param) state = h ▸ DPSFP.AESMixColumns (h ▸ state) := by
     simp only [MixColumns, DPSFP.AESMixColumns]
-    have h₀ : (fun x => XTimes x) = DPSFP.FFmul02 := by
-      funext x
-      simp only [XTimes, DPSFP.FFmul02]
-      simp only [Nat.reduceSub, Nat.reduceAdd, beq_iff_eq, Nat.sub_zero, List.length_cons, List.length_nil,
-      Nat.reduceSucc, Nat.reduceMul]
-      sorry -- looks like a sat problem
-    have h₁ : (fun x => x ^^^ XTimes x) = DPSFP.FFmul03 := by
-      funext x
-      simp only [XTimes, DPSFP.FFmul03]
-      simp only [Nat.reduceSub, Nat.reduceAdd, beq_iff_eq, Nat.sub_zero, List.length_cons, List.length_nil,
-      Nat.reduceSucc, Nat.reduceMul]
-      sorry -- looks like a sat problem
-    rw [h₀, h₁]
+    rw [AES.FFmul02_equiv, AES.FFmul03_equiv]
 
 def AddRoundKey {Param : KBR} (state : BitVec Param.block_size)
   (roundKey : BitVec Param.block_size) : BitVec Param.block_size :=
diff --git a/Specs/AESCommon.lean b/Specs/AESCommon.lean
index cffaae16..5d2f8c58 100644
--- a/Specs/AESCommon.lean
+++ b/Specs/AESCommon.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author(s): Shilpi Goel
+Author(s): Shilpi Goel, Yan Peng
 -/
 import Arm.BitVec
 
diff --git a/Specs/GCM.lean b/Specs/GCM.lean
new file mode 100644
index 00000000..ed5d77f7
--- /dev/null
+++ b/Specs/GCM.lean
@@ -0,0 +1,198 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Yan Peng
+-/
+import Arm.BitVec
+import Arm.Insts.Common
+
+-- References: https://nvlpubs.nist.gov/nistpubs/legacy/sp/nistspecialpublication800-38d.pdf
+
+namespace GCM
+
+open BitVec
+
+def R : (BitVec 128) := 0b11100001#8 ++ 0b0#120
+
+/-- A Cipher type is a function that takes an input of size n and
+    a key of size m and returns an encrypted block of size n -/
+abbrev Cipher {n : Nat} {m : Nat} :=  BitVec n → BitVec m → BitVec n
+
+/-- The s-bit incrementing function -/
+def inc_s (s : Nat) (X : BitVec l) (H₀ : 0 < s) (H₁ : s < l) : BitVec l :=
+  let msb_hi := l - 1
+  let msb_lo := s
+  let lsb_hi := s - 1
+  let lsb_lo := 0
+  have h₁ : lsb_hi - lsb_lo + 1 = s := by omega
+  let upper := extractLsb msb_hi msb_lo X
+  let lower := h₁ ▸ (extractLsb lsb_hi lsb_lo X) + 0b1#s
+  have h₂ : msb_hi - msb_lo + 1 + s = l := by omega
+  h₂ ▸ (upper ++ lower)
+
+def mul_aux (i : Nat) (X : BitVec 128) (Z : BitVec 128) (V : BitVec 128)
+  : BitVec 128 :=
+  if h : 128 ≤ i then
+    Z
+  else
+    let Xi := getMsb X i
+    let Z := if not Xi then Z else Z ^^^ V
+    let lsb_v := getLsb V 0
+    let V := if not lsb_v then V >>> 1 else (V >>> 1) ^^^ R
+    mul_aux (i + 1) X Z V
+  termination_by (128 - i)
+
+/-- The GF(2^128) multiplication -/
+def mul (X : BitVec 128) (Y : BitVec 128) : BitVec 128 :=
+  mul_aux 0 X 0b0#128 Y
+
+def GHASH_aux (i : Nat) (H : BitVec 128) (X : BitVec n) (Y : BitVec 128)
+  (h : 128 ∣ n) : BitVec 128 :=
+  if n / 128 ≤ i then
+    Y
+  else
+    let lo := i * 128
+    let hi := lo + 127
+    have h₀ : hi - lo + 1 = 128 := by omega
+    let Xi := extractLsb hi lo X
+    let res := rev_elems 128 8 (Y ^^^ (h₀ ▸ Xi)) (by decide) (by decide)
+    let H_rev := rev_elems 128 8 H (by decide) (by decide)
+    let Y := mul res H_rev
+    let Y := rev_elems 128 8 Y (by decide) (by decide)
+    GHASH_aux (i + 1) H X Y h
+  termination_by (n / 128 - i)
+
+/-- GHASH: hashing message X using Galois field multiplication -/
+def GHASH (H : BitVec 128) (X : BitVec n) (h : 128 ∣ n) : BitVec 128 :=
+  GHASH_aux 0 H X (BitVec.zero 128) h
+
+def GCTR_aux (CIPH : Cipher (n := 128) (m := m))
+  (i : Nat) (n : Nat) (K : BitVec m) (ICB : BitVec 128)
+  (X : BitVec v) (Y : BitVec v) : BitVec v :=
+  if n ≤ i then
+    Y
+  else
+    let lo := i * 128
+    let hi := lo + 127
+    have h : hi - lo + 1 = 128 := by omega
+    -- extractLsb will fill upper bits with zeros if hi >= len X
+    let Xi := extractLsb hi lo X
+    -- reversing counter because AES expects little-endian
+    let ICB_rev := rev_elems 128 8 ICB (by decide) (by decide)
+    let Yi := h ▸ Xi ^^^ CIPH ICB_rev K
+    -- partInstall ignores val indexes that exceeds length of Y
+    let Y := BitVec.partInstall hi lo (h.symm ▸ Yi) Y
+    let ICB := inc_s 32 ICB (by omega) (by omega)
+    GCTR_aux CIPH (i + 1) n K ICB X Y
+  termination_by (n - i)
+
+protected def ceiling_in_blocks (w : Nat) := (w - 1) / 128 + 1
+protected def ceiling_in_bits (w : Nat) := (GCM.ceiling_in_blocks w) * 128
+
+protected theorem bits_le_ceiling_in_bits (w : Nat) :
+  w ≤ (GCM.ceiling_in_blocks w) * 128 := by
+  simp only [GCM.ceiling_in_blocks]
+  omega
+
+/-- GCTR: encrypting/decrypting message x using Galois counter mode -/
+def GCTR {m : Nat} (CIPH : Cipher (n := 128) (m := m))
+  (K : BitVec m) (ICB : BitVec 128) (X : BitVec v) : (BitVec v) :=
+  let n := GCM.ceiling_in_blocks v
+  GCTR_aux CIPH 0 n K ICB X $ BitVec.zero v
+
+protected theorem initialize_J0_simplification
+  (lv : Nat) (x : Nat) (h : lv ≤ x * 128):
+  lv + (x * 128 - lv + 64) + 64  = x * 128 + 128 := by omega
+
+protected def initialize_J0 (H : BitVec 128) (IV : BitVec lv) :=
+  if h₀ : lv == 96
+  then have h₁ : lv + 31 + 1 = 128 := by
+         simp only [Nat.succ.injEq]
+         exact Nat.eq_of_beq_eq_true h₀
+       h₁ ▸ (IV ++ BitVec.zero 31 ++ 0b1#1)
+  else let s := GCM.ceiling_in_bits lv - lv
+       have h₂ : 128 ∣ (lv + (s + 64) + 64) := by
+         simp only [s, GCM.ceiling_in_bits]
+         rw [GCM.initialize_J0_simplification lv (GCM.ceiling_in_blocks lv)
+             (by apply GCM.bits_le_ceiling_in_bits)]
+         omega
+       have h₃ : 8 ∣ (lv + (s + 64) + 64) := by
+         simp only [s, GCM.ceiling_in_bits]
+         rw [GCM.initialize_J0_simplification lv (GCM.ceiling_in_blocks lv)
+             (by apply GCM.bits_le_ceiling_in_bits)]
+         omega
+       let block := rev_elems (lv + (s + 64 ) + 64) 8
+                      (IV ++ (BitVec.zero (s + 64)) ++ (BitVec.ofNat 64 lv))
+                      h₃ (by decide)
+       rev_elems 128 8 (GHASH H block h₂) (by decide) (by decide)
+
+protected theorem GCM_AE_DE_simplification1 (a : Nat) (v : Nat) (p : Nat) (u : Nat) :
+  64 + 64 + u + p + v + a = 128 + (u + p) + (v + a) := by omega
+
+protected theorem GCM_AE_DE_simplification2
+  (y : Nat) (x : Nat) (h : y ≤ x * 128):
+  (x * 128 - y) + y = x * 128 := by omega
+
+/-- GCM_AE : Galois Counter Mode Authenticated Encryption -/
+def GCM_AE {m : Nat} (CIPH : Cipher (n := 128) (m := m))
+  (K : BitVec m) (IV : BitVec lv) (P : BitVec p) (A : BitVec a) (t : Nat)
+  : (BitVec p) × (BitVec t) :=
+  let H := CIPH (BitVec.zero 128) K
+  let J0 : BitVec 128 := GCM.initialize_J0 H IV
+  let ICB := inc_s 32 J0 (by decide) (by decide)
+  let C := GCTR (m := m) CIPH K ICB P
+  let u := GCM.ceiling_in_bits p - p
+  let v := GCM.ceiling_in_bits a - a
+  let block := rev_elems 64 8 (BitVec.ofNat 64 p) (by decide) (by decide)
+               ++ rev_elems 64 8 (BitVec.ofNat 64 a) (by decide) (by decide)
+               ++ BitVec.zero u ++ C ++ BitVec.zero v ++ A
+  have h : 128 ∣ 64 + 64 + u + p + v + a := by
+    rw [GCM.GCM_AE_DE_simplification1]
+    simp only [u, v]
+    simp only [GCM.ceiling_in_bits]
+    rw [GCM.GCM_AE_DE_simplification2 p (GCM.ceiling_in_blocks p)
+        (by apply GCM.bits_le_ceiling_in_bits)]
+    rw [GCM.GCM_AE_DE_simplification2 a (GCM.ceiling_in_blocks a)
+        (by apply GCM.bits_le_ceiling_in_bits)]
+    omega
+  let S := GHASH H block h
+  let T := truncate t $ GCTR (m := m) CIPH K J0 S
+  (C, T)
+
+def length_constraints (_IV : BitVec v) (_A : BitVec a) (_C : BitVec c)
+  : Bool :=
+     1 ≤ v && v ≤ 2^64 - 1
+  && c ≤ 2^39 - 256
+  && a ≤ 2^64 - 1
+
+/-- GCM_AD : Galois Counter Mode Authenticated Decryption
+    GCM_AD returns none when decryption fails. -/
+def GCM_AD {m : Nat} (CIPH : Cipher (n := 128) (m := m))
+  (K : BitVec m) (IV : BitVec lv) (C : BitVec c) (A : BitVec a) (T : BitVec t)
+  : Option (BitVec c) :=
+  if not $ length_constraints IV C A then
+    none
+  else
+    let H := CIPH (BitVec.zero 128) K
+    let J0 := GCM.initialize_J0 H IV
+    let ICB := inc_s 32 J0 (by decide) (by decide)
+    let P := GCTR (m := m) CIPH K ICB C
+    let u := GCM.ceiling_in_bits c - c
+    let v := GCM.ceiling_in_bits a - a
+    let block := rev_elems 64 8 (BitVec.ofNat 64 c) (by decide) (by decide)
+                 ++ rev_elems 64 8 (BitVec.ofNat 64 a) (by decide) (by decide)
+                 ++ BitVec.zero u ++ C ++ BitVec.zero v ++ A
+    have h : 128 ∣ 64 + 64 + u + c + v + a := by
+      rw [GCM.GCM_AE_DE_simplification1]
+      simp only [u, v]
+      simp only [GCM.ceiling_in_bits]
+      rw [GCM.GCM_AE_DE_simplification2 c (GCM.ceiling_in_blocks c)
+          (by apply GCM.bits_le_ceiling_in_bits)]
+      rw [GCM.GCM_AE_DE_simplification2 a (GCM.ceiling_in_blocks a)
+          (by apply GCM.bits_le_ceiling_in_bits)]
+      omega
+    let S := GHASH H block h
+    let T' := truncate t $ GCTR (m := m) CIPH K J0 S
+    if T == T' then some P else none
+
+end GCM
diff --git a/Specs/Specs.lean b/Specs/Specs.lean
index 8ef481da..9586f35f 100644
--- a/Specs/Specs.lean
+++ b/Specs/Specs.lean
@@ -5,3 +5,5 @@ Author(s): Shilpi Goel
 -/
 import «Specs».SHA512
 import «Specs».AESCommon
+import «Specs».AES
+import «Specs».GCM
diff --git a/Tests/AESGCMSpecTest.lean b/Tests/AESGCMSpecTest.lean
new file mode 100644
index 00000000..2340aff3
--- /dev/null
+++ b/Tests/AESGCMSpecTest.lean
@@ -0,0 +1,166 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Yan Peng
+-/
+import Arm.BitVec
+import Specs.AES
+import Specs.GCM
+
+-- Reference: https://csrc.nist.rip/groups/ST/toolkit/BCM/documents/proposedmodes/gcm/gcm-spec.pdf
+
+namespace AES256GCMSpecTest
+
+open BitVec
+
+def CIPH_128 : GCM.Cipher (n := 128) (m := 128) :=
+  AES.AES_encrypt (Param := AES.AES128KBR)
+
+def GCM_AE_128 : BitVec 128 → BitVec lv → BitVec p → BitVec a → (t : Nat)
+  → (BitVec p) × (BitVec t) := GCM.GCM_AE (m := 128) CIPH_128
+
+def GCM_AD_128 : BitVec 128 → BitVec lv → BitVec c → BitVec a → BitVec t
+  → Option (BitVec c) := GCM.GCM_AD (m := 128) CIPH_128
+
+def CIPH_256 : GCM.Cipher (n := 128) (m := 256) :=
+  AES.AES_encrypt (Param := AES.AES256KBR)
+
+def GCM_AE_256 : BitVec 256 → BitVec lv → BitVec p → BitVec a → (t : Nat)
+  → (BitVec p) × (BitVec t) := GCM.GCM_AE (m := 256) CIPH_256
+
+def GCM_AD_256 : BitVec 256 → BitVec lv → BitVec c → BitVec a → BitVec t
+  → Option (BitVec c) := GCM.GCM_AD (m := 256) CIPH_256
+
+-- Test Vector 0
+
+def K0 : BitVec 128 := 0
+def IV0 : BitVec 96 := 0
+def P0 : BitVec 0 := BitVec.nil
+def A0 : BitVec 0 := BitVec.nil
+def C0 : BitVec 0 := BitVec.nil
+def T0 : BitVec 128 := rev_elems 128 8 0x58e2fccefa7e3061367f1d57a4e7455a#128 (by decide) (by decide)
+example : GCM_AE_128 K0 IV0 P0 A0 128 = (C0, T0) := by native_decide
+example : GCM_AD_128 K0 IV0 C0 A0 T0 = P0 := by native_decide
+
+-- Test Vector 1
+
+def K1 : BitVec 128 := 0
+def IV1 : BitVec 96 := 0
+def P1 : BitVec 128 := 0
+def A1 : BitVec 0 := BitVec.nil
+def C1 : BitVec 128 := rev_elems 128 8 0x0388dace60b6a392f328c2b971b2fe78#128 (by decide) (by decide)
+def T1 : BitVec 128 := rev_elems 128 8 0xab6e47d42cec13bdf53a67b21257bddf#128 (by decide) (by decide)
+example : GCM_AE_128 K1 IV1 P1 A1 128 = (C1, T1) := by native_decide
+example : GCM_AD_128 K1 IV1 C1 A1 T1 = P1 := by native_decide
+
+-- Test Vector 2
+
+def K2 : BitVec 128 := rev_elems 128 8 0xfeffe9928665731c6d6a8f9467308308#128 (by decide) (by decide)
+def IV2 : BitVec 96 := 0xcafebabefacedbaddecaf888#96
+def P2 : BitVec 512 := rev_elems 512 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255#512 (by decide) (by decide)
+def A2 : BitVec 0 := BitVec.nil
+def C2 : BitVec 512 := rev_elems 512 8 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091473f5985#512 (by decide) (by decide)
+def T2 : BitVec 128 := rev_elems 128 8 0x4d5c2af327cd64a62cf35abd2ba6fab4#128 (by decide) (by decide)
+example : GCM_AE_128 K2 IV2 P2 A2 128 = (C2, T2) := by native_decide
+example : GCM_AD_128 K2 IV2 C2 A2 T2 = P2 := by native_decide
+
+-- Test Vector 3
+
+def K3 : BitVec 128 := rev_elems 128 8 0xfeffe9928665731c6d6a8f9467308308#128 (by decide) (by decide)
+def IV3 : BitVec 96 := 0xcafebabefacedbaddecaf888#96
+def P3 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide)
+def A3 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide)
+def C3 : BitVec 480 := rev_elems 480 8 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091#480 (by decide) (by decide)
+def T3 : BitVec 128 := rev_elems 128 8 0x5bc94fbc3221a5db94fae95ae7121a47#128 (by decide) (by decide)
+example : GCM_AE_128 K3 IV3 P3 A3 128 = (C3, T3) := by native_decide
+example : GCM_AD_128 K3 IV3 C3 A3 T3 = P3 := by native_decide
+
+-- Test Vector 4
+
+def K4 : BitVec 128 := rev_elems 128 8 0xfeffe9928665731c6d6a8f9467308308#128 (by decide) (by decide)
+def IV4 : BitVec 64 := 0xcafebabefacedbad#64
+def P4 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide)
+def A4 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide)
+def C4 : BitVec 480 := rev_elems 480 8 0x61353b4c2806934a777ff51fa22a4755699b2a714fcdc6f83766e5f97b6c742373806900e49f24b22b097544d4896b424989b5e1ebac0f07c23f4598#480 (by decide) (by decide)
+def T4 : BitVec 128 := rev_elems 128 8 0x3612d2e79e3b0785561be14aaca2fccb#128 (by decide) (by decide)
+example : GCM_AE_128 K4 IV4 P4 A4 128 = (C4, T4) := by native_decide
+example : GCM_AD_128 K4 IV4 C4 A4 T4 = P4 := by native_decide
+
+-- Test Vector 5
+
+def K5 : BitVec 128 := rev_elems 128 8 0xfeffe9928665731c6d6a8f9467308308#128 (by decide) (by decide)
+def IV5 : BitVec 480 := 0x9313225df88406e555909c5aff5269aa6a7a9538534f7da1e4c303d2a318a728c3c0c95156809539fcf0e2429a6b525416aedbf5a0de6a57a637b39b#480
+def P5 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide)
+def A5 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide)
+def C5 : BitVec 480 := rev_elems 480 8 0x8ce24998625615b603a033aca13fb894be9112a5c3a211a8ba262a3cca7e2ca701e4a9a4fba43c90ccdcb281d48c7c6fd62875d2aca417034c34aee5#480 (by decide) (by decide)
+def T5 : BitVec 128 := rev_elems 128 8 0x619cc5aefffe0bfa462af43c1699d050#128 (by decide) (by decide)
+example : GCM_AE_128 K5 IV5 P5 A5 128 = (C5, T5) := by native_decide
+example : GCM_AD_128 K5 IV5 C5 A5 T5 = P5 := by native_decide
+
+-- Test Vector 6
+
+def K6 : BitVec 256 := 0
+def IV6 : BitVec 96 := 0
+def P6 : BitVec 0 := BitVec.nil
+def A6 : BitVec 0 := BitVec.nil
+def C6 : BitVec 0 := BitVec.nil
+def T6 : BitVec 128 := rev_elems 128 8 0x530f8afbc74536b9a963b4f1c4cb738b#128 (by decide) (by decide)
+example : GCM_AE_256 K6 IV6 P6 A6 128 = (C6, T6) := by native_decide
+example : GCM_AD_256 K6 IV6 C6 A6 T6 = P6 := by native_decide
+
+-- Test Vector 7
+
+def K7 : BitVec 256 := 0
+def IV7 : BitVec 96 := 0
+def P7 : BitVec 128 := 0
+def A7 : BitVec 0 := BitVec.nil
+def C7 : BitVec 128 := rev_elems 128 8 0xcea7403d4d606b6e074ec5d3baf39d18#128 (by decide) (by decide)
+def T7 : BitVec 128 := rev_elems 128 8 0xd0d1c8a799996bf0265b98b5d48ab919#128 (by decide) (by decide)
+example : GCM_AE_256 K7 IV7 P7 A7 128 = (C7, T7) := by native_decide
+example : GCM_AD_256 K7 IV7 C7 A7 T7 = P7 := by native_decide
+
+-- Test Vector 8
+
+def K8 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide)
+def IV8 : BitVec 96 := 0xcafebabefacedbaddecaf888#96
+def P8 : BitVec 512 := rev_elems 512 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255#512 (by decide) (by decide)
+def A8 : BitVec 0 := BitVec.nil
+def C8 : BitVec 512 := rev_elems 512 8 0x522dc1f099567d07f47f37a32a84427d643a8cdcbfe5c0c97598a2bd2555d1aa8cb08e48590dbb3da7b08b1056828838c5f61e6393ba7a0abcc9f662898015ad#512 (by decide) (by decide)
+def T8 : BitVec 128 := rev_elems 128 8 0xb094dac5d93471bdec1a502270e3cc6c#128 (by decide) (by decide)
+example : GCM_AE_256 K8 IV8 P8 A8 128 = (C8, T8) := by native_decide
+example : GCM_AD_256 K8 IV8 C8 A8 T8 = P8 := by native_decide
+
+-- Test Vector 9
+
+def K9 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide)
+def IV9 : BitVec 96 := 0xcafebabefacedbaddecaf888#96
+def P9 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide)
+def A9 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide)
+def C9 : BitVec 480 := rev_elems 480 8 0x522dc1f099567d07f47f37a32a84427d643a8cdcbfe5c0c97598a2bd2555d1aa8cb08e48590dbb3da7b08b1056828838c5f61e6393ba7a0abcc9f662#480 (by decide) (by decide)
+def T9 : BitVec 128 := rev_elems 128 8 0x76fc6ece0f4e1768cddf8853bb2d551b#128 (by decide) (by decide)
+example : GCM_AE_256 K9 IV9 P9 A9 128 = (C9, T9) := by native_decide
+example : GCM_AD_256 K9 IV9 C9 A9 T9 = P9 := by native_decide
+
+-- Test Vector 10 (17)
+
+def K10 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide)
+def IV10 : BitVec 64:= 0xcafebabefacedbad#64
+def P10 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide)
+def A10 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide)
+def C10 : BitVec 480 := rev_elems 480 8 0xc3762df1ca787d32ae47c13bf19844cbaf1ae14d0b976afac52ff7d79bba9de0feb582d33934a4f0954cc2363bc73f7862ac430e64abe499f47c9b1f#480 (by decide) (by decide)
+def T10 : BitVec 128 := rev_elems 128 8 0x3a337dbf46a792c45e454913fe2ea8f2#128 (by decide) (by decide)
+example : GCM_AE_256 K10 IV10 P10 A10 128 = (C10, T10) := by native_decide
+example : GCM_AD_256 K10 IV10 C10 A10 T10 = P10 := by native_decide
+
+-- Test Vector 11
+
+def K11 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide)
+def IV11 : BitVec 480 := 0x9313225df88406e555909c5aff5269aa6a7a9538534f7da1e4c303d2a318a728c3c0c95156809539fcf0e2429a6b525416aedbf5a0de6a57a637b39b#480
+def P11 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide)
+def A11 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide)
+def C11 : BitVec 480 := rev_elems 480 8 0x5a8def2f0c9e53f1f75d7853659e2a20eeb2b22aafde6419a058ab4f6f746bf40fc0c3b780f244452da3ebf1c5d82cdea2418997200ef82e44ae7e3f#480 (by decide) (by decide)
+def T11 : BitVec 128 := rev_elems 128 8 0xa44a8266ee1c8eb0c8b5d4cf5ae9f19a#128 (by decide) (by decide)
+example : GCM_AE_256 K11 IV11 P11 A11 128 = (C11, T11) := by native_decide
+example : GCM_AD_256 K11 IV11 C11 A11 T11 = P11 := by native_decide
+
+end AES256GCMSpecTest
diff --git a/Tests/Tests.lean b/Tests/Tests.lean
index 767bc04a..723c8577 100644
--- a/Tests/Tests.lean
+++ b/Tests/Tests.lean
@@ -10,4 +10,5 @@ import «Tests».SHA512SpecTest
 import «Tests».SHA512ProgramTest
 import «Tests».LDSTTest
 import «Tests».AESSpecTest
+import «Tests».AESGCMSpecTest