diff --git a/Arm/Insts/DPSFP/Crypto_aes.lean b/Arm/Insts/DPSFP/Crypto_aes.lean
index 32a8d09b..c6cff4e3 100644
--- a/Arm/Insts/DPSFP/Crypto_aes.lean
+++ b/Arm/Insts/DPSFP/Crypto_aes.lean
@@ -8,6 +8,7 @@ Author(s): Shilpi Goel, Yan Peng
 import Arm.Decode
 import Arm.Insts.Common
 import Arm.BitVec
+import Specs.AESCommon
 
 ----------------------------------------------------------------------
 
@@ -15,52 +16,6 @@ namespace DPSFP
 
 open BitVec
 
-def SBox :=
-  --   F E D C B A 9 8 7 6 5 4 3 2 1 0
-  [ 0x16bb54b00f2d99416842e6bf0d89a18c#128, -- F
-    0xdf2855cee9871e9b948ed9691198f8e1#128, -- E
-    0x9e1dc186b95735610ef6034866b53e70#128, -- D
-    0x8a8bbd4b1f74dde8c6b4a61c2e2578ba#128, -- C
-    0x08ae7a65eaf4566ca94ed58d6d37c8e7#128, -- B
-    0x79e4959162acd3c25c2406490a3a32e0#128, -- A
-    0xdb0b5ede14b8ee4688902a22dc4f8160#128, -- 9
-    0x73195d643d7ea7c41744975fec130ccd#128, -- 8
-    0xd2f3ff1021dab6bcf5389d928f40a351#128, -- 7
-    0xa89f3c507f02f94585334d43fbaaefd0#128, -- 6
-    0xcf584c4a39becb6a5bb1fc20ed00d153#128, -- 5
-    0x842fe329b3d63b52a05a6e1b1a2c8309#128, -- 4
-    0x75b227ebe28012079a059618c323c704#128, -- 3
-    0x1531d871f1e5a534ccf73f362693fdb7#128, -- 2
-    0xc072a49cafa2d4adf04759fa7dc982ca#128, -- 1
-    0x76abd7fe2b670130c56f6bf27b777c63#128  -- 0
-  ]
-
-def AESShiftRows (op : BitVec 128) : BitVec 128 :=
-  extractLsb 95 88 op ++ extractLsb 55 48 op ++
-  extractLsb 15 8 op ++ extractLsb 103 96 op ++
-  extractLsb 63 56 op ++ extractLsb 23 16 op ++
-  extractLsb 111 104 op ++ extractLsb 71 64 op ++
-  extractLsb 31 24 op ++ extractLsb 119 112 op ++
-  extractLsb 79 72 op ++ extractLsb 39 32 op ++
-  extractLsb 127 120 op ++ extractLsb 87 80 op ++
-  extractLsb 47 40 op ++ extractLsb 7 0 op
-
-def AESSubBytes_aux (i : Nat) (op : BitVec 128) (out : BitVec 128)
-  : BitVec 128 :=
-  if h₀ : 16 <= i then
-    out
-  else
-    let idx := (extractLsb (i * 8 + 7) (i * 8) op).toNat
-    let val := extractLsb (idx * 8 + 7) (idx * 8) $ BitVec.flatten SBox
-    have h₁ : idx * 8 + 7 - idx * 8 = i * 8 + 7 - i * 8 := by omega
-    let out := BitVec.partInstall (i * 8 + 7) (i * 8) (h₁ ▸ val) out
-    have _ : 15 - i < 16 - i := by omega
-    AESSubBytes_aux (i + 1) op out
-  termination_by (16 - i)
-
-def AESSubBytes (op : BitVec 128) : BitVec 128 :=
-  AESSubBytes_aux 0 op (BitVec.zero 128)
-
 @[state_simp_rules]
 def exec_aese
   (inst : Crypto_aes_cls) (s : ArmState) : ArmState :=
@@ -69,7 +24,7 @@ def exec_aese
   let operand1 := read_sfp 128 inst.Rd s
   let operand2 := read_sfp 128 inst.Rn s
   let result := operand1 ^^^ operand2
-  let result := AESSubBytes $ AESShiftRows result
+  let result := AESCommon.SubBytes $ AESCommon.ShiftRows result
   -- State Updates
   let s := write_sfp 128 inst.Rd result s
   let s := write_pc ((read_pc s) + 4#64) s
@@ -97,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 :=
@@ -122,61 +76,10 @@ 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
-
-def AESMixColumns_aux (c : Nat)
-  (in0 : BitVec 32) (in1 : BitVec 32) (in2 : BitVec 32) (in3 : BitVec 32)
-  (out0 : BitVec 32) (out1 : BitVec 32) (out2 : BitVec 32) (out3 : BitVec 32)
-  : BitVec 32 × BitVec 32 × BitVec 32 × BitVec 32 :=
-  if h₀ : 4 <= c then
-    (out0, out1, out2, out3)
-  else
-    let lo := c * 8
-    let hi := lo + 7
-    have h₁ : hi - lo + 1 = 8 := by omega
-    let in0_byte := h₁ ▸ extractLsb hi lo in0
-    let in1_byte := h₁ ▸ extractLsb hi lo in1
-    let in2_byte := h₁ ▸ extractLsb hi lo in2
-    let in3_byte := h₁ ▸ extractLsb hi lo in3
-    let val0 := h₁.symm ▸ (FFmul02 in0_byte ^^^ FFmul03 in1_byte ^^^ in2_byte ^^^ in3_byte)
-    let out0 := BitVec.partInstall hi lo val0 out0
-    let val1 := h₁.symm ▸ (FFmul02 in1_byte ^^^ FFmul03 in2_byte ^^^ in3_byte ^^^ in0_byte)
-    let out1 := BitVec.partInstall hi lo val1 out1
-    let val2 := h₁.symm ▸ (FFmul02 in2_byte ^^^ FFmul03 in3_byte ^^^ in0_byte ^^^ in1_byte)
-    let out2 := BitVec.partInstall hi lo val2 out2
-    let val3 := h₁.symm ▸ (FFmul02 in3_byte ^^^ FFmul03 in0_byte ^^^ in1_byte ^^^ in2_byte)
-    let out3 := BitVec.partInstall hi lo val3 out3
-    have _ : 3 - c < 4 - c := by omega
-    AESMixColumns_aux (c + 1) in0 in1 in2 in3 out0 out1 out2 out3
-  termination_by (4 - c)
+  BitVec.cast (by omega) $ extractLsb hi lo $ BitVec.flatten FFmul_03
 
 def AESMixColumns (op : BitVec 128) : BitVec 128 :=
-  let in0 :=
-    extractLsb 103 96 op ++ extractLsb 71 64 op ++
-    extractLsb 39 32 op ++ extractLsb 7 0 op
-  let in1 :=
-    extractLsb 111 104 op ++ extractLsb 79 72 op ++
-    extractLsb 47 40 op ++ extractLsb 15 8 op
-  let in2 :=
-    extractLsb 119 112 op ++ extractLsb 87 80 op ++
-    extractLsb 55 48 op ++ extractLsb 23 16 op
-  let in3 :=
-    extractLsb 127 120 op ++ extractLsb 95 88 op ++
-    extractLsb 63 56 op ++ extractLsb 31 24 op
-  let (out0, out1, out2, out3) :=
-    (BitVec.zero 32, BitVec.zero 32,
-     BitVec.zero 32, BitVec.zero 32)
-  let (out0, out1, out2, out3) :=
-    AESMixColumns_aux 0 in0 in1 in2 in3 out0 out1 out2 out3
-  extractLsb 31 24 out3 ++ extractLsb 31 24 out2 ++
-  extractLsb 31 24 out1 ++ extractLsb 31 24 out0 ++
-  extractLsb 23 16 out3 ++ extractLsb 23 16 out2 ++
-  extractLsb 23 16 out1 ++ extractLsb 23 16 out0 ++
-  extractLsb 15 8 out3 ++ extractLsb 15 8 out2 ++
-  extractLsb 15 8 out1 ++ extractLsb 15 8 out0 ++
-  extractLsb 7 0 out3 ++ extractLsb 7 0 out2 ++
-  extractLsb 7 0 out1 ++ extractLsb 7 0 out0
+  AESCommon.MixColumns op FFmul02 FFmul03
 
 @[state_simp_rules]
 def exec_aesmc
diff --git a/Specs/AESArm.lean b/Specs/AESArm.lean
new file mode 100644
index 00000000..13bede96
--- /dev/null
+++ b/Specs/AESArm.lean
@@ -0,0 +1,241 @@
+/-
+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.DPSFP.Crypto_aes
+import Specs.AESCommon
+
+-- References : https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.197-upd1.pdf
+--              https://csrc.nist.gov/csrc/media/projects/cryptographic-standards-and-guidelines/documents/aes-development/rijndael-ammended.pdf
+--
+--------------------------------------------------
+-- The NIST specification has the following rounds:
+--
+-- AddRoundKey key0
+-- for k in key1 to key9
+--   SubBytes
+--   ShiftRows
+--   MixColumns
+--   AddRoundKey
+-- SubBytes
+-- ShiftRows
+-- AddRoundKey key10
+--
+-- The Arm implementation has an optimization that commute intermediate steps:
+--
+-- for k in key0 to key8
+--   AddRoundKey + ShiftRows + SubBytes (AESE k)
+--   MixColumns (AESMC)
+-- AddRoundKey + ShiftRows + SubBytes (AESE key9)
+-- AddRoundKey key10
+--
+-- Note: SubBytes and ShiftRows are commutative because
+--       SubBytes is a byte-wise operation
+--
+--------------------------------------------------
+
+namespace AESArm
+
+open BitVec
+
+def WordSize := 32
+def BlockSize := 128
+
+-- 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,
+  0x00000004#32,
+  0x00000008#32,
+  0x00000010#32,
+  0x00000020#32,
+  0x00000040#32,
+  0x00000080#32,
+  0x0000001b#32,
+  0x00000036#32 ]
+
+-------------------------------------------------------
+-- types
+
+-- Key-Block-Round Combinations
+structure KBR where
+  key_len : Nat
+  block_size : Nat
+  Nk := key_len / 32
+  Nb := block_size / 32
+  Nr : Nat
+  h : block_size = BlockSize
+deriving DecidableEq, Repr
+
+def AES128KBR : KBR :=
+  {key_len := 128, block_size := BlockSize, Nr := 10, h := by decide}
+def AES192KBR : KBR :=
+  {key_len := 192, block_size := BlockSize, Nr := 12, h := by decide}
+def AES256KBR : KBR :=
+  {key_len := 256, block_size := BlockSize, Nr := 14, h := by decide}
+
+def KeySchedule : Type := List (BitVec WordSize)
+
+-- Declare KeySchedule to be an instance HAppend
+-- so we can apply `++` to KeySchedules propertly
+instance : HAppend KeySchedule KeySchedule KeySchedule where
+  hAppend := List.append
+
+-------------------------------------------------------
+
+def sbox (ind : BitVec 8) : BitVec 8 :=
+  match_bv ind with
+  | [x:4, y:4] =>
+    have h : (x.toNat * 128 + y.toNat * 8 + 7) - (x.toNat * 128 + y.toNat * 8) + 1 = 8 :=
+      by omega
+    h ▸ extractLsb
+      (x.toNat * 128 + y.toNat * 8 + 7)
+      (x.toNat * 128 + y.toNat * 8) $ BitVec.flatten AESCommon.SBOX
+  | _ => ind -- unreachable case
+
+-- 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
+  | _ => w -- unreachable case
+
+def SubWord (w : BitVec WordSize) : BitVec WordSize :=
+  match_bv w with
+  | [a3:8, a2:8, a1:8, a0:8] => (sbox a3) ++ (sbox a2) ++ (sbox a1) ++ (sbox a0)
+  | _ => w -- unreachable case
+
+protected def InitKey {Param : KBR} (i : Nat) (key : BitVec Param.key_len)
+  (acc : KeySchedule) : KeySchedule :=
+  if h₀ : Param.Nk ≤ i then acc
+  else
+    have h₁ : i * 32 + 32 - 1 - i * 32 + 1 = WordSize := by
+      simp only [WordSize]; omega
+    let wd := h₁ ▸ extractLsb (i * 32 + 32 - 1) (i * 32) key
+    let (x:KeySchedule) := [wd]
+    have _ : Param.Nk - (i + 1) < Param.Nk - i := by omega
+    AESArm.InitKey (Param := Param) (i + 1) key (acc ++ x)
+  termination_by (Param.Nk - i)
+
+protected def KeyExpansion_helper {Param : KBR} (i : Nat) (ks : KeySchedule)
+  : KeySchedule :=
+  if h : 4 * Param.Nr + 4 ≤ i then
+    ks
+  else
+    let tmp := List.get! ks (i - 1)
+    let tmp :=
+      if i % Param.Nk == 0 then
+        (SubWord (RotWord tmp)) ^^^ (List.get! Rcon $ (i / Param.Nk) - 1)
+      else if Param.Nk > 6 && i % Param.Nk == 4 then
+        SubWord tmp
+      else
+        tmp
+    let res := (List.get! ks (i - Param.Nk)) ^^^ tmp
+    let ks := List.append ks [ res ]
+    have _ : 4 * Param.Nr + 4 - (i + 1) < 4 * Param.Nr + 4 - i := by omega
+    AESArm.KeyExpansion_helper (Param := Param) (i + 1) ks
+  termination_by (4 * Param.Nr + 4 - i)
+
+def KeyExpansion {Param : KBR} (key : BitVec Param.key_len)
+  : KeySchedule :=
+  let seeded := AESArm.InitKey (Param := Param) 0 key []
+  AESArm.KeyExpansion_helper (Param := Param) Param.Nk seeded
+
+def SubBytes {Param : KBR} (state : BitVec Param.block_size)
+  : BitVec Param.block_size :=
+  have h : Param.block_size = 128 := by simp only [Param.h, BlockSize]
+  h ▸ AESCommon.SubBytes (h ▸ state)
+
+def ShiftRows {Param : KBR} (state : BitVec Param.block_size)
+  : BitVec Param.block_size :=
+  have h : Param.block_size = 128 := by simp only [Param.h, BlockSize]
+  h ▸ AESCommon.ShiftRows (h ▸ state)
+
+def XTimes (bv : BitVec 8) : BitVec 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 :=
+  have h : Param.block_size = 128 := by simp only [Param.h, BlockSize]
+  let FFmul02 := fun (x : BitVec 8) => XTimes x
+  let FFmul03 := fun (x : BitVec 8) => x ^^^ XTimes x
+  h ▸ AESCommon.MixColumns (h ▸ state) FFmul02 FFmul03
+
+-- Convert bitvector quantification into bounded natural number quantification
+theorem P_of_bv_to_of_nat {n : Nat} {P : BitVec n -> Prop}:
+  (∀(x : Nat), x < 2^n → P (BitVec.ofNat n x)) →
+  ∀(p : BitVec n), P p := by
+  intro H p
+  let x := p.toNat
+  have p_eq : p = x#n := by simp only [x, BitVec.ofNat_toNat, truncate_eq]
+  simp only [p_eq]
+  apply H
+  apply BitVec.isLt
+
+set_option maxRecDepth 1000 in
+protected theorem FFmul02_equiv : (fun x => XTimes x) = DPSFP.FFmul02 := by
+  funext x
+  let P := fun (x : BitVec 8) => XTimes x = DPSFP.FFmul02 x
+  apply @P_of_bv_to_of_nat 8 P
+  simp only [P]
+  decide
+
+set_option maxRecDepth 1000 in
+protected theorem FFmul03_equiv : (fun x => x ^^^ XTimes x) = DPSFP.FFmul03 := by
+  funext x
+  let P := fun (x : BitVec 8) => x ^^^ XTimes x = DPSFP.FFmul03 x
+  apply @P_of_bv_to_of_nat 8 P
+  simp only [P]
+  decide
+
+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]
+    rw [AESArm.FFmul02_equiv, AESArm.FFmul03_equiv]
+
+def AddRoundKey {Param : KBR} (state : BitVec Param.block_size)
+  (roundKey : BitVec Param.block_size) : BitVec Param.block_size :=
+  state ^^^ roundKey
+
+protected def getKey {Param : KBR} (n : Nat) (w : KeySchedule) : BitVec Param.block_size :=
+  let ind := 4 * n
+  have h : WordSize + WordSize + WordSize + WordSize = Param.block_size := by
+    simp only [WordSize, BlockSize, Param.h]
+  h ▸ ((List.get! w (ind + 3)) ++ (List.get! w (ind + 2)) ++
+       (List.get! w (ind + 1)) ++ (List.get! w ind))
+
+protected def AES_encrypt_with_ks_loop {Param : KBR} (round : Nat)
+  (state : BitVec Param.block_size) (w : KeySchedule)
+  : BitVec Param.block_size :=
+  if Param.Nr ≤ round then
+    state
+  else
+    let state := SubBytes state
+    let state := ShiftRows state
+    let state := MixColumns state
+    let state := AddRoundKey state $ AESArm.getKey round w
+    AESArm.AES_encrypt_with_ks_loop (Param := Param) (round + 1) state w
+  termination_by (Param.Nr - round)
+
+def AES_encrypt_with_ks {Param : KBR} (input : BitVec Param.block_size)
+  (w : KeySchedule) : BitVec Param.block_size :=
+  have h₀ : WordSize + WordSize + WordSize + WordSize = Param.block_size := by
+    simp only [WordSize, BlockSize, Param.h]
+  let state := AddRoundKey input $ (h₀ ▸ AESArm.getKey 0 w)
+  let state := AESArm.AES_encrypt_with_ks_loop (Param := Param) 1 state w
+  let state := SubBytes (Param := Param) state
+  let state := ShiftRows (Param := Param) state
+  AddRoundKey state $ h₀ ▸ AESArm.getKey Param.Nr w
+
+def AES_encrypt {Param : KBR} (input : BitVec Param.block_size)
+  (key : BitVec Param.key_len) : BitVec Param.block_size :=
+  let ks := KeyExpansion (Param := Param) key
+  AES_encrypt_with_ks (Param := Param) input ks
+
+end AESArm
diff --git a/Specs/AESCommon.lean b/Specs/AESCommon.lean
index dbfb20be..5d2f8c58 100644
--- a/Specs/AESCommon.lean
+++ b/Specs/AESCommon.lean
@@ -1,64 +1,116 @@
 /-
 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
 
-namespace aes_helpers
+namespace AESCommon
 
 open BitVec
 
-def aes_shift_rows (op : BitVec 128) : BitVec 128 :=
-  let op_7_0     := extractLsb 7 0 op
-  let op_47_40   := extractLsb 47 40 op
-  let op_87_80   := extractLsb 87 80 op
-  let op_127_120 := extractLsb 127 120 op
-  let op_39_32   := extractLsb 39 32 op
-  let op_79_72   := extractLsb 79 72 op
-  let op_119_112 := extractLsb 119 112 op
-  let op_31_24   := extractLsb 31 24 op
-  let op_71_64   := extractLsb 71 64 op
-  let op_111_104 := extractLsb 111 104 op
-  let op_23_16   := extractLsb 23 16 op
-  let op_63_56   := extractLsb 63 56 op
-  let op_103_96  := extractLsb 103 96 op
-  let op_15_8    := extractLsb 15 8 op
-  let op_55_48   := extractLsb 55 48 op
-  let op_95_88   := extractLsb 95 88 op
-  (op_95_88 ++ op_55_48 ++ op_15_8 ++ op_103_96 ++ op_63_56 ++
-  op_23_16 ++ op_111_104 ++ op_71_64 ++ op_31_24 ++ op_119_112 ++
-  op_79_72 ++ op_39_32 ++ op_127_120 ++ op_87_80 ++ op_47_40 ++
-  op_7_0)
+-------------------------------------------------------
+-- Constants
 
--- S-box values
-def gf2_list : List (BitVec 128) :=
-        [
-        0x16bb54b00f2d99416842e6bf0d89a18c#128, -- <127:0>
-        0xdf2855cee9871e9b948ed9691198f8e1#128, -- <127:0>
-        0x9e1dc186b95735610ef6034866b53e70#128, -- <127:0>
-        0x8a8bbd4b1f74dde8c6b4a61c2e2578ba#128, -- <127:0>
-        0x08ae7a65eaf4566ca94ed58d6d37c8e7#128, -- <127:0>
-        0x79e4959162acd3c25c2406490a3a32e0#128, -- <127:0>
-        0xdb0b5ede14b8ee4688902a22dc4f8160#128, -- <127:0>
-        0x73195d643d7ea7c41744975fec130ccd#128, -- <127:0>
-        0xd2f3ff1021dab6bcf5389d928f40a351#128, -- <127:0>
-        0xa89f3c507f02f94585334d43fbaaefd0#128, -- <127:0>
-        0xcf584c4a39becb6a5bb1fc20ed00d153#128, -- <127:0>
-        0x842fe329b3d63b52a05a6e1b1a2c8309#128, -- <127:0>
-        0x75b227ebe28012079a059618c323c704#128, -- <127:0>
-        0x1531d871f1e5a534ccf73f362693fdb7#128, -- <127:0>
-        0xc072a49cafa2d4adf04759fa7dc982ca#128, -- <127:0>
-        0x76abd7fe2b670130c56f6bf27b777c63#128  -- <127:0>
-        ]
+def SBOX :=
+  --   F E D C B A 9 8 7 6 5 4 3 2 1 0
+  [ 0x16bb54b00f2d99416842e6bf0d89a18c#128, -- F
+    0xdf2855cee9871e9b948ed9691198f8e1#128, -- E
+    0x9e1dc186b95735610ef6034866b53e70#128, -- D
+    0x8a8bbd4b1f74dde8c6b4a61c2e2578ba#128, -- C
+    0x08ae7a65eaf4566ca94ed58d6d37c8e7#128, -- B
+    0x79e4959162acd3c25c2406490a3a32e0#128, -- A
+    0xdb0b5ede14b8ee4688902a22dc4f8160#128, -- 9
+    0x73195d643d7ea7c41744975fec130ccd#128, -- 8
+    0xd2f3ff1021dab6bcf5389d928f40a351#128, -- 7
+    0xa89f3c507f02f94585334d43fbaaefd0#128, -- 6
+    0xcf584c4a39becb6a5bb1fc20ed00d153#128, -- 5
+    0x842fe329b3d63b52a05a6e1b1a2c8309#128, -- 4
+    0x75b227ebe28012079a059618c323c704#128, -- 3
+    0x1531d871f1e5a534ccf73f362693fdb7#128, -- 2
+    0xc072a49cafa2d4adf04759fa7dc982ca#128, -- 1
+    0x76abd7fe2b670130c56f6bf27b777c63#128  -- 0
+  ]
 
-def bitvec_list_concat (xs : List (BitVec n)) : BitVec (n * List.length xs) :=
-    match xs with
-    | [] => 0#0
-    | x :: rest =>
-      have h1: (n + n * List.length rest) = (n * List.length (x :: rest)) := by sorry
-      h1 ▸ (x ++ (bitvec_list_concat rest))
+def ShiftRows (op : BitVec 128) : BitVec 128 :=
+  extractLsb 95 88 op ++ extractLsb 55 48 op ++
+  extractLsb 15 8 op ++ extractLsb 103 96 op ++
+  extractLsb 63 56 op ++ extractLsb 23 16 op ++
+  extractLsb 111 104 op ++ extractLsb 71 64 op ++
+  extractLsb 31 24 op ++ extractLsb 119 112 op ++
+  extractLsb 79 72 op ++ extractLsb 39 32 op ++
+  extractLsb 127 120 op ++ extractLsb 87 80 op ++
+  extractLsb 47 40 op ++ extractLsb 7 0 op
 
-def gf2 : BitVec (128 * 16) := bitvec_list_concat gf2_list
+def SubBytes_aux (i : Nat) (op : BitVec 128) (out : BitVec 128)
+  : BitVec 128 :=
+  if h₀ : 16 <= i then
+    out
+  else
+    let idx := (extractLsb (i * 8 + 7) (i * 8) op).toNat
+    let val := extractLsb (idx * 8 + 7) (idx * 8) $ BitVec.flatten SBOX
+    have h₁ : idx * 8 + 7 - idx * 8 = i * 8 + 7 - i * 8 := by omega
+    let out := BitVec.partInstall (i * 8 + 7) (i * 8) (h₁ ▸ val) out
+    have _ : 15 - i < 16 - i := by omega
+    SubBytes_aux (i + 1) op out
+  termination_by (16 - i)
 
-end aes_helpers
+def SubBytes (op : BitVec 128) : BitVec 128 :=
+  SubBytes_aux 0 op (BitVec.zero 128)
+
+def MixColumns_aux (c : Nat)
+  (in0 : BitVec 32) (in1 : BitVec 32) (in2 : BitVec 32) (in3 : BitVec 32)
+  (out0 : BitVec 32) (out1 : BitVec 32) (out2 : BitVec 32) (out3 : BitVec 32)
+  (FFmul02 : BitVec 8 -> BitVec 8) (FFmul03 : BitVec 8 -> BitVec 8)
+  : BitVec 32 × BitVec 32 × BitVec 32 × BitVec 32 :=
+  if h₀ : 4 <= c then
+    (out0, out1, out2, out3)
+  else
+    let lo := c * 8
+    let hi := lo + 7
+    have h₁ : hi - lo + 1 = 8 := by omega
+    let in0_byte := h₁ ▸ extractLsb hi lo in0
+    let in1_byte := h₁ ▸ extractLsb hi lo in1
+    let in2_byte := h₁ ▸ extractLsb hi lo in2
+    let in3_byte := h₁ ▸ extractLsb hi lo in3
+    let val0 := h₁.symm ▸ (FFmul02 in0_byte ^^^ FFmul03 in1_byte ^^^ in2_byte ^^^ in3_byte)
+    let out0 := BitVec.partInstall hi lo val0 out0
+    let val1 := h₁.symm ▸ (FFmul02 in1_byte ^^^ FFmul03 in2_byte ^^^ in3_byte ^^^ in0_byte)
+    let out1 := BitVec.partInstall hi lo val1 out1
+    let val2 := h₁.symm ▸ (FFmul02 in2_byte ^^^ FFmul03 in3_byte ^^^ in0_byte ^^^ in1_byte)
+    let out2 := BitVec.partInstall hi lo val2 out2
+    let val3 := h₁.symm ▸ (FFmul02 in3_byte ^^^ FFmul03 in0_byte ^^^ in1_byte ^^^ in2_byte)
+    let out3 := BitVec.partInstall hi lo val3 out3
+    have _ : 3 - c < 4 - c := by omega
+    MixColumns_aux (c + 1) in0 in1 in2 in3 out0 out1 out2 out3 FFmul02 FFmul03
+  termination_by (4 - c)
+
+def MixColumns (op : BitVec 128) (FFmul02 : BitVec 8 -> BitVec 8)
+  (FFmul03 : BitVec 8 -> BitVec 8) : BitVec 128 :=
+  let in0 :=
+    extractLsb 103 96 op ++ extractLsb 71 64 op ++
+    extractLsb 39 32 op ++ extractLsb 7 0 op
+  let in1 :=
+    extractLsb 111 104 op ++ extractLsb 79 72 op ++
+    extractLsb 47 40 op ++ extractLsb 15 8 op
+  let in2 :=
+    extractLsb 119 112 op ++ extractLsb 87 80 op ++
+    extractLsb 55 48 op ++ extractLsb 23 16 op
+  let in3 :=
+    extractLsb 127 120 op ++ extractLsb 95 88 op ++
+    extractLsb 63 56 op ++ extractLsb 31 24 op
+  let (out0, out1, out2, out3) :=
+    (BitVec.zero 32, BitVec.zero 32,
+     BitVec.zero 32, BitVec.zero 32)
+  let (out0, out1, out2, out3) :=
+    MixColumns_aux 0 in0 in1 in2 in3 out0 out1 out2 out3 FFmul02 FFmul03
+  extractLsb 31 24 out3 ++ extractLsb 31 24 out2 ++
+  extractLsb 31 24 out1 ++ extractLsb 31 24 out0 ++
+  extractLsb 23 16 out3 ++ extractLsb 23 16 out2 ++
+  extractLsb 23 16 out1 ++ extractLsb 23 16 out0 ++
+  extractLsb 15 8 out3 ++ extractLsb 15 8 out2 ++
+  extractLsb 15 8 out1 ++ extractLsb 15 8 out0 ++
+  extractLsb 7 0 out3 ++ extractLsb 7 0 out2 ++
+  extractLsb 7 0 out1 ++ extractLsb 7 0 out0
+
+end AESCommon
diff --git a/Specs/GCM.lean b/Specs/GCM.lean
new file mode 100644
index 00000000..620845d4
--- /dev/null
+++ b/Specs/GCM.lean
@@ -0,0 +1,194 @@
+/-
+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
+
+/-- NIST Special Publication 800-38D, page 11-12.
+    This constant represents, up to x^127, the polynomial for defining GF(2^128)
+    -/
+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 := (n/128 - 1 - i) * 128
+    let hi := lo + 127
+    have h₀ : hi - lo + 1 = 128 := by omega
+    let Xi := extractLsb hi lo X
+    let res := Y ^^^ (h₀ ▸ Xi)
+    let Y := mul res H
+    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 := (n - i - 1) * 128
+    let hi := lo + 127
+    have h : hi - lo + 1 = 128 := by omega
+    let Xi := extractLsb hi lo X
+    let Yi := h ▸ Xi ^^^ CIPH ICB K
+    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_bits w) := by
+  simp only [GCM.ceiling_in_bits, GCM.ceiling_in_blocks]
+  omega
+
+/-- GCTR: encrypting/decrypting message x using Galois counter mode -/
+def GCTR (CIPH : Cipher (n := 128) (m := m))
+  (K : BitVec m) (ICB : BitVec 128) (X : BitVec v) : (BitVec v) :=
+  let n := GCM.ceiling_in_blocks v
+  let b := GCM.ceiling_in_bits v
+  let s := b - v
+  let h : v + s = b := by
+    simp only [s]
+    apply Nat.add_sub_cancel'
+          (by simp only [b]; apply GCM.bits_le_ceiling_in_bits)
+  let X' : BitVec b := h ▸ (shiftLeftZeroExtend X s)
+  let R := GCTR_aux CIPH 0 n K ICB X' $ BitVec.zero b
+  truncate v $ R >>> s
+
+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
+       let block := IV ++ (BitVec.zero (s + 64)) ++ (BitVec.ofNat 64 lv)
+       GHASH H block h₂
+
+protected theorem GCM_AE_DE_simplification1 (a : Nat) (v : Nat) (p : Nat) (u : Nat) :
+  a + v + p + u + 64 + 64 = 128 + (u + p) + (v + a) := by omega
+
+protected theorem GCM_AE_DE_simplification2
+  (y : Nat) (x : Nat) (h : y ≤ x):
+  (x - y) + y = x := by omega
+
+/-- GCM_AE : Galois Counter Mode Authenticated Encryption -/
+def GCM_AE (CIPH : Cipher (n := 128) (m := m))
+  (K : BitVec m) (t : Nat) (IV : BitVec lv) (P : BitVec p) (A : BitVec a)
+  : (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 := A ++ BitVec.zero v ++ C ++ BitVec.zero u
+               ++ (BitVec.ofNat 64 a) ++ (BitVec.ofNat 64 p)
+  have h : 128 ∣ a + v + p + u + 64 + 64 := by
+    rw [GCM.GCM_AE_DE_simplification1]
+    simp only [u, v]
+    rw [GCM.GCM_AE_DE_simplification2 p (GCM.ceiling_in_bits p)
+        (by apply GCM.bits_le_ceiling_in_bits)]
+    rw [GCM.GCM_AE_DE_simplification2 a (GCM.ceiling_in_bits a)
+        (by apply GCM.bits_le_ceiling_in_bits)]
+    simp only [GCM.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 (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 := A ++ BitVec.zero v ++ C ++ BitVec.zero u
+                 ++ (BitVec.ofNat 64 a) ++ (BitVec.ofNat 64 c)
+    have h : 128 ∣ a + v + c + u + 64 + 64 := by
+      rw [GCM.GCM_AE_DE_simplification1]
+      simp only [u, v]
+      rw [GCM.GCM_AE_DE_simplification2 c (GCM.ceiling_in_bits c)
+          (by apply GCM.bits_le_ceiling_in_bits)]
+      rw [GCM.GCM_AE_DE_simplification2 a (GCM.ceiling_in_bits a)
+          (by apply GCM.bits_le_ceiling_in_bits)]
+      simp only [GCM.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..57e638db 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».AESArm
+import «Specs».GCM
diff --git a/Tests/AESGCMSpecTest.lean b/Tests/AESGCMSpecTest.lean
new file mode 100644
index 00000000..8f17f107
--- /dev/null
+++ b/Tests/AESGCMSpecTest.lean
@@ -0,0 +1,257 @@
+/-
+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.AESArm
+import Specs.GCM
+
+-- Reference: https://csrc.nist.rip/groups/ST/toolkit/BCM/documents/proposedmodes/gcm/gcm-spec.pdf
+
+namespace AES256GCMSpecTest
+
+open BitVec
+
+-- Reversing bytes in inputs and output because AES uses little-endian
+def revCIPH (CIPH : BitVec n -> BitVec m -> BitVec n)
+  (h₀ : 8 ∣ n) (h₁ : 8 ∣ m) (p : BitVec n) (k : BitVec m) :=
+  (rev_elems n 8
+    (CIPH (rev_elems n 8 p h₀ (by decide)) (rev_elems m 8 k h₁ (by decide)))
+    h₀ (by decide))
+
+def CIPH_128' : GCM.Cipher (n := 128) (m := 128) :=
+  AESArm.AES_encrypt (Param := AESArm.AES128KBR)
+
+def CIPH_128 : GCM.Cipher (n := 128) (m := 128) :=
+  revCIPH CIPH_128' (by decide) (by decide)
+
+def GCM_AE_128 : BitVec 128 → (t : Nat) → BitVec lv → BitVec p → BitVec a
+  → (BitVec p) × (BitVec t) := GCM.GCM_AE CIPH_128
+
+def GCM_AD_128 : BitVec 128 → BitVec lv → BitVec c → BitVec a → BitVec t
+  → Option (BitVec c) := GCM.GCM_AD CIPH_128
+
+def CIPH_192' : GCM.Cipher (n := 128) (m := 192) :=
+  AESArm.AES_encrypt (Param := AESArm.AES192KBR)
+
+def CIPH_192 : GCM.Cipher (n := 128) (m := 192) :=
+  revCIPH CIPH_192' (by decide) (by decide)
+
+def GCM_AE_192 : BitVec 192 → (t : Nat) → BitVec lv → BitVec p → BitVec a
+  → (BitVec p) × (BitVec t) := GCM.GCM_AE CIPH_192
+
+def GCM_AD_192 : BitVec 192 → BitVec lv → BitVec c → BitVec a → BitVec t
+  → Option (BitVec c) := GCM.GCM_AD CIPH_192
+
+def CIPH_256' : GCM.Cipher (n := 128) (m := 256) :=
+  AESArm.AES_encrypt (Param := AESArm.AES256KBR)
+
+def CIPH_256 : GCM.Cipher (n := 128) (m := 256) :=
+  revCIPH CIPH_256' (by decide) (by decide)
+
+def GCM_AE_256 : BitVec 256 → (t : Nat) → BitVec lv → BitVec p → BitVec a
+  → (BitVec p) × (BitVec t) := GCM.GCM_AE CIPH_256
+
+def GCM_AD_256 : BitVec 256 → BitVec lv → BitVec c → BitVec a → BitVec t
+  → Option (BitVec c) := GCM.GCM_AD 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 := 0x58e2fccefa7e3061367f1d57a4e7455a#128
+example : GCM_AE_128 K0 128 IV0 P0 A0 = (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 := 0x0388dace60b6a392f328c2b971b2fe78#128
+def T1 : BitVec 128 := 0xab6e47d42cec13bdf53a67b21257bddf#128
+example : GCM_AE_128 K1 128 IV1 P1 A1 = (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 := 0xfeffe9928665731c6d6a8f9467308308#128
+def IV2 : BitVec 96 := 0xcafebabefacedbaddecaf888#96
+def P2 : BitVec 512 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255#512
+def A2 : BitVec 0 := BitVec.nil
+def C2 : BitVec 512 := 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091473f5985#512
+def T2 : BitVec 128 := 0x4d5c2af327cd64a62cf35abd2ba6fab4#128
+example : GCM_AE_128 K2 128 IV2 P2 A2 = (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 := 0xfeffe9928665731c6d6a8f9467308308#128
+def IV3 : BitVec 96 := 0xcafebabefacedbaddecaf888#96
+def P3 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480
+def A3 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160
+def C3 : BitVec 480 := 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091#480
+def T3 : BitVec 128 := 0x5bc94fbc3221a5db94fae95ae7121a47#128
+example : GCM_AE_128 K3 128 IV3 P3 A3 = (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 := 0xfeffe9928665731c6d6a8f9467308308#128
+def IV4 : BitVec 64 := 0xcafebabefacedbad#64
+def P4 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480
+def A4 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160
+def C4 : BitVec 480 := 0x61353b4c2806934a777ff51fa22a4755699b2a714fcdc6f83766e5f97b6c742373806900e49f24b22b097544d4896b424989b5e1ebac0f07c23f4598#480
+def T4 : BitVec 128 := 0x3612d2e79e3b0785561be14aaca2fccb#128
+example : GCM_AE_128 K4 128 IV4 P4 A4 = (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 := 0xfeffe9928665731c6d6a8f9467308308#128
+def IV5 : BitVec 480 := 0x9313225df88406e555909c5aff5269aa6a7a9538534f7da1e4c303d2a318a728c3c0c95156809539fcf0e2429a6b525416aedbf5a0de6a57a637b39b#480
+def P5 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480
+def A5 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160
+def C5 : BitVec 480 := 0x8ce24998625615b603a033aca13fb894be9112a5c3a211a8ba262a3cca7e2ca701e4a9a4fba43c90ccdcb281d48c7c6fd62875d2aca417034c34aee5#480
+def T5 : BitVec 128 := 0x619cc5aefffe0bfa462af43c1699d050#128
+example : GCM_AE_128 K5 128 IV5 P5 A5 = (C5, T5) := by native_decide
+example : GCM_AD_128 K5 IV5 C5 A5 T5 = P5 := by native_decide
+
+-- Test Vector 6
+
+def K6 : BitVec 192 := 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 := 0xcd33b28ac773f74ba00ed1f312572435#128
+example : GCM_AE_192 K6 128 IV6 P6 A6 = (C6, T6) := by native_decide
+example : GCM_AD_192 K6 IV6 C6 A6 T6 = P6 := by native_decide
+
+-- Test Vector 7
+
+def K7 : BitVec 192 := 0
+def IV7 : BitVec 96 := 0
+def P7 : BitVec 128 := 0
+def A7 : BitVec 0 := BitVec.nil
+def C7 : BitVec 128 := 0x98e7247c07f0fe411c267e4384b0f600#128
+def T7 : BitVec 128 := 0x2ff58d80033927ab8ef4d4587514f0fb#128
+example : GCM_AE_192 K7 128 IV7 P7 A7 = (C7, T7) := by native_decide
+example : GCM_AD_192 K7 IV7 C7 A7 T7 = P7 := by native_decide
+
+-- Test Vector 8
+
+def K8 : BitVec 192 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192
+def IV8 : BitVec 96 := 0xcafebabefacedbaddecaf888#96
+def P8 : BitVec 512 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255#512
+def A8 : BitVec 0 := BitVec.nil
+def C8 : BitVec 512 := 0x3980ca0b3c00e841eb06fac4872a2757859e1ceaa6efd984628593b40ca1e19c7d773d00c144c525ac619d18c84a3f4718e2448b2fe324d9ccda2710acade256#512
+def T8 : BitVec 128 := 0x9924a7c8587336bfb118024db8674a14#128
+example : GCM_AE_192 K8 128 IV8 P8 A8 = (C8, T8) := by native_decide
+example : GCM_AD_192 K8 IV8 C8 A8 T8 = P8 := by native_decide
+
+-- Test Vector 9
+
+def K9 : BitVec 192 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192
+def IV9 : BitVec 96 := 0xcafebabefacedbaddecaf888#96
+def P9 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480
+def A9 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160
+def C9 : BitVec 480 := 0x3980ca0b3c00e841eb06fac4872a2757859e1ceaa6efd984628593b40ca1e19c7d773d00c144c525ac619d18c84a3f4718e2448b2fe324d9ccda2710#480
+def T9 : BitVec 128 := 0x2519498e80f1478f37ba55bd6d27618c#128
+example : GCM_AE_192 K9 128 IV9 P9 A9 = (C9, T9) := by native_decide
+example : GCM_AD_192 K9 IV9 C9 A9 T9 = P9 := by native_decide
+
+-- Test Vector 10
+
+def K10 : BitVec 192 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192
+def IV10 : BitVec 64:= 0xcafebabefacedbad#64
+def P10 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480
+def A10 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160
+def C10 : BitVec 480 := 0x0f10f599ae14a154ed24b36e25324db8c566632ef2bbb34f8347280fc4507057fddc29df9a471f75c66541d4d4dad1c9e93a19a58e8b473fa0f062f7#480
+def T10 : BitVec 128 := 0x65dcc57fcf623a24094fcca40d3533f8#128
+example : GCM_AE_192 K10 128 IV10 P10 A10 = (C10, T10) := by native_decide
+example : GCM_AD_192 K10 IV10 C10 A10 T10 = P10 := by native_decide
+
+-- Test Vector 11
+
+def K11 : BitVec 192 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192
+def IV11 : BitVec 480 := 0x9313225df88406e555909c5aff5269aa6a7a9538534f7da1e4c303d2a318a728c3c0c95156809539fcf0e2429a6b525416aedbf5a0de6a57a637b39b#480
+def P11 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480
+def A11 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160
+def C11 : BitVec 480 := 0xd27e88681ce3243c4830165a8fdcf9ff1de9a1d8e6b447ef6ef7b79828666e4581e79012af34ddd9e2f037589b292db3e67c036745fa22e7e9b7373b#480
+def T11 : BitVec 128 := 0xdcf566ff291c25bbb8568fc3d376a6d9#128
+example : GCM_AE_192 K11 128 IV11 P11 A11 = (C11, T11) := by native_decide
+example : GCM_AD_192 K11 IV11 C11 A11 T11 = P11 := by native_decide
+
+-- Test Vector 12
+
+def K12 : BitVec 256 := 0
+def IV12 : BitVec 96 := 0
+def P12 : BitVec 0 := BitVec.nil
+def A12 : BitVec 0 := BitVec.nil
+def C12 : BitVec 0 := BitVec.nil
+def T12 : BitVec 128 := 0x530f8afbc74536b9a963b4f1c4cb738b#128
+example : GCM_AE_256 K12 128 IV12 P12 A12 = (C12, T12) := by native_decide
+example : GCM_AD_256 K12 IV12 C12 A12 T12 = P12 := by native_decide
+
+-- Test Vector 13
+
+def K13 : BitVec 256 := 0
+def IV13 : BitVec 96 := 0
+def P13 : BitVec 128 := 0
+def A13 : BitVec 0 := BitVec.nil
+def C13 : BitVec 128 := 0xcea7403d4d606b6e074ec5d3baf39d18#128
+def T13 : BitVec 128 := 0xd0d1c8a799996bf0265b98b5d48ab919#128
+example : GCM_AE_256 K13 128 IV13 P13 A13 = (C13, T13) := by native_decide
+example : GCM_AD_256 K13 IV13 C13 A13 T13 = P13 := by native_decide
+
+-- Test Vector 14
+
+def K14 : BitVec 256 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256
+def IV14 : BitVec 96 := 0xcafebabefacedbaddecaf888#96
+def P14 : BitVec 512 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255#512
+def A14 : BitVec 0 := BitVec.nil
+def C14 : BitVec 512 := 0x522dc1f099567d07f47f37a32a84427d643a8cdcbfe5c0c97598a2bd2555d1aa8cb08e48590dbb3da7b08b1056828838c5f61e6393ba7a0abcc9f662898015ad#512
+def T14 : BitVec 128 := 0xb094dac5d93471bdec1a502270e3cc6c#128
+example : GCM_AE_256 K14 128 IV14 P14 A14 = (C14, T14) := by native_decide
+example : GCM_AD_256 K14 IV14 C14 A14 T14 = P14 := by native_decide
+
+-- Test Vector 15
+
+def K15 : BitVec 256 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256
+def IV15 : BitVec 96 := 0xcafebabefacedbaddecaf888#96
+def P15 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480
+def A15 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160
+def C15 : BitVec 480 := 0x522dc1f099567d07f47f37a32a84427d643a8cdcbfe5c0c97598a2bd2555d1aa8cb08e48590dbb3da7b08b1056828838c5f61e6393ba7a0abcc9f662#480
+def T15 : BitVec 128 := 0x76fc6ece0f4e1768cddf8853bb2d551b#128
+example : GCM_AE_256 K15 128 IV15 P15 A15 = (C15, T15) := by native_decide
+example : GCM_AD_256 K15 IV15 C15 A15 T15 = P15 := by native_decide
+
+-- Test Vector 16
+
+def K16 : BitVec 256 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256
+def IV16 : BitVec 64:= 0xcafebabefacedbad#64
+def P16 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480
+def A16 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160
+def C16 : BitVec 480 := 0xc3762df1ca787d32ae47c13bf19844cbaf1ae14d0b976afac52ff7d79bba9de0feb582d33934a4f0954cc2363bc73f7862ac430e64abe499f47c9b1f#480
+def T16 : BitVec 128 := 0x3a337dbf46a792c45e454913fe2ea8f2#128
+example : GCM_AE_256 K16 128 IV16 P16 A16 = (C16, T16) := by native_decide
+example : GCM_AD_256 K16 IV16 C16 A16 T16 = P16 := by native_decide
+
+-- Test Vector 17
+
+def K17 : BitVec 256 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256
+def IV17 : BitVec 480 := 0x9313225df88406e555909c5aff5269aa6a7a9538534f7da1e4c303d2a318a728c3c0c95156809539fcf0e2429a6b525416aedbf5a0de6a57a637b39b#480
+def P17 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480
+def A17 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160
+def C17 : BitVec 480 := 0x5a8def2f0c9e53f1f75d7853659e2a20eeb2b22aafde6419a058ab4f6f746bf40fc0c3b780f244452da3ebf1c5d82cdea2418997200ef82e44ae7e3f#480
+def T17 : BitVec 128 := 0xa44a8266ee1c8eb0c8b5d4cf5ae9f19a#128
+example : GCM_AE_256 K17 128 IV17 P17 A17 = (C17, T17) := by native_decide
+example : GCM_AD_256 K17 IV17 C17 A17 T17 = P17 := by native_decide
+
+end AES256GCMSpecTest
diff --git a/Tests/AESSpecTest.lean b/Tests/AESSpecTest.lean
new file mode 100644
index 00000000..7564955b
--- /dev/null
+++ b/Tests/AESSpecTest.lean
@@ -0,0 +1,42 @@
+/-
+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 Specs.AESArm
+import Arm.BitVec
+
+-- Reference : https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.197-upd1.pdf Section B
+
+-- Testing AES-128 encryption of one message block
+
+namespace AESSpecTest
+
+open BitVec
+
+-- The specification expects little-endian input
+protected def input : BitVec 128 :=
+  BitVec.flatten
+    [ 0x32#8, 0x43#8, 0xf6#8, 0xa8#8,
+      0x88#8, 0x5a#8, 0x30#8, 0x8d#8,
+      0x31#8, 0x31#8, 0x98#8, 0xa2#8,
+      0xe0#8, 0x37#8, 0x07#8, 0x34#8 ].reverse
+
+protected def key : BitVec 128 :=
+  BitVec.flatten
+    [ 0x2b#8, 0x7e#8, 0x15#8, 0x16#8,
+      0x28#8, 0xae#8, 0xd2#8, 0xa6#8,
+      0xab#8, 0xf7#8, 0x15#8, 0x88#8,
+      0x09#8, 0xcf#8, 0x4f#8, 0x3c#8 ].reverse
+
+protected def output : BitVec 128 :=
+  BitVec.flatten
+    [ 0x39#8, 0x25#8, 0x84#8, 0x1d#8,
+      0x02#8, 0xdc#8, 0x09#8, 0xfb#8,
+      0xdc#8, 0x11#8, 0x85#8, 0x97#8,
+      0x19#8, 0x6a#8, 0x0b#8, 0x32#8 ].reverse
+
+example : AESArm.AES_encrypt (Param := AESArm.AES128KBR) AESSpecTest.input AESSpecTest.key = AESSpecTest.output := by native_decide
+
+end AESSpecTest
diff --git a/Tests/Tests.lean b/Tests/Tests.lean
index a1ae7724..723c8577 100644
--- a/Tests/Tests.lean
+++ b/Tests/Tests.lean
@@ -9,4 +9,6 @@ import «Tests».SHA512SpecTest
 -- import «Tests».SHA512StandardSpecTest
 import «Tests».SHA512ProgramTest
 import «Tests».LDSTTest
+import «Tests».AESSpecTest
+import «Tests».AESGCMSpecTest