diff --git a/capybaraKV/capybarakv/Cargo.toml b/capybaraKV/capybarakv/Cargo.toml
index 9b34db56..55f84950 100644
--- a/capybaraKV/capybarakv/Cargo.toml
+++ b/capybaraKV/capybarakv/Cargo.toml
@@ -19,7 +19,7 @@ default = [ "pmem" ]
 [dependencies]
 crc64fast = "1.0.0"
 rand = "0.8.5"
-vstd = "0.0.0-2025-11-30-0053"
+vstd = "0.0.0-2026-01-25-0057"
 pmcopy = { path = "../pmcopy" }
 
 [target.'cfg(target_family = "unix")'.dependencies]
diff --git a/capybaraKV/capybarakv/src/journal/commit_v.rs b/capybaraKV/capybarakv/src/journal/commit_v.rs
index 30395e50..b1350927 100644
--- a/capybaraKV/capybarakv/src/journal/commit_v.rs
+++ b/capybaraKV/capybarakv/src/journal/commit_v.rs
@@ -91,7 +91,7 @@ where
             forall|s1: Seq<u8>, s2: Seq<u8>| Self::recovery_equivalent_for_app(s1, s2) ==> #[trigger] perm_factory.permits(s1, s2),
         ensures
             self.inv(),
-            self == (Self{
+            *self == (Self{
                 powerpm: self.powerpm,
                 ..*old(self)
             }),
@@ -207,7 +207,7 @@ where
             forall|s1: Seq<u8>, s2: Seq<u8>| Self::recovery_equivalent_for_app(s1, s2) ==> #[trigger] perm_factory.permits(s1, s2),
         ensures
             self.inv(),
-            self == (Self{
+            *self == (Self{
                 powerpm: self.powerpm,
                 ..*old(self)
             }),
@@ -256,7 +256,7 @@ where
                                   self.sm.app_area_start as int, self.sm.app_area_end as int),
                 seqs_match_in_range(original_read_state, self.powerpm@.read_state,
                 self.sm.app_area_start as int, self.sm.app_area_end as int),
-                self == (Self{ powerpm: self.powerpm, ..*old(self) }),
+                *self == (Self{ powerpm: self.powerpm, ..*old(self) }),
                 crc_digest.bytes_in_digest() ==
                     self.powerpm@.read_state.subrange(self.sm.journal_entries_start as int, current_pos as int),
                 perm_factory.id() == self@.powerpm_id,
@@ -290,7 +290,7 @@ where
             self.inv(),
             self.powerpm.constants() == old(self).powerpm.constants(),
             self.powerpm.id() == old(self).powerpm.id(),
-            self == (Self{
+            *self == (Self{
                 powerpm: self.powerpm,
                 ..*old(self)
             }),
@@ -366,7 +366,7 @@ where
             self.inv(),
             self.powerpm.constants() == old(self).powerpm.constants(),
             self.powerpm.id() == old(self).powerpm.id(),
-            self == (Self{
+            *self == (Self{
                 status: Ghost(JournalStatus::Committed),
                 powerpm: self.powerpm,
                 ..*old(self)
@@ -471,7 +471,7 @@ where
             forall|s1: Seq<u8>, s2: Seq<u8>| Self::recovery_equivalent_for_app(s1, s2) ==> #[trigger] perm_factory.permits(s1, s2),
         ensures
             self.inv(),
-            self == (Self{
+            *self == (Self{
                 powerpm: self.powerpm,
                 ..*old(self)
             }),
@@ -563,7 +563,7 @@ where
             forall|s1: Seq<u8>, s2: Seq<u8>| Self::recovery_equivalent_for_app(s1, s2) ==> #[trigger] perm_factory.permits(s1, s2),
         ensures
             self.inv(),
-            self == (Self{
+            *self == (Self{
                 powerpm: self.powerpm,
                 ..*old(self)
             }),
@@ -614,7 +614,7 @@ where
                 seqs_match_in_range(original_commit_state, desired_commit_state,
                                     self.sm.app_area_start as int, self.sm.app_area_end as int),
                 recovers_to(original_commit_state, old(self).vm@, old(self).sm, old(self).constants),
-                self == (Self{ powerpm: self.powerpm, ..*old(self) }),
+                *self == (Self{ powerpm: self.powerpm, ..*old(self) }),
                 self.powerpm.constants() == old(self).powerpm.constants(),
                 self.powerpm.id() == old(self).powerpm.id(),
                 perm_factory.id() == self@.powerpm_id,
diff --git a/capybaraKV/capybarakv/src/journal/write_v.rs b/capybaraKV/capybarakv/src/journal/write_v.rs
index 263b3146..5a4d6b8b 100644
--- a/capybaraKV/capybarakv/src/journal/write_v.rs
+++ b/capybaraKV/capybarakv/src/journal/write_v.rs
@@ -155,7 +155,7 @@ where
                     },
                     Err(JournalError::NotEnoughSpace) => {
                         &&& space_needed > old(self)@.remaining_capacity
-                        &&& self == old(self)
+                        &&& *self == *old(self)
                     },
                     Err(_) => false,
                 }
diff --git a/capybaraKV/capybarakv/src/kv2/elements_v.rs b/capybaraKV/capybarakv/src/kv2/elements_v.rs
index 06a0625a..dcd45a53 100644
--- a/capybaraKV/capybarakv/src/kv2/elements_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/elements_v.rs
@@ -153,8 +153,8 @@ where
                 Ok(list_addr) => {
                     let old_list = if former_rm.list_addr == 0 { Seq::<L>::empty() }
                                    else { old(self).lists@.tentative.unwrap().m[former_rm.list_addr] };
-                    &&& self == Self{ status: Ghost(KvStoreStatus::ComponentsDontCorrespond),
-                                     journal: self.journal, lists: self.lists, ..*old(self) }
+                    &&& *self == Self{ status: Ghost(KvStoreStatus::ComponentsDontCorrespond),
+                                      journal: self.journal, lists: self.lists, ..*old(self) }
                     &&& self.inv()
                     &&& list_addr != 0
                     &&& list_addr == former_rm.list_addr || !old(self).lists@.tentative.unwrap().m.contains_key(list_addr)
diff --git a/capybaraKV/capybarakv/src/kv2/keys/crud_v.rs b/capybaraKV/capybarakv/src/kv2/keys/crud_v.rs
index 4726a226..6a223f92 100644
--- a/capybaraKV/capybarakv/src/kv2/keys/crud_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/keys/crud_v.rs
@@ -153,7 +153,7 @@ where
                 Ok(row_addr) => {
                     &&& 0 < self.free_list@.len()
                     &&& row_addr == self.free_list@.last()
-                    &&& self == (Self{ status: Ghost(KeyTableStatus::Inconsistent), ..*old(self) })
+                    &&& *self == (Self{ status: Ghost(KeyTableStatus::Inconsistent), ..*old(self) })
                     &&& recover_cdb(journal@.commit_state, row_addr + self.sm.row_cdb_start) == Some(true)
                     &&& seqs_match_except_in_range(old(journal)@.commit_state, journal@.commit_state,
                                                  row_addr as int, row_addr + self.sm.table.row_size)
@@ -524,7 +524,7 @@ where
             journal@.powerpm_id == old(journal)@.powerpm_id,
             match result {
                 Ok(()) => {
-                    &&& self == Self{ status: Ghost(KeyTableStatus::Inconsistent), ..*old(self) }
+                    &&& *self == Self{ status: Ghost(KeyTableStatus::Inconsistent), ..*old(self) }
                     &&& self.inv(journal@)
                     &&& self.internal_view().consistent_with_journaled_addrs(journal@.journaled_addrs, self.sm)
                     &&& journal@.matches_except_in_range(old(journal)@, row_addr + self.sm.row_metadata_start,
diff --git a/capybaraKV/capybarakv/src/kv2/lists/abort_v.rs b/capybaraKV/capybarakv/src/kv2/lists/abort_v.rs
index 6dbbe963..a713c1f5 100644
--- a/capybaraKV/capybarakv/src/kv2/lists/abort_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/lists/abort_v.rs
@@ -96,7 +96,7 @@ where
                     &&& !(old(self).m@[list_addr] is Durable)
                 }),
         ensures
-            self == (Self{ m: self.m, ..*old(self) }),
+            *self == (Self{ m: self.m, ..*old(self) }),
             self.internal_view() == (ListTableInternalView{ m: self.internal_view().m, ..old(self).internal_view() }),
             forall|i: int| 0 <= i < self.modifications.len() ==>
                 (#[trigger] old(self).modifications[i] matches Some(list_addr) ==> !self.m@.contains_key(list_addr)),
@@ -113,7 +113,7 @@ where
 
         for which_modification in 0..num_modifications
             invariant
-                self == (Self{ m: self.m, ..*old(self) }),
+                *self == (Self{ m: self.m, ..*old(self) }),
                 num_modifications == self.modifications.len(),
                 forall|i: int| 0 <= i < old(self).modifications.len() ==>
                     (#[trigger] old(self).modifications[i] matches Some(list_addr) ==> {
@@ -154,7 +154,7 @@ where
                 },
             forall|list_addr: u64| #[trigger] old(self).m@.contains_key(list_addr) ==> old(self).m@[list_addr] is Durable,
         ensures
-            self == (Self{ m: self.m, ..*old(self) }),
+            *self == (Self{ m: self.m, ..*old(self) }),
             forall|i: int| #![trigger self.deletes[i]] 0 <= i < self.deletes.len() ==> {
                 let summary = self.deletes[i];
                 &&& self.m@.contains_key(summary.head)
@@ -188,7 +188,7 @@ where
 
         for which_delete in 0..num_deletes
             invariant
-                self == (Self{ m: self.m, ..*old(self) }),
+                *self == (Self{ m: self.m, ..*old(self) }),
                 num_deletes == self.deletes.len(),
                 forall|list_addr: u64| #[trigger] self.deletes_inverse@.contains_key(list_addr) ==> {
                     let which_delete = self.deletes_inverse@[list_addr];
@@ -244,7 +244,7 @@ where
         requires
             old(self).valid(jv),
         ensures
-            self == (Self{ m: self.m, ..*old(self) }),
+            *self == (Self{ m: self.m, ..*old(self) }),
             self.internal_view().m == old(self).internal_view().abort().m,
     {
         self.update_m_to_reflect_abort_of_modifications();
diff --git a/capybaraKV/capybarakv/src/kv2/lists/append_v.rs b/capybaraKV/capybarakv/src/kv2/lists/append_v.rs
index 8143c77c..a08b018f 100644
--- a/capybaraKV/capybarakv/src/kv2/lists/append_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/lists/append_v.rs
@@ -423,7 +423,7 @@ where
         Ghost(prev_jv): Ghost<JournalView>,
     ) -> (result: Result<u64, KvError>)
         requires
-            old(self) == (Self{
+            *old(self) == (Self{
                 free_list: old(self).free_list,
                 m: old(self).m,
                 ..prev_self
@@ -580,7 +580,7 @@ where
         Ghost(prev_jv): Ghost<JournalView>,
     ) -> (result: Result<u64, KvError>)
         requires
-            old(self) == (Self{
+            *old(self) == (Self{
                 free_list: old(self).free_list,
                 m: old(self).m,
                 ..prev_self
diff --git a/capybaraKV/capybarakv/src/kv2/lists/commit_v.rs b/capybaraKV/capybarakv/src/kv2/lists/commit_v.rs
index 68755ee2..9a984012 100644
--- a/capybaraKV/capybarakv/src/kv2/lists/commit_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/lists/commit_v.rs
@@ -97,7 +97,7 @@ where
                 (#[trigger] old(self).modifications[which_modification] matches Some(list_addr) ==>
                  old(self).m@.contains_key(list_addr)),
         ensures
-            self == (Self{ m: self.m, ..*old(self) }),
+            *self == (Self{ m: self.m, ..*old(self) }),
             forall|i: int| 0 <= i < self.modifications.len() ==>
                 (#[trigger] old(self).modifications[i] matches Some(list_addr) ==> {
                     &&& self.m@.contains_key(list_addr)
@@ -115,7 +115,7 @@ where
         let num_modifications = self.modifications.len();
         for which_modification in 0..num_modifications
             invariant
-                self == (Self{ m: self.m, ..*old(self) }),
+                *self == (Self{ m: self.m, ..*old(self) }),
                 num_modifications == self.modifications.len(),
                 forall|i: int| 0 <= i < old(self).modifications.len() ==>
                     (#[trigger] old(self).modifications[i] matches Some(list_addr) ==>
@@ -153,7 +153,7 @@ where
         requires
             old(self).valid(jv),
         ensures
-            self == (Self{ m: self.m, ..*old(self) }),
+            *self == (Self{ m: self.m, ..*old(self) }),
             self.internal_view().m == old(self).internal_view().commit().m,
     {
         self.update_m_to_reflect_commit_of_modifications();
diff --git a/capybaraKV/capybarakv/src/kv2/lists/update_v.rs b/capybaraKV/capybarakv/src/kv2/lists/update_v.rs
index b9c51310..6eb356f5 100644
--- a/capybaraKV/capybarakv/src/kv2/lists/update_v.rs
+++ b/capybaraKV/capybarakv/src/kv2/lists/update_v.rs
@@ -519,7 +519,7 @@ where
         requires
             prev_self.valid(journal@),
             journal.valid(),
-            old(self) == (Self{
+            *old(self) == (Self{
                 m: old(self).m,
                 ..prev_self
             }),
@@ -530,8 +530,8 @@ where
             old(self).m@ == prev_self.m@.remove(list_addr),
         ensures
             journal.valid(),
-            self == (Self{ m: self.m, deletes: self.deletes, deletes_inverse: self.deletes_inverse,
-                           modifications: self.modifications, ..*old(self) }),
+            *self == (Self{ m: self.m, deletes: self.deletes, deletes_inverse: self.deletes_inverse,
+                            modifications: self.modifications, ..*old(self) }),
             ({
                 let (success, new_entry) = result;
                 if success {
@@ -551,7 +551,7 @@ where
                 }
                 else {
                     &&& !journal@.pm_constants.impervious_to_corruption()
-                    &&& self == old(self)
+                    &&& *self == *old(self)
                     &&& new_entry == entry
                 }
             }),
diff --git a/multilog/multilog/Cargo.toml b/multilog/multilog/Cargo.toml
index 3be4534a..6ef17da5 100644
--- a/multilog/multilog/Cargo.toml
+++ b/multilog/multilog/Cargo.toml
@@ -19,7 +19,7 @@ default = [ "pmem" ]
 [dependencies]
 crc64fast = "1.0.0"
 rand = "0.8.5"
-vstd = "0.0.0-2025-11-30-0053"
+vstd = "0.0.0-2026-01-25-0057"
 pmsafe = { path = "../pmsafe" }
 
 [target.'cfg(target_os = "windows")'.dependencies]
diff --git a/pmemlog/Cargo.toml b/pmemlog/Cargo.toml
index a7b75be0..8224fe93 100644
--- a/pmemlog/Cargo.toml
+++ b/pmemlog/Cargo.toml
@@ -6,7 +6,7 @@ edition = "2021"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-vstd = "0.0.0-2025-11-30-0053"
+vstd = "0.0.0-2026-01-25-0057"
 crc64fast = "1.0.0"
 
 [lints.rust]
diff --git a/unverified/metadata_kv/Cargo.toml b/unverified/metadata_kv/Cargo.toml
index 0a1bf78e..658d6c86 100644
--- a/unverified/metadata_kv/Cargo.toml
+++ b/unverified/metadata_kv/Cargo.toml
@@ -7,5 +7,5 @@ edition = "2021"
 
 [dependencies]
 rand = "0.8"
-vstd = "0.0.0-2025-11-30-0053"
+vstd = "0.0.0-2026-01-25-0057"
 proptest = "1.4"