diff --git a/crates/sui-framework/packages/sui-framework/Move.lock b/crates/sui-framework/packages/sui-framework/Move.lock
index 999fa85693d77..1bacad6d8baa2 100644
--- a/crates/sui-framework/packages/sui-framework/Move.lock
+++ b/crates/sui-framework/packages/sui-framework/Move.lock
@@ -2,18 +2,9 @@
 
 [move]
 version = 3
-manifest_digest = "06FD8F5C2B5CB25BBFF27D5AF3EEEC284C453E7190F2FA22CEC3FB4270B4B5D4"
-deps_digest = "3C4103934B1E040BB6B23F1D610B4EF9F2F1166A50A104EADCF77467C004C600"
-
-dependencies = [
-  { id = "MoveStdlib", name = "MoveStdlib" },
-]
+manifest_digest = "CD04B0AFFBEA9E38D757D76D077FCB8D9F7E69A99F98F542A4F6D5DBBB6B84A0"
+deps_digest = "E3B0C44298FC1C149AFBF4C8996FB92427AE41E4649B934CA495991B7852B855"
 
 [[move.package]]
 id = "MoveStdlib"
 source = { local = "../move-stdlib" }
-
-[move.toolchain-version]
-compiler-version = "1.30.0"
-edition = "2024.beta"
-flavor = "sui"
diff --git a/crates/sui-framework/packages/sui-system-specs/Move.toml b/crates/sui-framework/packages/sui-system-specs/Move.toml
new file mode 100644
index 0000000000000..788f684643331
--- /dev/null
+++ b/crates/sui-framework/packages/sui-system-specs/Move.toml
@@ -0,0 +1,11 @@
+[package]
+name = "SuiSystemSpecs"
+version = "0.0.1"
+published-at = "0x31"
+edition = "2024.beta"
+
+[dependencies]
+SuiSystem = { local = "../sui-system" }
+
+[addresses]
+sui_system_specs = "0x31"
diff --git a/crates/sui-framework/packages/sui-system-specs/sources/helpers.move b/crates/sui-framework/packages/sui-system-specs/sources/helpers.move
new file mode 100644
index 0000000000000..3e1003318ebde
--- /dev/null
+++ b/crates/sui-framework/packages/sui-system-specs/sources/helpers.move
@@ -0,0 +1,74 @@
+module sui_system_specs::helpers;
+
+#[spec_only]
+use std::{u64,u32,u16,u8};
+#[spec_only]
+use prover::prover::{ensures, invariant};
+
+#[spec_only]
+/// x+y will not abort (u64)
+fun can_add_u64(x: u64, y: u64): bool {
+    x.to_int().add(y.to_int()).lte(u64::max_value!().to_int())
+}
+
+#[spec_only]
+/// x+y will not abort (u32)
+fun can_add_u32(x: u32, y: u32): bool {
+    x.to_int().add(y.to_int()).lte(u32::max_value!().to_int())
+}
+
+#[spec_only]
+/// x-y will not abort
+fun can_sub_u64(x: u64, y: u64): bool {
+    y <= x
+}
+
+#[spec_only]
+/// x-y will not abort
+fun can_sub_u32(x: u32, y: u32): bool {
+    y <= x
+}
+
+// iteration macros have expansions that wrap up the contained loop,
+// so that an invariant cannot be attached.  the versions here have a
+// parameter that will give the loop invarant, which gets placed in
+// the correct spot.
+
+/// like `std::macros::range_do`, but allows for an invariant.
+/// The supplied function takes one parameter, the loop index
+public macro fun range_do_with_invariant<$T, $R: drop>($start: $T, $stop: $T, $f: |$T| -> $R, $g: |$T| -> bool) {
+    let mut i = $start;
+    let stop = $stop;
+    invariant!(|| { ensures( $g(i) ); });
+    while (i < stop) {
+        $f(i);
+        i = i + 1;
+    }
+}
+
+/// like `std::macros::do`, but allows for an invariant.
+/// The supplied function takes one parameter, the loop index
+public macro fun do_with_invariant<$T, $R: drop>($stop: $T, $f: |$T| -> $R, $g: |$T| -> bool) {
+    range_do_with_invariant!(0, $stop, $f, $g)
+}
+
+/// like `std:vectors::do`, but allows for an invariant.
+/// The supplied function takes one parameter, the loop index
+/// (which is also used as the index into the vector in the loop)
+public macro fun vector_do_ref_with_invariant<$T, $R: drop>($v: &vector<$T>, $f: |&$T| -> $R, $g: |u64| -> bool) {
+    let v = $v;
+    do_with_invariant!(v.length(), |i| $f(&v[i]), |i| i <= v.length() && ($g(i)))
+}
+
+/// like `std::vectors::find_index`, but allows for an invariant.
+public macro fun vector_find_index_with_invariant<$T>($v: &vector<$T>,
+    $f: |&$T| -> bool,
+    $g: |u64| -> bool): Option<u64> {
+    let v = $v;
+    'find_index: {
+        do_with_invariant!(v.length(),
+            (|i| if ($f(&v[i])) return 'find_index std::option::some(i)), // do this
+            (|i|  i <= v.length() && ($g(i)))); // using this invariant
+        std::option::none()
+    }
+}
diff --git a/crates/sui-framework/packages/sui-system-specs/sources/other_specs.move b/crates/sui-framework/packages/sui-system-specs/sources/other_specs.move
new file mode 100644
index 0000000000000..bf7a678c0ddc8
--- /dev/null
+++ b/crates/sui-framework/packages/sui-system-specs/sources/other_specs.move
@@ -0,0 +1,11 @@
+module sui_system_specs::other_specs;
+
+#[spec(target = sui::tx_context::epoch)]
+public fun epoch_spec(self: &TxContext): u64 {
+    sui::tx_context::epoch(self)
+}
+
+#[spec(target = sui::tx_context::sender)]
+public fun sender_spec(self: &TxContext): address {
+    sui::tx_context::sender(self)
+}
diff --git a/crates/sui-framework/packages/sui-system-specs/sources/stake_subsidy.move b/crates/sui-framework/packages/sui-system-specs/sources/stake_subsidy.move
new file mode 100644
index 0000000000000..e08144fb7bf4d
--- /dev/null
+++ b/crates/sui-framework/packages/sui-system-specs/sources/stake_subsidy.move
@@ -0,0 +1,21 @@
+module sui_system_specs::stake_subsidy;
+
+#[spec_only]
+use sui_system::stake_subsidy::{
+    StakeSubsidy,
+    current_epoch_subsidy_amount
+};
+
+// This invariant is needed to prove no abort in some of the non-public functions,
+// so can be skipped for now.
+
+// #[spec_only]
+// fun StakeSubsidy_inv(x: &StakeSubsidy): bool {
+//     x.stake_subsidy_decrease_rate <= BASIS_POINT_DENOMINATOR as u16 &&
+//     x.stake_subsidy_period_length > 0
+// }
+
+#[spec(prove, no_opaque, target = sui_system::stake_subsidy::current_epoch_subsidy_amount)]
+public fun current_epoch_subsidy_amount_spec(self: &StakeSubsidy): u64 {
+    current_epoch_subsidy_amount(self)
+}
diff --git a/crates/sui-framework/packages/sui-system-specs/sources/staking_pool.move b/crates/sui-framework/packages/sui-system-specs/sources/staking_pool.move
new file mode 100644
index 0000000000000..f38863ae622a0
--- /dev/null
+++ b/crates/sui-framework/packages/sui-system-specs/sources/staking_pool.move
@@ -0,0 +1,119 @@
+#[allow(unused_const)]
+module sui_system_specs::staking_pool;
+
+#[spec_only]
+use sui_system::staking_pool::{
+    PoolTokenExchangeRate,
+    StakedSui,
+    StakingPool,
+    FungibleStakedSui,
+    staked_sui_amount,
+    is_preactive,
+    is_inactive,
+    split_fungible_staked_sui,
+    join_fungible_staked_sui,
+    is_equal_staking_metadata,
+    split,
+    split_staked_sui,
+    pool_token_exchange_rate_at_epoch,
+    join_staked_sui,
+    fungible_staked_sui_value,
+    activation_epoch,
+};
+
+#[spec_only]
+use sui_system_specs::helpers::can_add_u64;
+
+#[spec_only]
+use prover::prover::{requires, ensures};
+
+#[spec_only]
+use prover::ghost;
+
+/// CLONE.
+#[spec_only]
+const MIN_STAKING_THRESHOLD: u64 = 1_000_000_000; // 1 SUI
+
+#[spec(prove, no_opaque, target = sui_system::staking_pool::staked_sui_amount)]
+public fun staked_sui_amount_spec(staked_sui: &StakedSui): u64 {
+    staked_sui_amount(staked_sui)
+}
+
+#[spec(prove, no_opaque, target = sui_system::staking_pool::is_preactive)]
+public fun is_preactive_spec(pool: &StakingPool): bool {
+    is_preactive(pool)
+}
+
+#[spec(prove, no_opaque, target = sui_system::staking_pool::is_inactive)]
+public fun is_inactive_spec(pool: &StakingPool): bool {
+    is_inactive(pool)
+}
+
+#[spec(prove, target = sui_system::staking_pool::split_fungible_staked_sui)]
+public fun split_fungible_staked_sui_spec(
+    fungible_staked_sui: &mut FungibleStakedSui,
+    split_amount: u64,
+    ctx: &mut TxContext,
+): FungibleStakedSui {
+    requires(split_amount <= fungible_staked_sui_value(fungible_staked_sui));
+    split_fungible_staked_sui(fungible_staked_sui, split_amount, ctx)
+}
+
+#[spec(prove, target = sui_system::staking_pool::join_fungible_staked_sui)]
+public fun join_fungible_staked_sui_spec(self: &mut FungibleStakedSui, other: FungibleStakedSui) {
+    requires(self.pool_id() == other.pool_id());
+    requires(can_add_u64(self.value(), other.value()));
+    join_fungible_staked_sui(self, other);
+}
+
+#[spec(prove, target = sui_system::staking_pool::split)]
+public fun split_spec(self: &mut StakedSui, split_amount: u64, ctx: &mut TxContext): StakedSui {
+    requires(split_amount <= staked_sui_amount(self));
+    requires(split_amount >= MIN_STAKING_THRESHOLD);
+    requires(staked_sui_amount(self) - split_amount >= MIN_STAKING_THRESHOLD);
+    split(self, split_amount, ctx)
+}
+
+#[spec(prove, no_opaque, target = sui_system::staking_pool::is_equal_staking_metadata)]
+public fun is_equal_staking_metadata_spec(self: &StakedSui, other: &StakedSui): bool {
+    is_equal_staking_metadata(self, other)
+}
+
+#[spec_only]
+/// function needed to make the requirements of `pool_token_exchange_rate_at_epoch_spec`
+/// expressible outside this module.
+public fun activation_epoch_is_positive(pool: &StakingPool): bool {
+    let epoch_opt = activation_epoch(pool);
+    epoch_opt.is_some() &&
+    *epoch_opt.borrow() > 0
+}
+
+#[spec(prove, target = sui_system::staking_pool::pool_token_exchange_rate_at_epoch)]
+public fun pool_token_exchange_rate_at_epoch_spec(
+    pool: &StakingPool,
+    epoch: u64,
+): PoolTokenExchangeRate {
+    requires(! pool.is_preactive());
+    // requires(*pool.activation_epoch.borrow() > 0); // visible? add to invariant?
+    requires(activation_epoch_is_positive(pool));
+    pool_token_exchange_rate_at_epoch(pool, epoch)
+}
+
+#[spec(prove, target = sui_system::staking_pool::split_staked_sui)]
+public fun split_staked_sui_spec(stake: &mut StakedSui, split_amount: u64, ctx: &mut TxContext) {
+    use specs::transfer_spec::{SpecTransferAddress,SpecTransferAddressExists};
+    ghost::declare_global_mut<SpecTransferAddressExists, bool>();
+    ghost::declare_global_mut<SpecTransferAddress, address>();
+    // preconditions from the call to split:
+    requires(split_amount <= staked_sui_amount(stake));
+    requires(split_amount >= MIN_STAKING_THRESHOLD);
+    requires(staked_sui_amount(stake) - split_amount >= MIN_STAKING_THRESHOLD);
+    split_staked_sui(stake, split_amount, ctx);
+}
+
+#[spec(prove, target = sui_system::staking_pool::join_staked_sui)]
+public fun join_staked_sui_spec(self: &mut StakedSui, other: StakedSui) {
+    requires(is_equal_staking_metadata(self, &other));
+    requires(can_add_u64(staked_sui_amount(self), staked_sui_amount(&other))); // or the join overflows
+    join_staked_sui(self, other);
+}
diff --git a/crates/sui-framework/packages/sui-system-specs/sources/storage_fund.move b/crates/sui-framework/packages/sui-system-specs/sources/storage_fund.move
new file mode 100644
index 0000000000000..16e2d1292fbb5
--- /dev/null
+++ b/crates/sui-framework/packages/sui-system-specs/sources/storage_fund.move
@@ -0,0 +1,27 @@
+module sui_system_specs::storage_fund;
+
+#[spec_only]
+use sui_system::storage_fund::{
+    StorageFund,
+    total_object_storage_rebates,
+    non_refundable_balance,
+    total_balance,
+};
+
+#[spec_only]
+use sui_system_specs::helpers::can_add_u64;
+
+#[spec_only]
+use prover::prover::requires;
+
+
+#[spec(prove, no_opaque, target = sui_system::storage_fund::total_object_storage_rebates)]
+public fun total_object_storage_rebates_spec(self: &StorageFund): u64 {
+    total_object_storage_rebates(self)
+}
+
+#[spec(prove, target = sui_system::storage_fund::total_balance)]
+public fun total_balance_spec(self: &StorageFund): u64 {
+    requires(can_add_u64(total_object_storage_rebates(self), non_refundable_balance(self)));
+    total_balance(self)
+}
diff --git a/crates/sui-framework/packages/sui-system-specs/sources/validator.move b/crates/sui-framework/packages/sui-system-specs/sources/validator.move
new file mode 100644
index 0000000000000..d3473417eadcb
--- /dev/null
+++ b/crates/sui-framework/packages/sui-system-specs/sources/validator.move
@@ -0,0 +1,65 @@
+#[allow(unused_const)]
+module sui_system_specs::validator;
+
+#[spec_only]
+use sui_system::staking_pool::{
+    PoolTokenExchangeRate,
+};
+
+#[spec_only]
+use sui_system::validator::{
+    Validator,
+    ValidatorMetadata,
+    is_preactive,
+    is_duplicate,
+    validate_metadata,
+    validate_metadata_bcs,
+    staking_pool_id,
+    pool_token_exchange_rate_at_epoch,
+    pool_activation_epoch,
+};
+#[spec_only]
+use sui_system::validator_cap::{Self, ValidatorOperationCap};
+
+#[spec_only]
+use prover::prover::requires;
+
+#[spec_only]
+public fun pool_activation_epoch_is_positive(validator: &Validator): bool {
+    let epoch_opt = pool_activation_epoch(validator);
+    epoch_opt.is_some() &&
+    *epoch_opt.borrow() > 0
+}
+
+#[spec(prove, no_opaque, target = sui_system::validator::is_preactive)]
+public fun is_preactive_spec(self: &Validator): bool {
+    is_preactive(self)
+}
+
+#[spec(prove, target = sui_system::validator::pool_token_exchange_rate_at_epoch)]
+public fun pool_token_exchange_rate_at_epoch_spec(self: &Validator, epoch: u64): PoolTokenExchangeRate {
+    requires(!is_preactive(self));
+    requires(pool_activation_epoch_is_positive(self));
+    pool_token_exchange_rate_at_epoch(self, epoch)
+}
+
+#[spec(prove, no_opaque, target = sui_system::validator::staking_pool_id)]
+public fun staking_pool_id_spec(self: &Validator): ID {
+    staking_pool_id(self)
+}
+
+#[spec(prove, target = sui_system::validator::is_duplicate)]
+public fun is_duplicate_spec(self: &Validator, other: &Validator): bool {
+    is_duplicate(self, other)
+}
+
+#[spec(prove, target = sui_system::validator::validate_metadata)]
+public fun validate_metadata_spec(metadata: &ValidatorMetadata) {
+    validate_metadata(metadata);
+}
+
+// "aborts if metadata is not valid" -- how to capture?
+#[spec(target = sui_system::validator::validate_metadata_bcs)]
+public fun validate_metadata_bcs_spec(metadata: vector<u8>) {
+    validate_metadata_bcs(metadata);
+}
diff --git a/crates/sui-framework/packages/sui-system/Move.lock b/crates/sui-framework/packages/sui-system/Move.lock
index af204d00c7990..fb23e91fa4f66 100644
--- a/crates/sui-framework/packages/sui-system/Move.lock
+++ b/crates/sui-framework/packages/sui-system/Move.lock
@@ -1,28 +1,27 @@
 # @generated by Move, please check-in and do not edit manually.
 
 [move]
-version = 1
+version = 3
 manifest_digest = "68AEB9354EE1D616F6D2293EC721FE3D7E810FEC4FE34197676ECFA3DA72CAE3"
 deps_digest = "3C4103934B1E040BB6B23F1D610B4EF9F2F1166A50A104EADCF77467C004C600"
-
 dependencies = [
-  { name = "MoveStdlib" },
-  { name = "Sui" },
+  { id = "MoveStdlib", name = "MoveStdlib" },
+  { id = "Sui", name = "Sui" },
 ]
 
 [[move.package]]
-name = "MoveStdlib"
+id = "MoveStdlib"
 source = { local = "../move-stdlib" }
 
 [[move.package]]
-name = "Sui"
+id = "Sui"
 source = { local = "../sui-framework" }
 
 dependencies = [
-  { name = "MoveStdlib" },
+  { id = "MoveStdlib", name = "MoveStdlib" },
 ]
 
 [move.toolchain-version]
-compiler-version = "1.22.0"
-edition = "legacy"
+compiler-version = "1.54.0"
+edition = "2024.beta"
 flavor = "sui"
diff --git a/crates/sui-framework/packages/sui-system/sources/storage_fund.move b/crates/sui-framework/packages/sui-system/sources/storage_fund.move
index 5cfae4038f0a4..5a572b118bd86 100644
--- a/crates/sui-framework/packages/sui-system/sources/storage_fund.move
+++ b/crates/sui-framework/packages/sui-system/sources/storage_fund.move
@@ -69,3 +69,10 @@ public fun total_object_storage_rebates(self: &StorageFund): u64 {
 public fun total_balance(self: &StorageFund): u64 {
     self.total_object_storage_rebates.value() + self.non_refundable_balance.value()
 }
+
+// === specs utils ===
+
+#[spec_only]
+public fun non_refundable_balance(self: &StorageFund): u64 {
+    self.non_refundable_balance.value()
+}
diff --git a/crates/sui-framework/packages/sui-system/sources/validator.move b/crates/sui-framework/packages/sui-system/sources/validator.move
index 9b6aedb648271..094778439656a 100644
--- a/crates/sui-framework/packages/sui-system/sources/validator.move
+++ b/crates/sui-framework/packages/sui-system/sources/validator.move
@@ -995,3 +995,13 @@ public(package) fun new_for_testing(
 
     validator
 }
+
+// === specs utils ===
+
+#[spec_only]
+use sui_system::staking_pool::activation_epoch;
+
+#[spec_only]
+public fun pool_activation_epoch(self: &Validator): Option<u64> {
+    activation_epoch(&self.staking_pool)
+}