diff --git a/verified-node-replication/src/constants.rs b/verified-node-replication/src/constants.rs
index 78a1ca9..413c133 100644
--- a/verified-node-replication/src/constants.rs
+++ b/verified-node-replication/src/constants.rs
@@ -5,8 +5,8 @@
 //! verification. The constants mostly define the size of the log, and certain thresholds
 //! when warnings are being printed etc.
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 verus! {
 
diff --git a/verified-node-replication/src/exec/context.rs b/verified-node-replication/src/exec/context.rs
index 4e3e8b4..ddcf781 100644
--- a/verified-node-replication/src/exec/context.rs
+++ b/verified-node-replication/src/exec/context.rs
@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 use vstd::{
     atomic_ghost::AtomicU64,
diff --git a/verified-node-replication/src/exec/log.rs b/verified-node-replication/src/exec/log.rs
index e9741aa..939e825 100644
--- a/verified-node-replication/src/exec/log.rs
+++ b/verified-node-replication/src/exec/log.rs
@@ -1,6 +1,6 @@
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 use vstd::{
     atomic_ghost::{AtomicBool, AtomicU64},
diff --git a/verified-node-replication/src/exec/mod.rs b/verified-node-replication/src/exec/mod.rs
index ea29c9d..f1e1ecb 100644
--- a/verified-node-replication/src/exec/mod.rs
+++ b/verified-node-replication/src/exec/mod.rs
@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 use vstd::prelude::*;
 
diff --git a/verified-node-replication/src/exec/replica.rs b/verified-node-replication/src/exec/replica.rs
index c5f6003..473b5de 100644
--- a/verified-node-replication/src/exec/replica.rs
+++ b/verified-node-replication/src/exec/replica.rs
@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 use vstd::{
     atomic_ghost::AtomicU64,
diff --git a/verified-node-replication/src/exec/rwlock.rs b/verified-node-replication/src/exec/rwlock.rs
index 1f93444..b58b623 100644
--- a/verified-node-replication/src/exec/rwlock.rs
+++ b/verified-node-replication/src/exec/rwlock.rs
@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 use vstd::{
     atomic_ghost::{AtomicBool, AtomicU64},
     atomic_with_ghost,
diff --git a/verified-node-replication/src/exec/utils.rs b/verified-node-replication/src/exec/utils.rs
index e3bbbbd..5137c24 100644
--- a/verified-node-replication/src/exec/utils.rs
+++ b/verified-node-replication/src/exec/utils.rs
@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 use vstd::{prelude::*, seq::Seq};
 
diff --git a/verified-node-replication/src/lib.rs b/verified-node-replication/src/lib.rs
index d737120..4b6419a 100644
--- a/verified-node-replication/src/lib.rs
+++ b/verified-node-replication/src/lib.rs
@@ -8,8 +8,8 @@
 //!
 //! This top-level module contains the trusted traits and the top-level lemmas.
 #[allow(unused_imports)]
-use builtin::*;
-use state_machines_macros::state_machine;
+use verus_builtin::*;
+use verus_state_machines_macros::state_machine;
 use vstd::prelude::*;
 
 pub mod constants;
diff --git a/verified-node-replication/src/spec/cyclicbuffer.rs b/verified-node-replication/src/spec/cyclicbuffer.rs
index 988b240..5236622 100644
--- a/verified-node-replication/src/spec/cyclicbuffer.rs
+++ b/verified-node-replication/src/spec/cyclicbuffer.rs
@@ -2,14 +2,14 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 use vstd::prelude::*;
 
 use vstd::cell::{CellId, PointsTo};
 
-use state_machines_macros::*;
+use verus_state_machines_macros::*;
 
 use crate::Dispatch;
 
diff --git a/verified-node-replication/src/spec/flat_combiner.rs b/verified-node-replication/src/spec/flat_combiner.rs
index 56364d8..9a9ea16 100644
--- a/verified-node-replication/src/spec/flat_combiner.rs
+++ b/verified-node-replication/src/spec/flat_combiner.rs
@@ -2,12 +2,12 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 use vstd::prelude::*;
 
-use state_machines_macros::*;
+use verus_state_machines_macros::*;
 
 use super::types::*;
 // use super::utils::*;
diff --git a/verified-node-replication/src/spec/linearization.rs b/verified-node-replication/src/spec/linearization.rs
index a3042a4..0220555 100644
--- a/verified-node-replication/src/spec/linearization.rs
+++ b/verified-node-replication/src/spec/linearization.rs
@@ -3,7 +3,7 @@
 //
 // The Linearization Proof
 #[allow(unused_imports)]
-use builtin::*;
+use verus_builtin::*;
 // use vstd::*;
 use vstd::prelude::*;
 
diff --git a/verified-node-replication/src/spec/rwlock.rs b/verified-node-replication/src/spec/rwlock.rs
index 01cad92..cb8de79 100644
--- a/verified-node-replication/src/spec/rwlock.rs
+++ b/verified-node-replication/src/spec/rwlock.rs
@@ -2,9 +2,9 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
-use state_machines_macros::tokenized_state_machine;
+use verus_builtin::*;
+use verus_builtin_macros::*;
+use verus_state_machines_macros::tokenized_state_machine;
 use vstd::{multiset::*, prelude::*};
 
 verus! {
diff --git a/verified-node-replication/src/spec/simple_log.rs b/verified-node-replication/src/spec/simple_log.rs
index 1d2a528..54a969f 100644
--- a/verified-node-replication/src/spec/simple_log.rs
+++ b/verified-node-replication/src/spec/simple_log.rs
@@ -1,9 +1,9 @@
 // Verified Node Replication Library
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-use builtin::*;
-use builtin_macros::*;
-use state_machines_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
+use verus_state_machines_macros::*;
 
 use vstd::prelude::*;
 
diff --git a/verified-node-replication/src/spec/types.rs b/verified-node-replication/src/spec/types.rs
index 84105d4..8f02623 100644
--- a/verified-node-replication/src/spec/types.rs
+++ b/verified-node-replication/src/spec/types.rs
@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 use crate::Dispatch;
 
diff --git a/verified-node-replication/src/spec/unbounded_log.rs b/verified-node-replication/src/spec/unbounded_log.rs
index 9e1dfaa..bb6de98 100644
--- a/verified-node-replication/src/spec/unbounded_log.rs
+++ b/verified-node-replication/src/spec/unbounded_log.rs
@@ -3,9 +3,9 @@
 //
 // rust_verify/tests/example.rs ignore
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
-use state_machines_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
+use verus_state_machines_macros::*;
 
 use vstd::map::Map;
 use vstd::prelude::*;
diff --git a/verified-node-replication/src/spec/unbounded_log_refines_simplelog.rs b/verified-node-replication/src/spec/unbounded_log_refines_simplelog.rs
index aab57eb..483a240 100644
--- a/verified-node-replication/src/spec/unbounded_log_refines_simplelog.rs
+++ b/verified-node-replication/src/spec/unbounded_log_refines_simplelog.rs
@@ -3,8 +3,8 @@
 //
 // rust_verify/tests/example.rs ignore
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 use vstd::prelude::*;
 
@@ -15,7 +15,7 @@ use vstd::seq::Seq;
 use vstd::seq_lib::*;
 
 #[cfg(verus_keep_ghost)]
-use state_machines_macros::*;
+use verus_state_machines_macros::*;
 
 use crate::{Dispatch, InputOperation, OutputOperation, ReqId};
 
diff --git a/verified-node-replication/src/spec/utils.rs b/verified-node-replication/src/spec/utils.rs
index f48b596..73e1511 100644
--- a/verified-node-replication/src/spec/utils.rs
+++ b/verified-node-replication/src/spec/utils.rs
@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 use vstd::prelude::*;
 use vstd::set::Set;