diff --git a/Primitive/Symmetric/Cipher/Authenticated/AES_GCM.cry b/Primitive/Symmetric/Cipher/Authenticated/AES_GCM.cry
index 61e9938e..3f762fa4 100644
--- a/Primitive/Symmetric/Cipher/Authenticated/AES_GCM.cry
+++ b/Primitive/Symmetric/Cipher/Authenticated/AES_GCM.cry
@@ -1,37 +1,101 @@
 
 // Cryptol AES GCM test vectors
-// Copyright (c) 2010-2018, Galois Inc.
+// Copyright (c) 2010-2024, Galois Inc.
 // www.cryptol.net
 // Author: Ajay Kumar Eeralla
 
-//Test vectors from http://luca-giuzzi.unibs.it/corsi/Support/papers-cryptography/gcm-spec.pdf
+// Test vectors from http://luca-giuzzi.unibs.it/corsi/Support/papers-cryptography/gcm-spec.pdf
 
 module Primitive::Symmetric::Cipher::Authenticated::AES_GCM where
 import `Primitive::Symmetric::Cipher::Authenticated::GCM
-import Primitive::Symmetric::Cipher::Block::AES_parameterized
+import Primitive::Symmetric::Cipher::Block::AES_parameterized as AES
 
+// GCM's symmetry property must hold for AES.
+// The other type parameter sizes are chosen arbitrarily.
+aesGcmIsSymmetric: [128] -> [96] -> [256] -> [0] -> Bool
+property aesGcmIsSymmetric key iv pt aad = gcmIsSymmetric `{T=128} { E=AES::encrypt } key iv pt aad
 
-property testPass0 = gcmEnc `{K=128, IV=96, AAD=0, T=128} {E=encrypt} {key=zero, iv=zero, pt=[], aad=[]} ==
-                              {ct = [], tag = 0x58e2fccefa7e3061367f1d57a4e7455a}
+// GCM's decryption API equivalence must hold for AES.
+// The other type parameter sizes are chosen arbitrarily.
+aesGcmDecryptionApisAreEquivalent: [128] -> [96] -> [256] -> [128] -> Bool
+property aesGcmDecryptionApisAreEquivalent key iv ct tag = decryptionApisAreEquivalent {E=AES::encrypt} key iv ct [] tag
 
-property testPass1 = gcmEnc `{K=128, IV=96, AAD=0, T=128} {E=encrypt} {key=zero, iv=zero, pt=zero, aad=[]} ==
-                              {ct = 0x0388dace60b6a392f328c2b971b2fe78, tag = 0xab6e47d42cec13bdf53a67b21257bddf}
+// GCM's encryption API equivalence must hold for AES.
+// The other type parameter sizes are chosen arbitrarily.
+aesGcmEncryptionApisAreEquivalent: [128] -> [96] -> [256] -> [128] -> Bool
+property aesGcmEncryptionApisAreEquivalent key iv pt = decryptionApisAreEquivalent {E=AES::encrypt} key iv pt []
 
-property testPass2 = gcmEnc `{K=128, IV=96, AAD=0, T=128} {E=encrypt} {key=0xfeffe9928665731c6d6a8f9467308308, iv=0xcafebabefacedbaddecaf888,         pt=0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255, aad=[]} ==
-    {ct = 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091473f5985,
-    tag = 0x4d5c2af327cd64a62cf35abd2ba6fab4}
+property AES_GCM_test_vector_0 = ct == expected_ct /\ tag == expected_tag /\ valid_dec
+    where
+        pt = []
+        (ct, tag) = GCM_AE `{K=128, IV=96, AAD=0, T=128} {E=AES::encrypt} zero zero pt []
+        dec = GCM_AD `{K=128, IV=96, AAD=0, T=128} {E=AES::encrypt} zero zero ct [] tag
+        expected_ct = []
+        expected_tag = 0x58e2fccefa7e3061367f1d57a4e7455a
+        valid_dec = dec.valid && (dec.pt == pt)
 
-property testPass3 = gcmEnc `{K=128, IV=96, AAD=160, T=128} {E=encrypt} {key=0xfeffe9928665731c6d6a8f9467308308,                                            iv=0xcafebabefacedbaddecaf888,
-    pt=0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39,
-    aad=0xfeedfacedeadbeeffeedfacedeadbeefabaddad2} ==
-    {ct=0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091,
-    tag=0x5bc94fbc3221a5db94fae95ae7121a47}
+property AES_GCM_test_vector_1 =
+    ct == expected_ct /\ tag == expected_tag /\ valid_dec
+    where
+        key = zero
+        iv = zero
+        pt = zero
+        aad = []
+        expected_ct = 0x0388dace60b6a392f328c2b971b2fe78
+        expected_tag = 0xab6e47d42cec13bdf53a67b21257bddf : [128]
+        (ct, tag) = GCM_AE `{K=128, IV=96} {E=AES::encrypt} key iv pt aad
+        dec = GCM_AD `{K=128, IV=96} {E=AES::encrypt} key iv ct aad tag
+        valid_dec = dec.valid && (dec.pt == pt)
 
-// A test case from aesgcmtest.c
-// Test passes
-property testPass4 = gcmEnc `{K=256, IV=96, AAD=128, T=128} {E=encrypt} {key=0xeebc1f57487f51921c0465665f8ae6d1658bb26de6f8a069a3520293a572078f,
-    iv=0x99aa3e68ed8173a0eed06684, pt=0xf56e87055bc32d0eeb31b2eacc2bf2a5, aad=0x4d23c3cec334b49bdb370c437fec78de} ==
-   {ct=0xf7264413a84c0e7cd536867eb9f21736, tag=0x67ba0510262ae487d737ee6298f77e0c}
+property AES_GCM_test_vector_2 =
+    ct == expected_ct /\ tag == expected_tag /\ valid_dec
+    where
+        key = 0xfeffe9928665731c6d6a8f9467308308 : [128]
+        iv = 0xcafebabefacedbaddecaf888 : [96]
+        pt = 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255
+        aad = []
+        expected_ct = 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091473f5985
+        expected_tag = 0x4d5c2af327cd64a62cf35abd2ba6fab4 : [128]
+        (ct, tag) = GCM_AE {E=AES::encrypt} key iv pt aad
+        dec = GCM_AD {E=AES::encrypt} key iv ct aad tag
+        valid_dec = dec.valid && (dec.pt == pt)
 
+property AES_GCM_test_vector_3 =
+    ct == expected_ct /\ tag == expected_tag /\ valid_dec
+    where
+        key = 0xfeffe9928665731c6d6a8f9467308308
+        pt  = 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39
+        iv  = 0xcafebabefacedbaddecaf888
+        aad = 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2
+        expected_ct  = 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091
+        expected_tag = 0x5bc94fbc3221a5db94fae95ae7121a47
+        (ct, tag) = GCM_AE {E=AES::encrypt} key iv pt aad
+        dec = GCM_AD {E=AES::encrypt} key iv ct aad tag
+        valid_dec = dec.valid && (dec.pt == pt)
 
+// A test case from aesgcmtest.c
+property AES_GCM_test_vector_4 =
+    ct == expected_ct /\ tag == expected_tag /\ valid_dec
+    where
+        key   = 0xeebc1f57487f51921c0465665f8ae6d1658bb26de6f8a069a3520293a572078f : [256]
+        iv    = 0x99aa3e68ed8173a0eed06684 : [96]
+        pt    = 0xf56e87055bc32d0eeb31b2eacc2bf2a5 : [128]
+        aad   = 0x4d23c3cec334b49bdb370c437fec78de : [128]
+        expected_ct   = 0xf7264413a84c0e7cd536867eb9f21736
+        expected_tag  = 0x67ba0510262ae487d737ee6298f77e0c
+        (ct, tag) = GCM_AE {E=AES::encrypt} key iv pt aad
+        dec = GCM_AD {E=AES::encrypt} key iv ct aad tag
+        valid_dec = dec.valid && (dec.pt == pt)
 
+property AES_GCM_invalid_test_vector =
+    ct == expected_ct /\ tag == expected_tag /\ ~dec.valid
+    where
+        key   = 0xeebc1f57487f51921c0465665f8ae6d1658bb26de6f8a069a3520293a572078f : [256]
+        iv    = 0x99aa3e68ed8173a0eed06684 : [96]
+        pt    = 0xf56e87055bc32d0eeb31b2eacc2bf2a5 : [128]
+        aad   = 0x4d23c3cec334b49bdb370c437fec78de : [128]
+        expected_ct   = 0xf7264413a84c0e7cd536867eb9f21736
+        expected_tag  = 0x67ba0510262ae487d737ee6298f77e0c
+        invalid_tag  = 0x67ba0510262ae487d737ee6298f77888
+        (ct, tag) = GCM_AE {E=AES::encrypt} key iv pt aad
+        dec = GCM_AD {E=AES::encrypt} key iv ct aad invalid_tag
\ No newline at end of file
diff --git a/Primitive/Symmetric/Cipher/Authenticated/GCM.cry b/Primitive/Symmetric/Cipher/Authenticated/GCM.cry
index b4393abc..0f6864af 100644
--- a/Primitive/Symmetric/Cipher/Authenticated/GCM.cry
+++ b/Primitive/Symmetric/Cipher/Authenticated/GCM.cry
@@ -1,10 +1,12 @@
 /*
 Galois Counter Mode in Cryptol
 Copyright (c) 2017-2018, Galois, Inc.
+Author: Sean Weaver, Marcella Hastings
 
-This implementation follows:
-"The Galois/Counter Mode of Operation (GCM)"
-paper by McGrew and Viega.
+This implementation follows NIST special publication 800-38D:
+[NISTSP800-38D] Morris Dworkin. Recommendation for Block Cipher Modes
+of Operation: Galois/Counter Mode (GCM) and GMAC. NIST Special
+Publication 800-38D. November 2007.
 */
 
 module Primitive::Symmetric::Cipher::Authenticated::GCM where
@@ -29,82 +31,204 @@ parameter
   /** Block encryption function */
   E : [K] -> [128] -> [128]
 
+/**
+ * GCM encryption function
+ *
+ * Maintaining this API for backwards compatability, but `GCM-AE` is recommended for
+ * more precise spec adherence.
+ */
 gcmEnc :
   {n} (2^^39 - 256 >= n) =>
       { key : [K], iv : [IV], aad : [AAD], pt : [n] } -> { ct : [n], tag : [T] }
 gcmEnc input = { ct = C, tag = T }
-  where (C,T) = enc_dec input.key input.iv input.aad input.pt
+  where (C,T) = GCM_AE input.key input.iv input.pt input.aad
+
+/**
+ * GCM-AE Function, [NISTSP800-38D] Section 7.1, Algorithm 4. This provides
+ * authenticated encryption.
+ */
+
+GCM_AE : { P } (fin P, P <= 2^^39 - 256 ) // This constraint comes from [NISTSP800-38D]
+ => [K] -> [IV] -> [P] -> [AAD] -> ([P], [T])
+GCM_AE k iv p a = (C, T)
+  where
+    // Set names to match the spec
+    CIPHk = E k
+    type len_A = AAD
+    // Ciphertext length is the same as the input plaintext length
+    type len_C = P
+
+    H = CIPHk 0
+    J0 = define_J0 k iv H
+    C = GCTR CIPHk (inc`{32} J0) p
+    type u = len_C %^ 128 // Equivalently: 128 * len_C /^ 128 - len_C
+    type v = len_A %^ 128 // Equivalently: 128 * len_A /^ 128 - len_A
+    S = GHASH`{len_A/^ 128 + P /^ 128 + 1}
+            H (a # (0 : [v]) # C # (0 : [u]) # (`len_A : [64]) # (`len_C : [64]))
+    T = MSB`{T} (GCTR CIPHk J0 S)
 
+/**
+ * GCM decryption function.
+ *
+ * Maintaining this API for backwards compatibility, but `GCM-AD` is recommended
+ * for more precise spec adherence.
+ */
 gcmDec :
   {n} (2^^39 - 256 >= n) =>
   { key : [K], iv  : [IV], aad : [AAD], ct  : [n], tag : [T] } ->
   { valid : Bool, pt : [n] }
-gcmDec input = if input.tag == T then { valid = True, pt = P }
-                                  else { valid = False, pt = 0 }
-  where (P,T) = enc_dec input.key input.iv input.aad input.ct
-
+gcmDec input = GCM_AD input.key input.iv input.ct input.aad input.tag
 
 
 /**
-The basic functionality between encryption and decryption.
-In the case of decryption, the plain text is only valid if the tags match.
-*/
-enc_dec :
-  {n} ((2^^39 - 256) >= n) => [K] -> [IV] -> [AAD] -> [n] -> ([n], [T])
-enc_dec K IV A P = (C,T)
-  where
-  H  = (E K 0)
-
-  Y0 = ifWidth`{96} IV (\IV96 -> IV96 # 1)
-                       (GHASH H [] IV)
-
-  Ys = [Y0] # [ y+1 | y <- Ys ]
-
-  Cs = [ p ^ (E K y) | p <- blockify P | y <- drop`{1} Ys ]
-  C  = unblockify Cs
-
-  T = take (GHASH H A C ^ (E K Y0))
-
-
-/** Section 2.3, equation (2) */
-GHASH : {C,A} (64 >= width C, 64 >= width A) => [128] -> [A] -> [C] -> [128]
-GHASH H A C = step (XS ! 0) (wa # wc)
+ * GCM-AD Function, [NISTSP800-38D] Section 7.2, Algorithm 5. This provides
+ * authenticated decryption.
+ */
+
+GCM_AD : { C }
+    ( fin C, C <= 2^^39 - 256 )  // This constraint comes from [NISTSP800-38D]
+ => [K] -> [IV] -> [C] -> [AAD] -> [T] -> { valid : Bool, pt : [C] }
+GCM_AD key iv ct aad tag =
+  if tag == T'
+  then { valid = True, pt = P }
+  else { valid = False, pt = 0 }
   where
-  wa = `A : [64]
-  wc = `C : [64]
+    CIPHk = E key
+    len_IV = `IV
+    type len_A = AAD
+    type len_C = C
+
+    H = CIPHk 0
+    J0 = define_J0 key iv H
+    P = GCTR CIPHk (inc`{32} J0) ct
+    type u = len_C %^ 128 // Equivalently: 128 * len_C /^ 128 - len_C
+    type v = len_A %^ 128 // Equivalently: 128 * len_A /^ 128 - len_A
+    S = GHASH`{len_A /^ 128 + len_C /^ 128 + 1}
+            H (aad # (0 : [v]) # ct # (0 : [u]) # (`len_A : [64]) # (`len_C : [64]))
+    T' = MSB`{T} (GCTR CIPHk J0 S)
 
-  XS = [0] # [ step X' B | X' <- XS | B <- blockify A # blockify C ]
-
-  step x b = mult (x ^ b) H
-
-
-
-/** Section 2.5, multiplication in GF(2^^128)
-
-This is simple polynomial multipliation and reduction in Cryptol.
-Somewhat oddly, when thinking of the 128-bits as polynomials,
-the spec treats the most significant bit as the 0 power,
-which is the reason for the `reverse` operations.
+/**
+* Property demonstrating equivalence between `mult` and `•`.
 */
-mult : [128] -> [128] -> [128]
-mult X Y = reverse (pmod (pmult (reverse X) (reverse Y)) irred)
-  where irred = <| 1 + x + x^^2 + x^^7 + x^^128 |>
-
 
-/** Create blocks as described in the spec, first paragraph of Section 2.3.
-Basically we split into 128-bit chunk and pad the last one with 0. */
-blockify : {n} (fin n) => [n] -> [n /^ 128][128]
-blockify msg = split (msg # 0)
-
-/** Join back the blocks, dropping any additional padding. */
-unblockify : {n} (fin n) => [n /^ 128][128] -> [n]
-unblockify ms = take (join ms)
-
-
-ifWidth : {w,n,a} (fin n, fin w) => [n] -> ([w] -> a) -> a -> a
-ifWidth thing yep nope = if `w == (`n : [max (width w) (width n)])
-                            then yep (take (thing # (zero : [inf])))
-                            else nope
+property dotAndMultAreEquivalent X Y = mult X Y == X • Y
 
+/**
+* Property demonstrating equivalence between `gcmDec` and `GCM_AD`.
+*/
+decryptionApisAreEquivalent : {P} ( fin P, P <= 2^^39 - 256 )
+  => [K] -> [IV] -> [P] -> [AAD] -> [T] -> Bool
+property decryptionApisAreEquivalent key iv ct aad tag =
+      gcmDec { key=key, iv=iv, ct=ct, aad=aad, tag=tag}
+      == GCM_AD key iv ct aad tag
 
+/**
+ * Property demonstrating equivalence between `gcmEnc` and `GCM_AE`.
+ */
+encryptionApisAreEquivalent : {P} ( fin P, P <= 2^^39 - 256 )
+  => [K] -> [IV] -> [P] -> [AAD] -> Bool
+property encryptionApisAreEquivalent key iv pt aad = gcm_ae_output == (gcmEnc_output.ct, gcmEnc_output.tag)
+    where
+      input = { key=key, iv=iv, pt=pt, aad=aad }
+      gcmEnc_output = gcmEnc input
+      gcm_ae_output = GCM_AE key iv pt aad
 
+/**
+ * Property demonstrating that decryption is the inverse of encryption.
+ *
+ * This should be instantiated for each block cipher `E` that uses GCM mode.
+ */
+gcmIsSymmetric : {P} ( fin P, P < 2^^39 - 256 )
+  => [K] -> [IV] -> [P] -> [AAD] -> Bool
+property gcmIsSymmetric key iv pt aad = dec.valid && (dec.pt == pt)
+    where
+        (ct, tag) = GCM_AE key iv pt aad
+        dec = GCM_AD key iv ct aad tag
+
+private
+  /**
+  * A helper function used in GCM_AE and GCM_AD. We must define this at the top
+  * level due to its use of Cryptol's numeric constraint guards feature, which
+  * currently only works in top-level definitions.
+  *
+  * This renames the IV type to `len_IV` to better match [NISTSP800-38D].
+  */
+  define_J0 : { len_IV } ( len_IV == IV) => [K] -> [len_IV] -> [128] -> [128]
+  define_J0 k iv H
+    | len_IV == 96 => iv # (0 : [31]) # (1 : [1])
+    | len_IV != 96 => GHASH`{len_IV /^ 128 + 1} H (iv # (0 : [s + 64]) # (`len_IV: [64]))
+    where
+      // Set names to match the spec
+      type s = len_IV %^ 128  // Equivalently: 128 * len_IV /^ 128 - len_IV
+
+  /**
+  * Multiplication Operation on Blocks, [NISTSP800-38D] Section
+  * 6.3, Algorithm 1. This is optimized to use Cryptol's built-in `pmult` and
+  * `pmod` functions. This operation is described using little-endian
+  * notation, hence the `reverse`s.
+  */
+
+  (•) : [128] -> [128] -> [128]
+  (•) X Y = reverse (pmod (pmult (reverse X) (reverse Y))
+                          <| 1 + x + x^^2 + x^^7 + x^^128|>)
+
+  /**
+  * Multiplication Operation on Blocks, [NISTSP800-38D] Section
+  * 6.3. This matches the spec very closely.
+  */
+
+  mult : [128] -> [128] -> [128]
+  mult X Y = last Z
+    where
+      R = 0b11100001 # (0 : [120])
+      Z = [0] # [ if [xi] == 0 then Zi else Zi ^ Vi
+                | Zi <- Z
+                | xi <- X
+                | Vi <- V ]
+      V = [Y] # [ if LSB`{1} Vi == 0 then Vi >> 1 else (Vi >> 1) ^ R
+                | Vi <- V ]
+
+  /**
+  * GHASH Function, [NISTSP800-38D] Section 6.4, Algorithm 2.
+  */
+
+  GHASH : {m} (fin m) => [128] -> [m * 128] -> [128]
+  GHASH H X = last Y
+    where Y = [0] # [ (Yi ^ Xi) • H | Yi <- Y | Xi <- groupBy`{128} X ]
+
+  /**
+  * The output of incrementing the right-most s bits of the bit
+  * string X, regarded as the binary representation of an integer, by
+  * 1 modulo 2s, [NISTSP800-38D] Sections 4.2.2 and 6.2. Care was
+  * taken here to ensure `s` could be zero.
+  */
+
+  inc : {s, a} (fin s, fin a, a >= s) => [a] -> [a]
+  inc X = MSB`{a-s} X # (LSB`{s} X + take (1 : [max s 1]))
+
+
+  /**
+  * The bit string consisting of the s right-most bits
+  * of the bit string X, [NISTSP800-38D] Section 4.2.2.
+  */
+
+  LSB : {s, a} (fin s, fin a, a >= s) => [a] -> [s]
+  LSB X = drop X
+
+  /**
+  * The bit string consisting of the s left-most bits of
+  * the bit string X, [NISTSP800-38D] Section 4.2.2.
+  */
+
+  MSB : {s, a} (fin s, a >= s) => [a] -> [s]
+  MSB X = take X
+
+  /**
+  * GCTR Function, [NISTSP800-38D] Section 6.5, Algorithm 3.
+  */
+
+  GCTR : {a} (fin a) => ([128] -> [128]) -> [128] -> [a] -> [a]
+  GCTR CIPHk ICB X = Y
+    where
+      Y = X ^ take`{a} (join (map CIPHk CB))
+      CB = iterate inc`{32} ICB
diff --git a/Primitive/Symmetric/Cipher/Authenticated/aes_gcm.bat b/Primitive/Symmetric/Cipher/Authenticated/aes_gcm.bat
new file mode 100644
index 00000000..f4c630d5
--- /dev/null
+++ b/Primitive/Symmetric/Cipher/Authenticated/aes_gcm.bat
@@ -0,0 +1,28 @@
+:l AES_GCM.cry
+
+:prove AES_GCM_test_vector_0
+:prove AES_GCM_test_vector_1
+:prove AES_GCM_test_vector_2
+:prove AES_GCM_test_vector_3
+:prove AES_GCM_test_vector_4
+:prove AES_GCM_invalid_test_vector
+
+// The following checks do not really provide any significant formal
+// verification because they check so little of the sample space.
+// They each take a long time to `:prove` and would likely require
+// manual modification to prove in a reasonable amount of time.
+
+// These properties can be checked manually; one of the APIs calls the other.
+// They take more than an hour to `:prove`.
+:check aesGcmDecryptionApisAreEquivalent
+:check aesGcmEncryptionApisAreEquivalent
+
+// This property is independent of the type parameters but we have to specify
+// them anyway.
+// It takes more than 25 minutes to `:prove`.
+:check dotAndMultAreEquivalent `{K=128, IV=96, AAD=0, T=128} {E=AES::encrypt}
+
+// Make sure that decryption is the inverse of encryption
+// This property takes more than 20 minutes to `:prove`.
+// It's also spot-checked in the test vectors
+:check aesGcmIsSymmetric
\ No newline at end of file