diff --git a/aptos-framework/doc/reconfiguration_with_dkg.md b/aptos-framework/doc/reconfiguration_with_dkg.md
index 231ce0b06..f64d57763 100644
--- a/aptos-framework/doc/reconfiguration_with_dkg.md
+++ b/aptos-framework/doc/reconfiguration_with_dkg.md
@@ -164,8 +164,10 @@ Abort if no DKG is in progress.
 <b>requires</b> <a href="chain_status.md#0x1_chain_status_is_operating">chain_status::is_operating</a>();
 <b>include</b> <a href="stake.md#0x1_stake_ResourceRequirement">stake::ResourceRequirement</a>;
 <b>include</b> <a href="stake.md#0x1_stake_GetReconfigStartTimeRequirement">stake::GetReconfigStartTimeRequirement</a>;
-<b>include</b> <a href="../../aptos-stdlib/../move-stdlib/doc/features.md#0x1_features_spec_periodical_reward_rate_decrease_enabled">features::spec_periodical_reward_rate_decrease_enabled</a>() ==&gt; <a href="staking_config.md#0x1_staking_config_StakingRewardsConfigEnabledRequirement">staking_config::StakingRewardsConfigEnabledRequirement</a>;
+<b>include</b> <a href="../../aptos-stdlib/../move-stdlib/doc/features.md#0x1_features_spec_periodical_reward_rate_decrease_enabled">features::spec_periodical_reward_rate_decrease_enabled</a>(
+) ==&gt; <a href="staking_config.md#0x1_staking_config_StakingRewardsConfigEnabledRequirement">staking_config::StakingRewardsConfigEnabledRequirement</a>;
 <b>aborts_if</b> <b>false</b>;
+<b>pragma</b> verify_duration_estimate = 600;
 </code></pre>
 
 
diff --git a/aptos-framework/sources/reconfiguration_with_dkg.spec.move b/aptos-framework/sources/reconfiguration_with_dkg.spec.move
index fd5709dd5..d03da0033 100644
--- a/aptos-framework/sources/reconfiguration_with_dkg.spec.move
+++ b/aptos-framework/sources/reconfiguration_with_dkg.spec.move
@@ -12,8 +12,10 @@ spec aptos_framework::reconfiguration_with_dkg {
         requires chain_status::is_operating();
         include stake::ResourceRequirement;
         include stake::GetReconfigStartTimeRequirement;
-        include features::spec_periodical_reward_rate_decrease_enabled() ==> staking_config::StakingRewardsConfigEnabledRequirement;
+        include features::spec_periodical_reward_rate_decrease_enabled(
+        ) ==> staking_config::StakingRewardsConfigEnabledRequirement;
         aborts_if false;
+        pragma verify_duration_estimate = 600; // TODO: set because of timeout (property proved).
     }
 
     spec finish(account: &signer) {
@@ -59,5 +61,4 @@ spec aptos_framework::reconfiguration_with_dkg {
         requires dkg::has_incomplete_session();
         aborts_if false;
     }
-
 }