diff --git a/CHANGELOG.md b/CHANGELOG.md
index add0005..ffe5d02 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,7 @@
 # Unreleased
 
+* Fix parser for `assume_specification` to improve support
+
 # v0.5.1
 
 * Add support for `returns` clauses (see [verus#1283](https://github.com/verus-lang/verus/pull/1283))
diff --git a/src/verus.pest b/src/verus.pest
index bf174a8..324f7f6 100644
--- a/src/verus.pest
+++ b/src/verus.pest
@@ -738,8 +738,8 @@ assume_specification = {
     generic_param_list? ~
     lbracket_str ~ assume_specification_for ~ rbracket_str ~
     param_list ~
-    where_clause? ~
     ret_type? ~
+    where_clause? ~
     fn_qualifier ~
     semi_str
 }
diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs
index e13d439..5405b3f 100644
--- a/tests/verus-consistency.rs
+++ b/tests/verus-consistency.rs
@@ -2654,6 +2654,20 @@ pub assume_specification<T, const N: usize> [ <[T; N]>::as_slice ](ar: &[T; N])
     ensures
         ar@ == out@;
 
+pub assume_specification<Key, Value, S>[HashMap::<Key, Value, S>::insert](
+    m: &mut HashMap<Key, Value, S>,
+    k: Key,
+    v: Value,
+) -> (result: Option<Value>) where Key: Eq + Hash, S: BuildHasher
+    ensures
+        obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
+            &&& m@ == old(m)@.insert(k, v)
+            &&& match result {
+                Some(v) => old(m)@.contains_key(k) && v == old(m)[k],
+                None => !old(m)@.contains_key(k),
+            }
+        };
+
 } // verus!
 "#;
     assert_snapshot!(parse_and_format(file).unwrap(), @r"
@@ -2664,6 +2678,21 @@ pub assume_specification<T, const N: usize> [ <[T; N]>::as_slice ](ar: &[T; N])
             ar@ == out@,
     ;
 
+    pub assume_specification<Key, Value, S>[ HashMap::<Key, Value, S>::insert ](
+        m: &mut HashMap<Key, Value, S>,
+        k: Key,
+        v: Value,
+    ) -> (result: Option<Value>) where Key: Eq + Hash, S: BuildHasher
+        ensures
+            obeys_key_model::<Key>() && builds_valid_hashers::<S>() ==> {
+                &&& m@ == old(m)@.insert(k, v)
+                &&& match result {
+                    Some(v) => old(m)@.contains_key(k) && v == old(m)[k],
+                    None => !old(m)@.contains_key(k),
+                }
+            },
+    ;
+
     } // verus!
     ")
 }