diff --git a/PROPERTY_STANDARDS.md b/PROPERTY_STANDARDS.md
new file mode 100644
index 0000000..535b1d5
--- /dev/null
+++ b/PROPERTY_STANDARDS.md
@@ -0,0 +1,435 @@
+# Property Documentation Standards
+
+This document defines the standardization rules for all property test functions in the Crytic Properties repository. These standards ensure consistency, clarity, and educational value across all 168+ properties.
+
+## Overview
+
+All property test functions must follow these standards:
+1. **NatSpec Documentation** - Complete structured documentation
+2. **Testing Mode** - Clearly specified approach (INTERNAL/EXTERNAL/ISOLATED/FUNCTION_OVERRIDE/MODEL)
+3. **Invariant Description** - Plain English explanation of what must always be true
+4. **Logical Organization** - Properties grouped into meaningful sections
+5. **Unique Identifiers** - Trackable property IDs for reference
+
+## Testing Modes
+
+Based on [Echidna's common testing approaches](https://secure-contracts.com/program-analysis/echidna/basic/common-testing-approaches.html#partial-testing), we use five testing modes:
+
+### INTERNAL
+Test harness inherits from the contract under test. Properties have direct access to internal state and functions.
+
+**When to use:** Testing your own contracts during development.
+
+**Example:**
+```solidity
+contract TestHarness is MyToken, CryticERC20BasicProperties {
+    constructor() {
+        _mint(USER1, INITIAL_BALANCE);
+    }
+}
+```
+
+### EXTERNAL
+Test harness interacts with the contract through its public interface only. Simulates real-world usage patterns.
+
+**When to use:** Testing deployed contracts or simulating external user interactions.
+
+**Example:**
+```solidity
+contract TestHarness is CryticERC20ExternalBasicProperties {
+    constructor() {
+        token = ITokenMock(address(new MyToken()));
+    }
+}
+```
+
+### ISOLATED
+Testing individual components abstracted from the rest of the system. Particularly useful for stateless mathematical operations.
+
+**When to use:** Testing math libraries, pure functions, or components with no external dependencies.
+
+**Example:** Testing ABDKMath64x64 arithmetic operations independently.
+
+### FUNCTION_OVERRIDE
+Uses Solidity's override mechanism to mock or disable dependencies that cannot be simulated (e.g., oracles, bridges, signature verification).
+
+**When to use:** System depends on off-chain components or external systems that cannot be easily mocked.
+
+**Example:**
+```solidity
+contract TestHarness is System {
+    function verifySignature(...) public override returns (bool) {
+        return true; // Mock: signatures always valid for testing
+    }
+}
+```
+
+### MODEL
+Abstract mathematical model represents expected behavior. Properties compare actual contract behavior against a simplified reference implementation.
+
+**When to use:** Contract implements complex logic with known mathematical properties that can be expressed as a simpler model.
+
+**Example:** Comparing vault share calculations against a simplified mathematical formula.
+
+---
+
+## NatSpec Documentation Template
+
+Every property function **must** include the following NatSpec tags:
+
+```solidity
+/// @title [Human-Readable Property Name]
+/// @notice [Brief user-facing description of what this property tests]
+/// @dev Testing Mode: [INTERNAL|EXTERNAL|ISOLATED|FUNCTION_OVERRIDE|MODEL]
+/// @dev Invariant: [Plain English description of what must always be true]
+/// @dev [Optional: Additional context, examples, or preconditions]
+/// @custom:property-id [STANDARD]-[CATEGORY]-[NUMBER]
+function test_Standard_PropertyName() public {
+    // Implementation
+}
+```
+
+### Tag Requirements
+
+| Tag | Required | Purpose | Example |
+|-----|----------|---------|---------|
+| `@title` | ✅ Yes | Clear, human-readable property name | "User Balance Cannot Exceed Total Supply" |
+| `@notice` | ✅ Yes | Brief description for users/auditors | "Ensures individual balances never exceed the total token supply" |
+| `@dev Testing Mode:` | ✅ Yes | Specify which testing approach is used | "Testing Mode: INTERNAL" |
+| `@dev Invariant:` | ✅ Yes | Plain English invariant description | "For any address `user`, `balanceOf(user) <= totalSupply()` must always hold" |
+| `@dev [context]` | ⚠️ Optional | Additional explanations, examples, or preconditions | "This is a fundamental accounting invariant..." |
+| `@custom:property-id` | ✅ Yes | Unique identifier for tracking | "ERC20-BALANCE-001" |
+
+---
+
+## Property ID Format
+
+Property IDs follow the pattern: `[STANDARD]-[CATEGORY]-[NUMBER]`
+
+### Standard Prefixes
+- `ERC20` - ERC20 token properties
+- `ERC721` - ERC721 NFT properties
+- `ERC4626` - ERC4626 vault properties
+- `MATH` - Mathematical library properties
+
+### Category Guidelines
+
+Choose categories based on **functionality** being tested:
+
+**For ERC20:**
+- `SUPPLY` - Total supply accounting
+- `BALANCE` - Individual balance accounting
+- `TRANSFER` - Transfer mechanics and safety
+- `ALLOWANCE` - Approve/transferFrom mechanics
+- `BURN` - Burning mechanics
+- `MINT` - Minting mechanics
+- `PAUSE` - Pause functionality
+
+**For ERC721:**
+- `OWNERSHIP` - Token ownership tracking
+- `TRANSFER` - Transfer mechanics
+- `APPROVAL` - Approval mechanics
+- `BURN` - Burning mechanics
+- `MINT` - Minting mechanics
+
+**For ERC4626:**
+- `ACCOUNTING` - Share/asset accounting
+- `DEPOSIT` - Deposit mechanics
+- `WITHDRAW` - Withdrawal mechanics
+- `SECURITY` - Security properties (inflation attacks, etc.)
+- `ROUNDING` - Rounding direction safety
+
+**For Math:**
+- `[OPERATION]` - Name of the operation (ADD, SUB, MUL, DIV, SQRT, LOG, etc.)
+
+### Numbering
+- Use zero-padded 3-digit numbers: 001, 002, 003, etc.
+- Sequential within each category
+- No gaps in numbering
+
+### Examples
+- `ERC20-SUPPLY-001` - First supply accounting property
+- `ERC20-TRANSFER-005` - Fifth transfer property
+- `ERC721-OWNERSHIP-001` - First ownership property
+- `ERC4626-SECURITY-002` - Second security property
+- `MATH-ADD-001` - First addition property
+
+---
+
+## File Organization
+
+### File-Level Documentation
+
+Every property contract must include comprehensive contract-level NatSpec:
+
+```solidity
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity ^0.8.0;
+
+import "./PropertiesHelper.sol";
+
+/**
+ * @title [Contract Name] Properties
+ * @author Crytic (Trail of Bits)
+ * @notice [High-level description of what this contract tests]
+ * @dev Testing Mode: [Primary mode used in this contract]
+ * @dev This contract contains [X] properties testing [brief description]
+ * @dev
+ * @dev Usage Example:
+ * @dev ```solidity
+ * @dev contract TestHarness is MyToken, CryticERC20BasicProperties {
+ * @dev     constructor() {
+ * @dev         _mint(USER1, INITIAL_BALANCE);
+ * @dev         initialSupply = totalSupply();
+ * @dev     }
+ * @dev }
+ * @dev ```
+ */
+contract ContractNameProperties is PropertiesAsserts {
+    // Contract body
+}
+```
+
+### Section Structure
+
+Properties should be organized into logical sections based on functionality:
+
+```solidity
+// ================================================================
+// STATE VARIABLES & CONFIGURATION
+// ================================================================
+
+/// @notice [Description of state variable]
+uint256 public someStateVar;
+
+
+/* ================================================================
+
+                    [SECTION NAME IN CAPS]
+
+   Description: [What this section tests]
+   Testing Mode: [MODE if different from default]
+   Property Count: [X]
+
+   ================================================================ */
+
+// Properties for this section...
+
+
+/* ================================================================
+
+                    [NEXT SECTION NAME]
+
+   Description: [What this section tests]
+   Property Count: [X]
+
+   ================================================================ */
+
+// Properties for next section...
+```
+
+### Section Header Format
+
+Must follow this exact format (matching ABDKMath64x64PropertyTests.sol):
+
+```solidity
+/* ================================================================
+
+                    [SECTION TITLE HERE]
+
+   Description: [Brief explanation]
+   Testing Mode: [MODE] (if different from file default)
+   Property Count: [X]
+
+   ================================================================ */
+```
+
+**Rules:**
+- Opening `/*` and closing `*/` on their own lines
+- `================================================================` lines (64 equals signs)
+- Empty line after opening
+- Section title centered (3 blank lines before title)
+- Empty line after title
+- Description and metadata left-aligned with 3-space indent
+- Empty line before closing
+
+---
+
+## Complete Example
+
+Here's a complete before/after example:
+
+### Before (Current State)
+```solidity
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity ^0.8.13;
+
+import "../util/ERC20TestBase.sol";
+
+abstract contract CryticERC20BasicProperties is CryticERC20Base {
+    // User balance must not exceed total supply
+    function test_ERC20_userBalanceNotHigherThanSupply() public {
+        assertLte(
+            balanceOf(msg.sender),
+            totalSupply(),
+            "User balance higher than total supply"
+        );
+    }
+
+    // Address zero should have zero balance
+    function test_ERC20_zeroAddressBalance() public {
+        assertEq(
+            balanceOf(address(0)),
+            0,
+            "Address zero balance not equal to zero"
+        );
+    }
+}
+```
+
+### After (Standardized)
+```solidity
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity ^0.8.13;
+
+import "../util/ERC20TestBase.sol";
+
+/**
+ * @title ERC20 Basic Properties
+ * @author Crytic (Trail of Bits)
+ * @notice Core invariant properties for ERC20 token implementations
+ * @dev Testing Mode: INTERNAL (can also be used EXTERNALLY via interface)
+ * @dev This contract contains 17 fundamental properties testing supply accounting,
+ * @dev balance accounting, transfer mechanics, and allowance operations.
+ * @dev
+ * @dev Usage Example:
+ * @dev ```solidity
+ * @dev contract TestHarness is MyToken, CryticERC20BasicProperties {
+ * @dev     constructor() {
+ * @dev         _mint(USER1, INITIAL_BALANCE);
+ * @dev         _mint(USER2, INITIAL_BALANCE);
+ * @dev         initialSupply = totalSupply();
+ * @dev         isMintableOrBurnable = false; // Set based on your token
+ * @dev     }
+ * @dev }
+ * @dev ```
+ */
+abstract contract CryticERC20BasicProperties is CryticERC20Base {
+
+    // ================================================================
+    // STATE VARIABLES
+    // ================================================================
+
+    /// @notice Initial total supply recorded at test initialization
+    /// @dev Used for constant supply checks in non-mintable/burnable tokens
+    uint256 public initialSupply;
+
+    /// @notice Flag indicating if token supply can change after deployment
+    /// @dev Set to true for mintable/burnable tokens, false for fixed supply
+    bool public isMintableOrBurnable;
+
+
+    /* ================================================================
+
+                    BALANCE ACCOUNTING PROPERTIES
+
+       Description: Properties verifying individual balance accounting
+       Testing Mode: INTERNAL
+       Property Count: 2
+
+       ================================================================ */
+
+    /// @title User Balance Cannot Exceed Total Supply
+    /// @notice Ensures individual user balances never exceed the total token supply
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: For any address `user`, `balanceOf(user) <= totalSupply()` must always hold
+    /// @dev This is a fundamental accounting invariant - if violated, the token contract
+    /// @dev has a critical bug allowing token creation from nothing or double-counting
+    /// @custom:property-id ERC20-BALANCE-001
+    function test_ERC20_userBalanceNotHigherThanSupply() public {
+        assertLte(
+            balanceOf(msg.sender),
+            totalSupply(),
+            "User balance higher than total supply"
+        );
+    }
+
+    /// @title Zero Address Has Zero Balance
+    /// @notice The zero address should never hold tokens
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: `balanceOf(address(0)) == 0` must always hold
+    /// @dev The zero address is conventionally used to represent burned tokens.
+    /// @dev If it holds a non-zero balance, tokens are effectively lost/inaccessible
+    /// @custom:property-id ERC20-BALANCE-002
+    function test_ERC20_zeroAddressBalance() public {
+        assertEq(
+            balanceOf(address(0)),
+            0,
+            "Address zero balance not equal to zero"
+        );
+    }
+}
+```
+
+---
+
+## Code Style Requirements
+
+### Assertion Messages
+- Must be descriptive and clearly indicate what invariant was violated
+- Use present tense ("Balance exceeds supply" not "Balance exceeded supply")
+- No abbreviations or unclear technical jargon
+
+### Formatting
+- Property functions should have blank lines between them for readability
+- Long assertions should be formatted with one parameter per line
+- Consistent indentation (4 spaces)
+
+### Comments
+- Replace inline comments with NatSpec documentation
+- Only keep inline comments if they explain non-obvious implementation details
+- Avoid redundant comments that simply restate the code
+
+---
+
+## Contribution Checklist
+
+Before submitting a PR with new or modified properties:
+
+- [ ] All property functions have complete NatSpec (@title, @notice, @dev tags)
+- [ ] Testing mode is clearly documented in @dev tag
+- [ ] Invariant is described in plain English in @dev tag
+- [ ] Property has a unique ID in @custom:property-id tag
+- [ ] Property ID follows the [STANDARD]-[CATEGORY]-[NUMBER] format
+- [ ] Property is placed in the appropriate logical section
+- [ ] Section headers follow the standardized format
+- [ ] File has comprehensive contract-level NatSpec
+- [ ] Assertion messages are clear and descriptive
+- [ ] Related documentation (PROPERTIES.md, README) is updated
+
+---
+
+## Automated Validation
+
+Future: A linting script will validate:
+- All `test_*` functions have required NatSpec tags
+- Testing mode is specified and valid
+- Invariant descriptions are present
+- Property IDs are unique and properly formatted
+- Section headers follow the standard format
+
+---
+
+## Questions?
+
+For questions about these standards:
+1. Review existing standardized files (e.g., ERC20BasicProperties.sol)
+2. Check examples in this document
+3. Open an issue in the GitHub repository
+4. Refer to the [contribution guidelines](./CONTRIBUTING.md)
+
+## Document History
+
+- **2025-11**: Initial standardization document created
+- Based on issue: "Standardize properties in the repo"
+- Reference implementation: ABDKMath64x64PropertyTests.sol section headers
diff --git a/contracts/ERC20/internal/properties/ERC20BasicProperties.sol b/contracts/ERC20/internal/properties/ERC20BasicProperties.sol
index 9ce039e..5ed7d62 100644
--- a/contracts/ERC20/internal/properties/ERC20BasicProperties.sol
+++ b/contracts/ERC20/internal/properties/ERC20BasicProperties.sol
@@ -3,19 +3,74 @@ pragma solidity ^0.8.13;
 
 import "../util/ERC20TestBase.sol";
 
+/**
+ * @title ERC20 Basic Properties
+ * @author Crytic (Trail of Bits)
+ * @notice Core invariant properties for ERC20 token implementations
+ * @dev Testing Mode: INTERNAL (test harness inherits from token and properties)
+ * @dev This contract contains 17 fundamental properties that test supply accounting,
+ * @dev balance accounting, transfer mechanics, and allowance operations for ERC20 tokens.
+ * @dev These properties represent the essential invariants that all ERC20 implementations
+ * @dev should maintain to ensure correct accounting and safe operations.
+ * @dev
+ * @dev Usage Example:
+ * @dev ```solidity
+ * @dev contract TestHarness is MyToken, CryticERC20BasicProperties {
+ * @dev     constructor() {
+ * @dev         _mint(USER1, INITIAL_BALANCE);
+ * @dev         _mint(USER2, INITIAL_BALANCE);
+ * @dev         _mint(USER3, INITIAL_BALANCE);
+ * @dev         initialSupply = totalSupply();
+ * @dev         isMintableOrBurnable = false; // Set based on your token's features
+ * @dev     }
+ * @dev }
+ * @dev ```
+ */
 abstract contract CryticERC20BasicProperties is CryticERC20Base {
     constructor() {}
 
-    ////////////////////////////////////////
-    // Properties
 
-    // Total supply should change only by means of mint or burn
+    /* ================================================================
+
+                    SUPPLY ACCOUNTING PROPERTIES
+
+       Description: Properties verifying total supply accounting correctness
+       Testing Mode: INTERNAL
+       Property Count: 1
+
+       ================================================================ */
+
+    /// @title Constant Supply Invariant
+    /// @notice For non-mintable/burnable tokens, total supply must remain constant
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: If `!isMintableOrBurnable`, then `totalSupply() == initialSupply` must always hold
+    /// @dev This property only applies to tokens with fixed supply. For mintable or burnable
+    /// @dev tokens, set `isMintableOrBurnable = true` to skip this check.
+    /// @dev Preconditions: Only meaningful when isMintableOrBurnable is false
+    /// @custom:property-id ERC20-SUPPLY-001
     function test_ERC20_constantSupply() public virtual {
         require(!isMintableOrBurnable);
         assertEq(initialSupply, totalSupply(), "Token supply was modified");
     }
 
-    // User balance must not exceed total supply
+
+    /* ================================================================
+
+                    BALANCE ACCOUNTING PROPERTIES
+
+       Description: Properties verifying individual balance accounting correctness
+       Testing Mode: INTERNAL
+       Property Count: 3
+
+       ================================================================ */
+
+    /// @title User Balance Cannot Exceed Total Supply
+    /// @notice Ensures that any individual user's balance never exceeds the total token supply
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: For any address `user`, `balanceOf(user) <= totalSupply()` must always hold
+    /// @dev This is a fundamental accounting invariant. If violated, the token contract has
+    /// @dev a critical bug allowing token creation from nothing, double-counting, or overflow.
+    /// @custom:property-id ERC20-BALANCE-001
     function test_ERC20_userBalanceNotHigherThanSupply() public {
         assertLte(
             balanceOf(msg.sender),
@@ -24,7 +79,13 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base {
         );
     }
 
-    // Sum of users balance must not exceed total supply
+    /// @title Sum of User Balances Cannot Exceed Total Supply
+    /// @notice Ensures that the sum of test user balances never exceeds the total supply
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: `balanceOf(USER1) + balanceOf(USER2) + balanceOf(USER3) <= totalSupply()`
+    /// @dev This checks that the accounting for multiple users remains consistent with total supply.
+    /// @dev While not exhaustive (doesn't check all addresses), it provides confidence in multi-user scenarios.
+    /// @custom:property-id ERC20-BALANCE-002
     function test_ERC20_usersBalancesNotHigherThanSupply() public {
         uint256 balance = balanceOf(USER1) +
             balanceOf(USER2) +
@@ -36,7 +97,14 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base {
         );
     }
 
-    // Address zero should have zero balance
+    /// @title Zero Address Has Zero Balance
+    /// @notice The zero address should never hold tokens
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: `balanceOf(address(0)) == 0` must always hold
+    /// @dev The zero address (0x0) is conventionally used to represent burned tokens or null state.
+    /// @dev If it holds a non-zero balance, tokens are effectively lost and inaccessible, breaking
+    /// @dev the accounting assumption that all supply is either held by users or explicitly burned.
+    /// @custom:property-id ERC20-BALANCE-003
     function test_ERC20_zeroAddressBalance() public {
         assertEq(
             balanceOf(address(0)),
@@ -45,7 +113,24 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base {
         );
     }
 
-    // Transfers to zero address should not be allowed
+
+    /* ================================================================
+
+                    TRANSFER PROPERTIES
+
+       Description: Properties verifying transfer mechanics and safety guarantees
+       Testing Mode: INTERNAL
+       Property Count: 10
+
+       ================================================================ */
+
+    /// @title Transfer to Zero Address Must Fail
+    /// @notice Transfers to the zero address should not be allowed
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: `transfer(address(0), amount)` must return false or revert for any amount > 0
+    /// @dev Prevents accidental token burning via transfer. Burning should use explicit burn()
+    /// @dev functions if supported. This protects users from irreversible mistakes.
+    /// @custom:property-id ERC20-TRANSFER-001
     function test_ERC20_transferToZeroAddress() public {
         uint256 balance = balanceOf(address(this));
         require(balance > 0);
@@ -54,7 +139,13 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base {
         assertWithMsg(r == false, "Successful transfer to address zero");
     }
 
-    // Transfers to zero address should not be allowed
+    /// @title TransferFrom to Zero Address Must Fail
+    /// @notice TransferFrom to the zero address should not be allowed
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: `transferFrom(sender, address(0), amount)` must return false or revert
+    /// @dev Similar to direct transfers, this prevents accidental burning through delegated transfers.
+    /// @dev Protects against both user error and potential exploits involving allowances.
+    /// @custom:property-id ERC20-TRANSFER-002
     function test_ERC20_transferFromToZeroAddress(uint256 value) public {
         uint256 balance_sender = balanceOf(msg.sender);
         uint256 current_allowance = allowance(msg.sender, address(this));
@@ -67,7 +158,13 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base {
         assertWithMsg(r == false, "Successful transferFrom to address zero");
     }
 
-    // Self transfers should not break accounting
+    /// @title Self TransferFrom Preserves Balance
+    /// @notice Transferring tokens to oneself via transferFrom should not change balance
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: After `transferFrom(user, user, amount)`, `balanceOf(user)` must remain unchanged
+    /// @dev Self-transfers are a special case that some implementations handle incorrectly.
+    /// @dev The balance should remain the same since tokens are both leaving and entering the same account.
+    /// @custom:property-id ERC20-TRANSFER-003
     function test_ERC20_selfTransferFrom(uint256 value) public {
         uint256 balance_sender = balanceOf(msg.sender);
         uint256 current_allowance = allowance(msg.sender, address(this));
@@ -85,7 +182,13 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base {
         );
     }
 
-    // Self transfers should not break accounting
+    /// @title Self Transfer Preserves Balance
+    /// @notice Transferring tokens to oneself should not change balance
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: After `transfer(sender, amount)` where sender == recipient, balance must be unchanged
+    /// @dev Self-transfers via direct transfer() should behave identically to self transferFrom().
+    /// @dev This is a common edge case that can expose accounting bugs in naive implementations.
+    /// @custom:property-id ERC20-TRANSFER-004
     function test_ERC20_selfTransfer(uint256 value) public {
         uint256 balance_sender = balanceOf(address(this));
         require(balance_sender > 0);
@@ -99,7 +202,13 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base {
         );
     }
 
-    // Transfers for more than available balance should not be allowed
+    /// @title TransferFrom More Than Balance Must Fail
+    /// @notice TransferFrom exceeding sender's balance should not be allowed
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: `transferFrom(sender, recipient, amount)` where `amount > balanceOf(sender)` must fail
+    /// @dev Even with sufficient allowance, transfers cannot exceed the sender's actual balance.
+    /// @dev Both sender and recipient balances must remain unchanged on failure.
+    /// @custom:property-id ERC20-TRANSFER-005
     function test_ERC20_transferFromMoreThanBalance(address target) public {
         uint256 balance_sender = balanceOf(msg.sender);
         uint256 balance_receiver = balanceOf(target);
@@ -123,7 +232,13 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base {
         );
     }
 
-    // Transfers for more than available balance should not be allowed
+    /// @title Transfer More Than Balance Must Fail
+    /// @notice Transfers exceeding sender's balance should not be allowed
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: `transfer(recipient, amount)` where `amount > balanceOf(sender)` must fail
+    /// @dev Fundamental safety property preventing token creation or negative balances.
+    /// @dev Both sender and recipient balances must remain unchanged on failure.
+    /// @custom:property-id ERC20-TRANSFER-006
     function test_ERC20_transferMoreThanBalance(address target) public {
         uint256 balance_sender = balanceOf(address(this));
         uint256 balance_receiver = balanceOf(target);
@@ -146,7 +261,13 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base {
         );
     }
 
-    // Zero amount transfers should not break accounting
+    /// @title Zero Amount Transfer Succeeds Without Changes
+    /// @notice Transferring zero tokens should succeed without modifying balances
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: `transfer(recipient, 0)` must succeed and leave all balances unchanged
+    /// @dev Zero-value transfers should be no-ops. Some contracts incorrectly reject them,
+    /// @dev which can break composability with other contracts expecting standard behavior.
+    /// @custom:property-id ERC20-TRANSFER-007
     function test_ERC20_transferZeroAmount(address target) public {
         uint256 balance_sender = balanceOf(address(this));
         uint256 balance_receiver = balanceOf(target);
@@ -166,7 +287,13 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base {
         );
     }
 
-    // Zero amount transfers should not break accounting
+    /// @title Zero Amount TransferFrom Succeeds Without Changes
+    /// @notice TransferFrom with zero tokens should succeed without modifying balances
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: `transferFrom(sender, recipient, 0)` must succeed and leave balances unchanged
+    /// @dev Zero-value delegated transfers should also be no-ops, maintaining consistency
+    /// @dev with direct transfer behavior and ERC20 standard expectations.
+    /// @custom:property-id ERC20-TRANSFER-008
     function test_ERC20_transferFromZeroAmount(address target) public {
         uint256 balance_sender = balanceOf(msg.sender);
         uint256 balance_receiver = balanceOf(target);
@@ -187,7 +314,14 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base {
         );
     }
 
-    // Transfers should update accounting correctly
+    /// @title Transfer Updates Balances Correctly
+    /// @notice Regular transfers should update sender and recipient balances correctly
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: After `transfer(recipient, amount)`, sender balance decreases by `amount`
+    /// @dev and recipient balance increases by `amount`
+    /// @dev This is the core correctness property for transfers: tokens leaving one account
+    /// @dev must arrive in the destination account, preserving total supply.
+    /// @custom:property-id ERC20-TRANSFER-009
     function test_ERC20_transfer(address target, uint256 amount) public {
         require(target != address(this));
         uint256 balance_sender = balanceOf(address(this));
@@ -209,7 +343,14 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base {
         );
     }
 
-    // Transfers should update accounting correctly
+    /// @title TransferFrom Updates Balances Correctly
+    /// @notice Delegated transfers should update sender and recipient balances correctly
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: After `transferFrom(sender, recipient, amount)`, sender balance decreases
+    /// @dev by `amount` and recipient balance increases by `amount`
+    /// @dev Core correctness property for delegated transfers. Must maintain same accounting
+    /// @dev guarantees as direct transfers, just with allowance consumption.
+    /// @custom:property-id ERC20-TRANSFER-010
     function test_ERC20_transferFrom(address target, uint256 amount) public {
         require(target != address(this));
         require(target != msg.sender);
@@ -233,7 +374,24 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base {
         );
     }
 
-    // Approve should set correct allowances
+
+    /* ================================================================
+
+                    ALLOWANCE PROPERTIES
+
+       Description: Properties verifying approve/transferFrom allowance mechanics
+       Testing Mode: INTERNAL
+       Property Count: 3
+
+       ================================================================ */
+
+    /// @title Approve Sets Allowance Correctly
+    /// @notice Approve should set the allowance to the specified amount
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: After `approve(spender, amount)`, `allowance(owner, spender) == amount`
+    /// @dev Basic correctness property for the approval mechanism. The allowance value
+    /// @dev must be set exactly as specified, enabling precise delegation of spending rights.
+    /// @custom:property-id ERC20-ALLOWANCE-001
     function test_ERC20_setAllowance(address target, uint256 amount) public {
         bool r = this.approve(target, amount);
         assertWithMsg(r == true, "Failed to set allowance via approve");
@@ -244,7 +402,13 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base {
         );
     }
 
-    // Approve should set correct allowances
+    /// @title Approve Can Overwrite Previous Allowance
+    /// @notice Approve should be able to change existing allowances
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: Sequential `approve()` calls should each set allowance to the new value
+    /// @dev Allowances must be updateable to allow users to modify or revoke spending permissions.
+    /// @dev This is essential for security (reducing allowances) and flexibility (increasing them).
+    /// @custom:property-id ERC20-ALLOWANCE-002
     function test_ERC20_setAllowanceTwice(
         address target,
         uint256 amount
@@ -266,7 +430,15 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base {
         );
     }
 
-    // TransferFrom should decrease allowance
+    /// @title TransferFrom Decreases Allowance
+    /// @notice TransferFrom should decrease the allowance by the transferred amount
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: After `transferFrom(owner, recipient, amount)`, allowance decreases by `amount`
+    /// @dev Exception: Allowance of `type(uint256).max` is treated as infinite by some implementations
+    /// @dev This ensures that allowances are consumed correctly, preventing spenders from
+    /// @dev exceeding their delegated permissions. The infinite allowance exception is a
+    /// @dev common optimization to avoid storage updates for "unlimited" approvals.
+    /// @custom:property-id ERC20-ALLOWANCE-003
     function test_ERC20_spendAllowanceAfterTransfer(
         address target,
         uint256 amount
@@ -281,7 +453,7 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base {
         bool r = this.transferFrom(msg.sender, target, transfer_value);
         assertWithMsg(r == true, "transferFrom failed");
 
-        // Some implementations take an allowance of 2**256-1 as infinite, and therefore don't update
+        // Some implementations treat type(uint256).max as infinite allowance
         if (current_allowance != type(uint256).max) {
             assertEq(
                 allowance(msg.sender, address(this)),