diff --git a/.gitignore b/.gitignore
index 70487d22..32102142 100644
--- a/.gitignore
+++ b/.gitignore
@@ -7,3 +7,4 @@
 node_modules
 test-ledger
 dist
+/.codex/
diff --git a/p-token/test-properties/VERIFICATION_GUIDE.md b/p-token/test-properties/VERIFICATION_GUIDE.md
index f39830bd..04bc2b0f 100644
--- a/p-token/test-properties/VERIFICATION_GUIDE.md
+++ b/p-token/test-properties/VERIFICATION_GUIDE.md
@@ -82,6 +82,16 @@ then the `Account` fields will be equivalent. Cheatcode `maybe_same_account` wil
 Currently this cheatcode will only link symbolic state for SPL Token _Account_ (not `AccountInfo` and not P-Token),
 that would be valid under the same assumptions but has not been necessary for the current proofs.
 
+### Multisig `m`/`n` Bounds
+The `cheatcode_is_multisig` marker sets up a symbolic `Multisig` layout, but it does not by itself constrain the
+`m` and `n` fields. For harnesses that reason about multisig validation, we therefore add assumptions that
+`1 <= m <= MAX_SIGNERS` and `1 <= n <= MAX_SIGNERS`.
+
+These are not extra behavioral restrictions on the implementation. They match the invariants enforced by
+`initialize_multisig`, and they exclude symbolic states that cannot arise from a valid initialized multisig account.
+Without these bounds, the prover can explore unreachable cases such as `n == 0`, `m == 0`, or `n > MAX_SIGNERS`,
+which lead to proof artifacts rather than meaningful counterexamples.
+
 ## Limitations
 
 ### Compiling with non-solana target
@@ -170,4 +180,4 @@ cargo build --features runtime-verification
 ## Notes
 
 - Default settings: max-depth 2000, max-iterations 500, timeout 1h
-- Results are stored in `artefacts/proof-SHA1-SHA2/` directory, where `SHA1` and `SHA2` indicate the version of `solana-token` and `mir-semantics` used.
\ No newline at end of file
+- Results are stored in `artefacts/proof-SHA1-SHA2/` directory, where `SHA1` and `SHA2` indicate the version of `solana-token` and `mir-semantics` used.
diff --git a/specs/shared/inner_test_validate_owner.rs b/specs/shared/inner_test_validate_owner.rs
index 2abd0abd..a4cc7fed 100644
--- a/specs/shared/inner_test_validate_owner.rs
+++ b/specs/shared/inner_test_validate_owner.rs
@@ -26,16 +26,18 @@ fn expected_validate_owner_result(
 
             // Did all declared and allowd signers sign?
             let unsigned_exists = tx_signers.iter().any(|potential_signer| {
-                multisig.signers.iter().any(|registered_key| {
-                    registered_key == key!(potential_signer) && !is_signer!(potential_signer)
-                })
+                multisig.signers[0..multisig.n as usize]
+                    .iter()
+                    .any(|registered_key| {
+                        registered_key == key!(potential_signer) && !is_signer!(potential_signer)
+                    })
             });
             if unsigned_exists {
                 return Err(ProgramError::MissingRequiredSignature);
             }
 
             // Were enough signatures received?
-            let signers_count = multisig.signers
+            let signers_count = multisig.signers[0..multisig.n as usize]
                 .iter()
                 .filter_map(|registered_key| {
                     tx_signers.iter().find(|potential_signer| {
@@ -93,9 +95,11 @@ fn inner_test_validate_owner(
 
             // Did all declared and allowd signers sign?
             let unsigned_exists = tx_signers.iter().any(|potential_signer| {
-                multisig.signers.iter().any(|registered_key| {
-                    registered_key == key!(potential_signer) && !is_signer!(potential_signer)
-                })
+                multisig.signers[0..multisig.n as usize]
+                    .iter()
+                    .any(|registered_key| {
+                        registered_key == key!(potential_signer) && !is_signer!(potential_signer)
+                    })
             });
             if unsigned_exists {
                 assert_eq!(result, Err(ProgramError::MissingRequiredSignature));
@@ -103,7 +107,7 @@ fn inner_test_validate_owner(
             }
 
             // Were enough signatures received?
-            let signers_count = multisig.signers
+            let signers_count = multisig.signers[0..multisig.n as usize]
                 .iter()
                 .filter_map(|registered_key| {
                     tx_signers.iter().find(|potential_signer| {
diff --git a/specs/shared/test_process_approve_checked_multisig.rs b/specs/shared/test_process_approve_checked_multisig.rs
index 29737f6a..c9fb0759 100644
--- a/specs/shared/test_process_approve_checked_multisig.rs
+++ b/specs/shared/test_process_approve_checked_multisig.rs
@@ -14,6 +14,17 @@ fn test_process_approve_checked_multisig(
     cheatcode_account!(&accounts[2]); // Delegate
     cheatcode_multisig!(&accounts[3]); // Owner
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[3]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let amount = u64::from_le_bytes([
diff --git a/specs/shared/test_process_approve_multisig.rs b/specs/shared/test_process_approve_multisig.rs
index 87d1c6d4..1eadcba0 100644
--- a/specs/shared/test_process_approve_multisig.rs
+++ b/specs/shared/test_process_approve_multisig.rs
@@ -12,6 +12,17 @@ fn test_process_approve_multisig(
     cheatcode_account!(&accounts[1]); // Delegate
     cheatcode_multisig!(&accounts[2]); // Owner
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[2]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let amount = unsafe { u64::from_le_bytes(*(instruction_data.as_ptr() as *const [u8; 8])) };
diff --git a/specs/shared/test_process_burn_checked_multisig.rs b/specs/shared/test_process_burn_checked_multisig.rs
index 38515d8c..2b6d64e9 100644
--- a/specs/shared/test_process_burn_checked_multisig.rs
+++ b/specs/shared/test_process_burn_checked_multisig.rs
@@ -12,6 +12,17 @@ fn test_process_burn_checked_multisig(
     cheatcode_mint!(&accounts[1]);
     cheatcode_multisig!(&accounts[2]);
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[2]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let mint_old = get_mint(&accounts[1]);
diff --git a/specs/shared/test_process_burn_multisig.rs b/specs/shared/test_process_burn_multisig.rs
index c45b7f7a..318e0e62 100644
--- a/specs/shared/test_process_burn_multisig.rs
+++ b/specs/shared/test_process_burn_multisig.rs
@@ -12,6 +12,17 @@ pub fn test_process_burn_multisig(
     cheatcode_mint!(&accounts[1]);
     cheatcode_multisig!(&accounts[2]);
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[2]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let mint_old = get_mint(&accounts[1]);
diff --git a/specs/shared/test_process_close_account_multisig.rs b/specs/shared/test_process_close_account_multisig.rs
index e9c45093..e2d15acb 100644
--- a/specs/shared/test_process_close_account_multisig.rs
+++ b/specs/shared/test_process_close_account_multisig.rs
@@ -8,6 +8,17 @@ fn test_process_close_account_multisig(accounts: &[AccountInfo; 4]) -> ProgramRe
     cheatcode_account!(&accounts[1]);
     cheatcode_multisig!(&accounts[2]);
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[2]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let src_initialised = src_old.is_initialized();
diff --git a/specs/shared/test_process_freeze_account_multisig.rs b/specs/shared/test_process_freeze_account_multisig.rs
index c583f9de..3374496f 100644
--- a/specs/shared/test_process_freeze_account_multisig.rs
+++ b/specs/shared/test_process_freeze_account_multisig.rs
@@ -8,6 +8,17 @@ fn test_process_freeze_account_multisig(accounts: &[AccountInfo; 4]) -> ProgramR
     cheatcode_mint!(&accounts[1]);
     cheatcode_multisig!(&accounts[2]);
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[2]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let mint_old = get_mint(&accounts[1]);
diff --git a/specs/shared/test_process_mint_to_checked_multisig.rs b/specs/shared/test_process_mint_to_checked_multisig.rs
index 4cb006c3..ed446d23 100644
--- a/specs/shared/test_process_mint_to_checked_multisig.rs
+++ b/specs/shared/test_process_mint_to_checked_multisig.rs
@@ -12,6 +12,17 @@ fn test_process_mint_to_checked_multisig(
     cheatcode_account!(&accounts[1]);
     cheatcode_multisig!(&accounts[2]);
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[2]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let mint_old = get_mint(&accounts[0]);
     let dst_old = get_account(&accounts[1]);
diff --git a/specs/shared/test_process_mint_to_multisig.rs b/specs/shared/test_process_mint_to_multisig.rs
index 35859a59..50076357 100644
--- a/specs/shared/test_process_mint_to_multisig.rs
+++ b/specs/shared/test_process_mint_to_multisig.rs
@@ -12,6 +12,17 @@ fn test_process_mint_to_multisig(
     cheatcode_account!(&accounts[1]);
     cheatcode_multisig!(&accounts[2]);
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[2]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let mint_old = get_mint(&accounts[0]);
     let dst_old = get_account(&accounts[1]);
diff --git a/specs/shared/test_process_revoke_multisig.rs b/specs/shared/test_process_revoke_multisig.rs
index 1f30ad69..352d4c52 100644
--- a/specs/shared/test_process_revoke_multisig.rs
+++ b/specs/shared/test_process_revoke_multisig.rs
@@ -6,6 +6,17 @@ fn test_process_revoke_multisig(accounts: &[AccountInfo; 3]) -> ProgramResult {
     cheatcode_account!(&accounts[0]); // Source Account
     cheatcode_multisig!(&accounts[1]); // Owner
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[1]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let src_initialised = src_old.is_initialized();
diff --git a/specs/shared/test_process_set_authority_account_multisig.rs b/specs/shared/test_process_set_authority_account_multisig.rs
index e70033e3..de467a73 100644
--- a/specs/shared/test_process_set_authority_account_multisig.rs
+++ b/specs/shared/test_process_set_authority_account_multisig.rs
@@ -12,6 +12,17 @@ fn test_process_set_authority_account_multisig(
     cheatcode_account!(&accounts[0]); // Assume Account
     cheatcode_multisig!(&accounts[1]); // Authority
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[1]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let src_initialised = src_old.is_initialized();
diff --git a/specs/shared/test_process_set_authority_mint_multisig.rs b/specs/shared/test_process_set_authority_mint_multisig.rs
index 5fc06067..e85c8438 100644
--- a/specs/shared/test_process_set_authority_mint_multisig.rs
+++ b/specs/shared/test_process_set_authority_mint_multisig.rs
@@ -12,6 +12,17 @@ fn test_process_set_authority_mint_multisig(
     cheatcode_mint!(&accounts[0]); // Assume Mint
     cheatcode_multisig!(&accounts[1]); // Authority
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[1]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let mint_old = get_mint(&accounts[0]);
     let mint_data_len = accounts[0].data_len();
diff --git a/specs/shared/test_process_thaw_account_multisig.rs b/specs/shared/test_process_thaw_account_multisig.rs
index 5abbd200..ccd8103b 100644
--- a/specs/shared/test_process_thaw_account_multisig.rs
+++ b/specs/shared/test_process_thaw_account_multisig.rs
@@ -8,6 +8,17 @@ fn test_process_thaw_account_multisig(accounts: &[AccountInfo; 4]) -> ProgramRes
     cheatcode_mint!(&accounts[1]);
     cheatcode_multisig!(&accounts[2]);
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[2]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let mint_old = get_mint(&accounts[1]);
diff --git a/specs/shared/test_process_transfer_checked_multisig.rs b/specs/shared/test_process_transfer_checked_multisig.rs
index b2a7d618..0c3d49fa 100644
--- a/specs/shared/test_process_transfer_checked_multisig.rs
+++ b/specs/shared/test_process_transfer_checked_multisig.rs
@@ -14,6 +14,17 @@ fn test_process_transfer_checked_multisig(
     cheatcode_account!(&accounts[2]);
     cheatcode_multisig!(&accounts[3]);
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[3]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     #[cfg(feature = "assumptions")]
     // Link symbolic state of dst and src if they have the same key
     cheatcode_maybe_same_account(&accounts[0], &accounts[2]);
diff --git a/specs/shared/test_process_transfer_multisig.rs b/specs/shared/test_process_transfer_multisig.rs
index fd916b90..47b94535 100644
--- a/specs/shared/test_process_transfer_multisig.rs
+++ b/specs/shared/test_process_transfer_multisig.rs
@@ -12,6 +12,17 @@ fn test_process_transfer_multisig(
     cheatcode_account!(&accounts[1]);
     cheatcode_multisig!(&accounts[2]);
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[2]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     #[cfg(feature = "assumptions")]
     // Link symbolic state of dst and src if they have the same key
     cheatcode_maybe_same_account(&accounts[0], &accounts[1]);
diff --git a/specs/shared/test_validate_owner_multisig.rs b/specs/shared/test_validate_owner_multisig.rs
index 0526d482..a70d3377 100644
--- a/specs/shared/test_validate_owner_multisig.rs
+++ b/specs/shared/test_validate_owner_multisig.rs
@@ -8,6 +8,17 @@ fn test_validate_owner_multisig(
     cheatcode_account!(&accounts[0]);    // Source Account
     cheatcode_multisig!(&accounts[1]);   // Owner (multisig)
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[1]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let expected_owner = src_old.owner;