diff --git a/contracts/math/package.json b/contracts/math/package.json
index e27ea572..2af5d5fd 100644
--- a/contracts/math/package.json
+++ b/contracts/math/package.json
@@ -26,6 +26,7 @@
   "packageManager": "pnpm@10.4.1",
   "devDependencies": {
     "@types/node": "^24.10.0",
+    "fast-check": "^3.23.1",
     "typescript": "^5.8.3",
     "vitest": "^3.1.4"
   },
diff --git a/contracts/math/src/test/Bytes32.fuzz.test.ts b/contracts/math/src/test/Bytes32.fuzz.test.ts
new file mode 100644
index 00000000..aa6450fd
--- /dev/null
+++ b/contracts/math/src/test/Bytes32.fuzz.test.ts
@@ -0,0 +1,462 @@
+import { beforeEach, describe, test } from 'vitest';
+import * as fc from 'fast-check';
+import { Bytes32Simulator } from './Bytes32Simulator';
+
+let bytes32Simulator: Bytes32Simulator;
+
+const setup = () => {
+  bytes32Simulator = new Bytes32Simulator();
+};
+
+// Maximum value that fits in 254 bits (field modulus constraint)
+const MAX_FIELD254 = 2n ** 254n - 1n;
+
+// Custom arbitrary for 32-byte arrays within the 254-bit field constraint
+const arbBytes32InField = (): fc.Arbitrary<Uint8Array> => {
+  return fc
+    .bigUint({ max: MAX_FIELD254 })
+    .map((value) => {
+      const bytes = new Uint8Array(32);
+      let remaining = value;
+      // Convert bigint to bytes (little-endian)
+      for (let i = 0; i < 32 && remaining > 0n; i++) {
+        bytes[i] = Number(remaining & 0xffn);
+        remaining = remaining >> 8n;
+      }
+      return bytes;
+    });
+};
+
+// Custom arbitrary for any 32-byte arrays
+const arbBytes32 = (): fc.Arbitrary<Uint8Array> => {
+  return fc.uint8Array({ minLength: 32, maxLength: 32 });
+};
+
+// Helper to convert bytes to bigint (little-endian)
+const bytesToBigInt = (bytes: Uint8Array): bigint => {
+  let result = 0n;
+  for (let i = bytes.length - 1; i >= 0; i--) {
+    result = (result << 8n) | BigInt(bytes[i]);
+  }
+  return result;
+};
+
+// Helper to create bytes from bigint (little-endian)
+const bigIntToBytes = (value: bigint): Uint8Array => {
+  const bytes = new Uint8Array(32);
+  let remaining = value;
+  for (let i = 0; i < 32 && remaining > 0n; i++) {
+    bytes[i] = Number(remaining & 0xffn);
+    remaining = remaining >> 8n;
+  }
+  return bytes;
+};
+
+// Helper to check if two Uint8Arrays are equal
+const bytesEqual = (a: Uint8Array, b: Uint8Array): boolean => {
+  if (a.length !== b.length) return false;
+  return a.every((val, idx) => val === b[idx]);
+};
+
+/**
+ * Property-based fuzz tests for Bytes32 operations
+ * Using fast-check for automated test case generation
+ */
+describe('Bytes32 - Property-Based Fuzz Tests', () => {
+  beforeEach(setup);
+
+  describe('Conversion Properties', () => {
+    test('fromBytes and toBytes are inverses within field', () => {
+      fc.assert(
+        fc.property(
+          arbBytes32InField(),
+          (bytes) => {
+            const field = bytes32Simulator.fromBytes(bytes);
+            const reconstructed = bytes32Simulator.toBytes(field);
+            return bytesEqual(bytes, reconstructed);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('toBytes and fromBytes are inverses', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUint({ max: MAX_FIELD254 }),
+          (field) => {
+            const bytes = bytes32Simulator.toBytes(field);
+            const reconstructed = bytes32Simulator.fromBytes(bytes);
+            return reconstructed === field;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('fromBytes produces values within field bounds', () => {
+      fc.assert(
+        fc.property(
+          arbBytes32InField(),
+          (bytes) => {
+            const field = bytes32Simulator.fromBytes(bytes);
+            return field >= 0n && field < 2n ** 254n;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('fromBytes rejects values exceeding field size', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUint({ min: 2n ** 254n, max: 2n ** 256n - 1n }),
+          (value) => {
+            const bytes = bigIntToBytes(value);
+            try {
+              bytes32Simulator.fromBytes(bytes);
+              // Should have thrown an error
+              return false;
+            } catch {
+              // Expected behavior
+              return true;
+            }
+          }
+        ),
+        { numRuns: 500 }
+      );
+    });
+  });
+
+  describe('Comparison Properties', () => {
+    test('Equality is reflexive: a = a', () => {
+      fc.assert(
+        fc.property(
+          arbBytes32InField(),
+          (a) => {
+            return bytes32Simulator.eq(a, a);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Equality is symmetric: a = b implies b = a', () => {
+      fc.assert(
+        fc.property(
+          arbBytes32InField(),
+          arbBytes32InField(),
+          (a, b) => {
+            const eqAB = bytes32Simulator.eq(a, b);
+            const eqBA = bytes32Simulator.eq(b, a);
+            return eqAB === eqBA;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Equality is transitive: if a = b and b = c, then a = c', () => {
+      fc.assert(
+        fc.property(
+          arbBytes32InField(),
+          (a) => {
+            const b = new Uint8Array(a); // Copy of a
+            const c = new Uint8Array(a); // Another copy
+            
+            const eqAB = bytes32Simulator.eq(a, b);
+            const eqBC = bytes32Simulator.eq(b, c);
+            const eqAC = bytes32Simulator.eq(a, c);
+            
+            return (eqAB && eqBC) ? eqAC : true;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Less than is transitive: if a < b and b < c, then a < c', () => {
+      fc.assert(
+        fc.property(
+          arbBytes32InField(),
+          arbBytes32InField(),
+          arbBytes32InField(),
+          (a, b, c) => {
+            const ltAB = bytes32Simulator.lt(a, b);
+            const ltBC = bytes32Simulator.lt(b, c);
+            
+            if (ltAB && ltBC) {
+              return bytes32Simulator.lt(a, c);
+            }
+            return true;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Less than or equal is reflexive: a ≤ a', () => {
+      fc.assert(
+        fc.property(
+          arbBytes32InField(),
+          (a) => {
+            return bytes32Simulator.lte(a, a);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Greater than is inverse of less than: a > b = b < a', () => {
+      fc.assert(
+        fc.property(
+          arbBytes32InField(),
+          arbBytes32InField(),
+          (a, b) => {
+            const gtAB = bytes32Simulator.gt(a, b);
+            const ltBA = bytes32Simulator.lt(b, a);
+            return gtAB === ltBA;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Greater than or equal is inverse of less than: a ≥ b = not (a < b)', () => {
+      fc.assert(
+        fc.property(
+          arbBytes32InField(),
+          arbBytes32InField(),
+          (a, b) => {
+            const gteAB = bytes32Simulator.gte(a, b);
+            const ltAB = bytes32Simulator.lt(a, b);
+            return gteAB === !ltAB;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Trichotomy: exactly one of a < b, a = b, a > b is true', () => {
+      fc.assert(
+        fc.property(
+          arbBytes32InField(),
+          arbBytes32InField(),
+          (a, b) => {
+            const lt = bytes32Simulator.lt(a, b);
+            const eq = bytes32Simulator.eq(a, b);
+            const gt = bytes32Simulator.gt(a, b);
+            
+            const count = (lt ? 1 : 0) + (eq ? 1 : 0) + (gt ? 1 : 0);
+            return count === 1;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Consistency between comparison operators: a ≤ b ↔ (a < b or a = b)', () => {
+      fc.assert(
+        fc.property(
+          arbBytes32InField(),
+          arbBytes32InField(),
+          (a, b) => {
+            const lte = bytes32Simulator.lte(a, b);
+            const lt = bytes32Simulator.lt(a, b);
+            const eq = bytes32Simulator.eq(a, b);
+            
+            return lte === (lt || eq);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Ordering Properties', () => {
+    test('Anti-symmetry: if a ≤ b and b ≤ a, then a = b', () => {
+      fc.assert(
+        fc.property(
+          arbBytes32InField(),
+          arbBytes32InField(),
+          (a, b) => {
+            const lteAB = bytes32Simulator.lte(a, b);
+            const lteBA = bytes32Simulator.lte(b, a);
+            const eqAB = bytes32Simulator.eq(a, b);
+            
+            if (lteAB && lteBA) {
+              return eqAB;
+            }
+            return true;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Totality: for any a and b, either a ≤ b or b ≤ a', () => {
+      fc.assert(
+        fc.property(
+          arbBytes32InField(),
+          arbBytes32InField(),
+          (a, b) => {
+            const lteAB = bytes32Simulator.lte(a, b);
+            const lteBA = bytes32Simulator.lte(b, a);
+            return lteAB || lteBA;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Comparison consistency with field values', () => {
+      fc.assert(
+        fc.property(
+          arbBytes32InField(),
+          arbBytes32InField(),
+          (a, b) => {
+            const aValue = bytes32Simulator.fromBytes(a);
+            const bValue = bytes32Simulator.fromBytes(b);
+            
+            const ltBytes = bytes32Simulator.lt(a, b);
+            const ltValues = aValue < bValue;
+            
+            return ltBytes === ltValues;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Boundary and Edge Cases', () => {
+    test('Operations with zero bytes', () => {
+      fc.assert(
+        fc.property(
+          arbBytes32InField(),
+          (a) => {
+            const zero = new Uint8Array(32);
+            
+            // Comparisons with zero
+            const eqZero = bytes32Simulator.eq(zero, zero);
+            const lteZeroA = bytes32Simulator.lte(zero, a);
+            
+            return eqZero && lteZeroA;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Operations with maximum field value', () => {
+      fc.assert(
+        fc.property(
+          arbBytes32InField(),
+          (a) => {
+            const maxField = bigIntToBytes(MAX_FIELD254);
+            
+            // All values should be less than or equal to max
+            const lteMax = bytes32Simulator.lte(a, maxField);
+            
+            return lteMax;
+          }
+        ),
+        { numRuns: 500 }
+      );
+    });
+
+    test('Byte array structure preservation', () => {
+      fc.assert(
+        fc.property(
+          arbBytes32InField(),
+          (bytes) => {
+            // Verify array length is preserved
+            return bytes.length === 32;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Conversion handles all byte positions', () => {
+      fc.assert(
+        fc.property(
+          fc.integer({ min: 0, max: 31 }),
+          fc.integer({ min: 0, max: 255 }),
+          (position, value) => {
+            const bytes = new Uint8Array(32);
+            bytes[position] = value;
+            
+            // Should be within field bounds if small enough
+            if (position < 31 || value < 0x40) {
+              const field = bytes32Simulator.fromBytes(bytes);
+              return field >= 0n;
+            }
+            return true;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Little-endian byte order consistency', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUint({ max: MAX_FIELD254 }),
+          (value) => {
+            const bytes = bytes32Simulator.toBytes(value);
+            const reconstructed = bytesToBigInt(bytes);
+            return reconstructed === value;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Identity and Special Value Properties', () => {
+    test('Zero conversion consistency', () => {
+      fc.assert(
+        fc.property(
+          fc.constant(0n),
+          (zero) => {
+            const bytes = bytes32Simulator.toBytes(zero);
+            const field = bytes32Simulator.fromBytes(bytes);
+            return field === zero;
+          }
+        ),
+        { numRuns: 100 }
+      );
+    });
+
+    test('Powers of two conversion', () => {
+      fc.assert(
+        fc.property(
+          fc.integer({ min: 0, max: 253 }),
+          (exponent) => {
+            const value = 2n ** BigInt(exponent);
+            const bytes = bytes32Simulator.toBytes(value);
+            const reconstructed = bytes32Simulator.fromBytes(bytes);
+            return reconstructed === value;
+          }
+        ),
+        { numRuns: 254 }
+      );
+    });
+
+    test('Sequential values maintain ordering', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUint({ max: MAX_FIELD254 - 1n }),
+          (value) => {
+            const bytes1 = bytes32Simulator.toBytes(value);
+            const bytes2 = bytes32Simulator.toBytes(value + 1n);
+            
+            return bytes32Simulator.lt(bytes1, bytes2);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+});
diff --git a/contracts/math/src/test/Field254.fuzz.test.ts b/contracts/math/src/test/Field254.fuzz.test.ts
new file mode 100644
index 00000000..11553434
--- /dev/null
+++ b/contracts/math/src/test/Field254.fuzz.test.ts
@@ -0,0 +1,685 @@
+import { beforeEach, describe, test } from 'vitest';
+import * as fc from 'fast-check';
+import type { U256 } from '../artifacts/Index/contract/index.d.cts';
+import { FIELD_MODULUS, toU256, fromU256 } from '../utils/u256';
+import { Field254Simulator } from './Field254Simulator';
+
+let field254Simulator: Field254Simulator;
+
+const setup = () => {
+  field254Simulator = new Field254Simulator();
+};
+
+// Custom arbitrary for Field254 values (within 254-bit range)
+const arbField254 = (): fc.Arbitrary<bigint> => {
+  return fc.bigUint({ max: FIELD_MODULUS });
+};
+
+// Custom arbitrary for U256 within field constraints
+const arbU256InField = (): fc.Arbitrary<U256> => {
+  return fc.bigUint({ max: FIELD_MODULUS }).map((value) => toU256(value));
+};
+
+/**
+ * Property-based fuzz tests for Field254 operations
+ * Using fast-check for automated test case generation
+ */
+describe('Field254 - Property-Based Fuzz Tests', () => {
+  beforeEach(setup);
+
+  describe('Conversion Properties', () => {
+    test('fromField and toField are inverses', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          (value) => {
+            const u256 = field254Simulator.fromField(value);
+            const reconstructed = field254Simulator.toField(u256);
+            return reconstructed === value;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('toField and fromField are inverses for valid U256', () => {
+      fc.assert(
+        fc.property(
+          arbU256InField(),
+          (u256) => {
+            const field = field254Simulator.toField(u256);
+            const reconstructed = field254Simulator.fromField(field);
+            
+            const originalValue = fromU256(u256);
+            const reconstructedValue = fromU256(reconstructed);
+            
+            return originalValue === reconstructedValue;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('fromField produces valid U256 structure', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          (value) => {
+            const u256 = field254Simulator.fromField(value);
+            const reconstructedValue = fromU256(u256);
+            return reconstructedValue === value;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('toField rejects values exceeding 254 bits', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUint({ min: 2n ** 254n, max: 2n ** 256n - 1n }),
+          (value) => {
+            const u256 = toU256(value);
+            try {
+              field254Simulator.toField(u256);
+              // Should have thrown an error
+              return false;
+            } catch {
+              // Expected behavior
+              return true;
+            }
+          }
+        ),
+        { numRuns: 500 }
+      );
+    });
+  });
+
+  describe('Comparison Properties', () => {
+    test('Equality is reflexive: a = a', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          (a) => {
+            return field254Simulator.eq(a, a);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Equality is symmetric: a = b implies b = a', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          arbField254(),
+          (a, b) => {
+            const eqAB = field254Simulator.eq(a, b);
+            const eqBA = field254Simulator.eq(b, a);
+            return eqAB === eqBA;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Equality is transitive: if a = b and b = c, then a = c', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          arbField254(),
+          arbField254(),
+          (a, b, c) => {
+            const eqAB = field254Simulator.eq(a, b);
+            const eqBC = field254Simulator.eq(b, c);
+            const eqAC = field254Simulator.eq(a, c);
+            
+            if (eqAB && eqBC) {
+              return eqAC;
+            }
+            return true;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Less than is transitive: if a < b and b < c, then a < c', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          arbField254(),
+          arbField254(),
+          (a, b, c) => {
+            const ltAB = field254Simulator.lt(a, b);
+            const ltBC = field254Simulator.lt(b, c);
+            
+            if (ltAB && ltBC) {
+              return field254Simulator.lt(a, c);
+            }
+            return true;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Less than or equal is reflexive: a ≤ a', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          (a) => {
+            return field254Simulator.lte(a, a);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Greater than is inverse of less than: a > b = b < a', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          arbField254(),
+          (a, b) => {
+            const gtAB = field254Simulator.gt(a, b);
+            const ltBA = field254Simulator.lt(b, a);
+            return gtAB === ltBA;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Greater than or equal is inverse of less than: a ≥ b = not (a < b)', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          arbField254(),
+          (a, b) => {
+            const gteAB = field254Simulator.gte(a, b);
+            const ltAB = field254Simulator.lt(a, b);
+            return gteAB === !ltAB;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Trichotomy: exactly one of a < b, a = b, a > b is true', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          arbField254(),
+          (a, b) => {
+            const lt = field254Simulator.lt(a, b);
+            const eq = field254Simulator.eq(a, b);
+            const gt = field254Simulator.gt(a, b);
+            
+            const count = (lt ? 1 : 0) + (eq ? 1 : 0) + (gt ? 1 : 0);
+            return count === 1;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Consistency between comparison operators: a ≤ b ↔ (a < b or a = b)', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          arbField254(),
+          (a, b) => {
+            const lte = field254Simulator.lte(a, b);
+            const lt = field254Simulator.lt(a, b);
+            const eq = field254Simulator.eq(a, b);
+            
+            return lte === (lt || eq);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Arithmetic Properties', () => {
+    test('Addition commutativity: a + b = b + a', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          arbField254(),
+          (a, b) => {
+            const resultAB = field254Simulator.add(a, b);
+            const resultBA = field254Simulator.add(b, a);
+            return resultAB === resultBA;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Addition associativity: (a + b) + c = a + (b + c)', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          arbField254(),
+          arbField254(),
+          (a, b, c) => {
+            const resultLeft = field254Simulator.add(field254Simulator.add(a, b), c);
+            const resultRight = field254Simulator.add(a, field254Simulator.add(b, c));
+            return resultLeft === resultRight;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Addition identity: a + 0 = a', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          (a) => {
+            const result = field254Simulator.add(a, 0n);
+            return result === a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Subtraction inverse: (a + b) - b = a', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          arbField254(),
+          (a, b) => {
+            try {
+              const sum = field254Simulator.add(a, b);
+              const result = field254Simulator.sub(sum, b);
+              return result === a;
+            } catch {
+              // Overflow cases are acceptable
+              return true;
+            }
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Subtraction identity: a - 0 = a', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          (a) => {
+            const result = field254Simulator.sub(a, 0n);
+            return result === a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Self-subtraction: a - a = 0', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          (a) => {
+            const result = field254Simulator.sub(a, a);
+            return result === 0n;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Multiplication commutativity: a * b = b * a', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          arbField254(),
+          (a, b) => {
+            const resultAB = field254Simulator.mul(a, b);
+            const resultBA = field254Simulator.mul(b, a);
+            return resultAB === resultBA;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Multiplication associativity: (a * b) * c = a * (b * c)', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(84),
+          fc.bigUintN(84),
+          fc.bigUintN(84),
+          (a, b, c) => {
+            const resultLeft = field254Simulator.mul(field254Simulator.mul(a, b), c);
+            const resultRight = field254Simulator.mul(a, field254Simulator.mul(b, c));
+            return resultLeft === resultRight;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Multiplication identity: a * 1 = a', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          (a) => {
+            const result = field254Simulator.mul(a, 1n);
+            return result === a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Multiplication zero: a * 0 = 0', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          (a) => {
+            const result = field254Simulator.mul(a, 0n);
+            return result === 0n;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Distributivity: a * (b + c) = (a * b) + (a * c)', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(84),
+          fc.bigUintN(84),
+          fc.bigUintN(84),
+          (a, b, c) => {
+            try {
+              const left = field254Simulator.mul(a, field254Simulator.add(b, c));
+              const right = field254Simulator.add(
+                field254Simulator.mul(a, b),
+                field254Simulator.mul(a, c)
+              );
+              return left === right;
+            } catch {
+              // Overflow is acceptable
+              return true;
+            }
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Division by 1: a / 1 = a', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          (a) => {
+            const result = field254Simulator.div(a, 1n);
+            return result.quotient === a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Division by self: a / a = 1 (for non-zero a)', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          (a) => {
+            fc.pre(a > 0n);
+            const result = field254Simulator.div(a, a);
+            return result.quotient === 1n;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Zero dividend: 0 / a = 0 (for non-zero a)', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          (a) => {
+            fc.pre(a > 0n);
+            const result = field254Simulator.div(0n, a);
+            return result.quotient === 0n;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Division-modulo relationship: a = (a / b) * b + (a % b)', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          arbField254(),
+          (a, b) => {
+            fc.pre(b > 0n);
+            const divResult = field254Simulator.div(a, b);
+            const reconstructed = field254Simulator.add(
+              field254Simulator.mul(divResult.quotient, b),
+              divResult.remainder
+            );
+            return reconstructed === a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Remainder is always less than divisor: (a % b) < b', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          arbField254(),
+          (a, b) => {
+            fc.pre(b > 0n);
+            const divResult = field254Simulator.div(a, b);
+            return divResult.remainder < b;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('IsZero Properties', () => {
+    test('isZero is true only for zero', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          (a) => {
+            const result = field254Simulator.isZero(a);
+            return result === (a === 0n);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('isZero consistency with equality', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          (a) => {
+            const isZeroResult = field254Simulator.isZero(a);
+            const eqZeroResult = field254Simulator.eq(a, 0n);
+            return isZeroResult === eqZeroResult;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Boundary and Edge Cases', () => {
+    test('Operations with FIELD_MODULUS', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          (a) => {
+            // Comparison with field modulus
+            const ltResult = field254Simulator.lte(a, FIELD_MODULUS);
+            
+            // Should complete without error
+            return ltResult;
+          }
+        ),
+        { numRuns: 500 }
+      );
+    });
+
+    test('Operations with zero', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          (a) => {
+            // Add zero
+            const addZero = field254Simulator.add(a, 0n);
+            // Multiply by zero
+            const mulZero = field254Simulator.mul(a, 0n);
+            // Subtract zero
+            const subZero = field254Simulator.sub(a, 0n);
+            
+            return addZero === a && mulZero === 0n && subZero === a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Operations with one', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          (a) => {
+            // Multiply by one
+            const mulOne = field254Simulator.mul(a, 1n);
+            // Divide by one (if non-zero)
+            const divOne = a > 0n ? field254Simulator.div(a, 1n).quotient : 0n;
+            
+            return mulOne === a && (a === 0n || divOne === a);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Powers of two', () => {
+      fc.assert(
+        fc.property(
+          fc.integer({ min: 0, max: 253 }),
+          (exponent) => {
+            const value = 2n ** BigInt(exponent);
+            const u256 = field254Simulator.fromField(value);
+            const reconstructed = field254Simulator.toField(u256);
+            return reconstructed === value;
+          }
+        ),
+        { numRuns: 254 }
+      );
+    });
+
+    test('Sequential values maintain ordering', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUint({ max: FIELD_MODULUS - 1n }),
+          (value) => {
+            return field254Simulator.lt(value, value + 1n);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Conversion preserves value within field range', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          (value) => {
+            fc.pre(value <= FIELD_MODULUS);
+            const u256 = field254Simulator.fromField(value);
+            const converted = field254Simulator.toField(u256);
+            return converted === value;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Ordering Properties', () => {
+    test('Anti-symmetry: if a ≤ b and b ≤ a, then a = b', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          arbField254(),
+          (a, b) => {
+            const lteAB = field254Simulator.lte(a, b);
+            const lteBA = field254Simulator.lte(b, a);
+            const eqAB = field254Simulator.eq(a, b);
+            
+            if (lteAB && lteBA) {
+              return eqAB;
+            }
+            return true;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Totality: for any a and b, either a ≤ b or b ≤ a', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          arbField254(),
+          (a, b) => {
+            const lteAB = field254Simulator.lte(a, b);
+            const lteBA = field254Simulator.lte(b, a);
+            return lteAB || lteBA;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Less than is irreflexive: not (a < a)', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          (a) => {
+            return !field254Simulator.lt(a, a);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Less than is asymmetric: if a < b, then not (b < a)', () => {
+      fc.assert(
+        fc.property(
+          arbField254(),
+          arbField254(),
+          (a, b) => {
+            const ltAB = field254Simulator.lt(a, b);
+            const ltBA = field254Simulator.lt(b, a);
+            
+            if (ltAB) {
+              return !ltBA;
+            }
+            return true;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+});
diff --git a/contracts/math/src/test/Uint128.fuzz.test.ts b/contracts/math/src/test/Uint128.fuzz.test.ts
new file mode 100644
index 00000000..1bfaed73
--- /dev/null
+++ b/contracts/math/src/test/Uint128.fuzz.test.ts
@@ -0,0 +1,628 @@
+import { beforeEach, describe, test } from 'vitest';
+import * as fc from 'fast-check';
+import type { U128 } from '../artifacts/Index/contract/index.d.cts';
+import { MAX_UINT64, MAX_UINT128 } from '../utils/consts';
+import { Uint128Simulator } from './Uint128Simulator';
+
+let uint128Simulator: Uint128Simulator;
+
+const setup = () => {
+  uint128Simulator = new Uint128Simulator();
+};
+
+// Custom arbitraries for U128 structure
+const arbU128 = (): fc.Arbitrary<U128> => {
+  return fc.record({
+    low: fc.bigUintN(64),
+    high: fc.bigUintN(64),
+  });
+};
+
+// Arbitrary for Uint<128> values
+const arbUint128 = (): fc.Arbitrary<bigint> => {
+  return fc.bigUint({ max: MAX_UINT128 });
+};
+
+/**
+ * Property-based fuzz tests for Uint128 operations
+ * Using fast-check for automated test case generation
+ */
+describe('Uint128 - Property-Based Fuzz Tests', () => {
+  beforeEach(setup);
+
+  describe('Conversion Properties', () => {
+    test('toU128 and fromU128 are inverses', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          (value) => {
+            const u128 = uint128Simulator.toU128(value);
+            const reconstructed = uint128Simulator.fromU128(u128);
+            return reconstructed === value;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('fromU128 and toU128 are inverses', () => {
+      fc.assert(
+        fc.property(
+          arbU128(),
+          (u128) => {
+            const value = uint128Simulator.fromU128(u128);
+            const reconstructed = uint128Simulator.toU128(value);
+            return reconstructed.low === u128.low && reconstructed.high === u128.high;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('toU128 produces valid low and high components', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          (value) => {
+            const u128 = uint128Simulator.toU128(value);
+            return u128.low <= MAX_UINT64 && u128.high <= MAX_UINT64;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Addition Properties', () => {
+    test('Commutativity: a + b = b + a', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          arbUint128(),
+          (a, b) => {
+            const resultAB = uint128Simulator.add(a, b);
+            const resultBA = uint128Simulator.add(b, a);
+            return resultAB === resultBA;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Associativity: (a + b) + c = a + (b + c)', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          arbUint128(),
+          arbUint128(),
+          (a, b, c) => {
+            const resultLeft = uint128Simulator.add(uint128Simulator.add(a, b), c);
+            const resultRight = uint128Simulator.add(a, uint128Simulator.add(b, c));
+            return resultLeft === resultRight;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Identity: a + 0 = a', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          (a) => {
+            const result = uint128Simulator.add(a, 0n);
+            return result === a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('U128 Addition commutativity: a + b = b + a', () => {
+      fc.assert(
+        fc.property(
+          arbU128(),
+          arbU128(),
+          (a, b) => {
+            const resultAB = uint128Simulator.addU128(a, b);
+            const resultBA = uint128Simulator.addU128(b, a);
+            return resultAB.low === resultBA.low && resultAB.high === resultBA.high;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Subtraction Properties', () => {
+    test('Inverse of addition: (a + b) - b = a', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUint({ max: MAX_UINT128 / 2n }),
+          fc.bigUint({ max: MAX_UINT128 / 2n }),
+          (a, b) => {
+            const sum = uint128Simulator.add(a, b);
+            const result = uint128Simulator.sub(sum, b);
+            return result === a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Identity: a - 0 = a', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          (a) => {
+            const result = uint128Simulator.sub(a, 0n);
+            return result === a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Self-subtraction: a - a = 0', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          (a) => {
+            const result = uint128Simulator.sub(a, a);
+            return result === 0n;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('U128 Subtraction inverse: (a + b) - b = a', () => {
+      fc.assert(
+        fc.property(
+          arbU128(),
+          arbU128(),
+          (a, b) => {
+            try {
+              const sum = uint128Simulator.addU128(a, b);
+              const result = uint128Simulator.subU128(sum, b);
+              return result.low === a.low && result.high === a.high;
+            } catch {
+              // Overflow cases are acceptable
+              return true;
+            }
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Multiplication Properties', () => {
+    test('Commutativity: a * b = b * a', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          arbUint128(),
+          (a, b) => {
+            const resultAB = uint128Simulator.mul(a, b);
+            const resultBA = uint128Simulator.mul(b, a);
+            return resultAB === resultBA;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Associativity: (a * b) * c = a * (b * c)', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(42),
+          fc.bigUintN(42),
+          fc.bigUintN(42),
+          (a, b, c) => {
+            const resultLeft = uint128Simulator.mul(uint128Simulator.mul(a, b), c);
+            const resultRight = uint128Simulator.mul(a, uint128Simulator.mul(b, c));
+            return resultLeft === resultRight;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Identity: a * 1 = a', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          (a) => {
+            const result = uint128Simulator.mul(a, 1n);
+            return result === a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Zero property: a * 0 = 0', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          (a) => {
+            const result = uint128Simulator.mul(a, 0n);
+            return result === 0n;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Distributivity: a * (b + c) = (a * b) + (a * c)', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(42),
+          fc.bigUintN(42),
+          fc.bigUintN(42),
+          (a, b, c) => {
+            const left = uint128Simulator.mul(a, uint128Simulator.add(b, c));
+            const right = uint128Simulator.add(
+              uint128Simulator.mul(a, b),
+              uint128Simulator.mul(a, c)
+            );
+            return left === right;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('U128 Multiplication commutativity: a * b = b * a', () => {
+      fc.assert(
+        fc.property(
+          arbU128(),
+          arbU128(),
+          (a, b) => {
+            const resultAB = uint128Simulator.mulU128(a, b);
+            const resultBA = uint128Simulator.mulU128(b, a);
+            return (
+              resultAB.low === resultBA.low &&
+              resultAB.high === resultBA.high &&
+              resultAB.overflow === resultBA.overflow
+            );
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Division Properties', () => {
+    test('Division by 1: a / 1 = a', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          (a) => {
+            const result = uint128Simulator.div(a, 1n);
+            return result === a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Division by self: a / a = 1 (for non-zero a)', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          (a) => {
+            fc.pre(a > 0n);
+            const result = uint128Simulator.div(a, a);
+            return result === 1n;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Zero dividend: 0 / a = 0 (for non-zero a)', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          (a) => {
+            fc.pre(a > 0n);
+            const result = uint128Simulator.div(0n, a);
+            return result === 0n;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Division is less than or equal to dividend: a / b ≤ a (for b ≥ 1)', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          arbUint128(),
+          (a, b) => {
+            fc.pre(b > 0n);
+            const result = uint128Simulator.div(a, b);
+            return result <= a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Multiplication-division relationship: (a * b) / b = a (for non-zero b, no overflow)', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          fc.bigUintN(64),
+          (a, b) => {
+            fc.pre(b > 0n);
+            const product = uint128Simulator.mul(a, b);
+            const result = uint128Simulator.div(product, b);
+            return result === a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('U128 Division quotient validity: (a / b) * b + (a % b) = a', () => {
+      fc.assert(
+        fc.property(
+          arbU128(),
+          arbU128(),
+          (a, b) => {
+            const bValue = uint128Simulator.fromU128(b);
+            fc.pre(bValue > 0n);
+            
+            const divResult = uint128Simulator.divU128(a, b);
+            const quotientValue = uint128Simulator.fromU128(divResult.quotient);
+            const remainderValue = uint128Simulator.fromU128(divResult.remainder);
+            const aValue = uint128Simulator.fromU128(a);
+            
+            const reconstructed = quotientValue * bValue + remainderValue;
+            return reconstructed === aValue;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Modulo Properties', () => {
+    test('Modulo is always less than divisor: a % b < b (for non-zero b)', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          arbUint128(),
+          (a, b) => {
+            fc.pre(b > 0n);
+            const result = uint128Simulator.mod(a, b);
+            return result < b;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Division-modulo relationship: a = (a / b) * b + (a % b)', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          arbUint128(),
+          (a, b) => {
+            fc.pre(b > 0n);
+            const quotient = uint128Simulator.div(a, b);
+            const remainder = uint128Simulator.mod(a, b);
+            const reconstructed = uint128Simulator.add(
+              uint128Simulator.mul(quotient, b),
+              remainder
+            );
+            return reconstructed === a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Modulo by 1: a % 1 = 0', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          (a) => {
+            const result = uint128Simulator.mod(a, 1n);
+            return result === 0n;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Modulo by self: a % a = 0 (for non-zero a)', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          (a) => {
+            fc.pre(a > 0n);
+            const result = uint128Simulator.mod(a, a);
+            return result === 0n;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Comparison Properties', () => {
+    test('Less than is transitive: if a < b and b < c, then a < c', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          arbUint128(),
+          arbUint128(),
+          (a, b, c) => {
+            fc.pre(a < b && b < c);
+            return uint128Simulator.lt(a, c);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Less than or equal is reflexive: a ≤ a', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          (a) => {
+            return uint128Simulator.lte(a, a);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Equality is symmetric: a = b implies b = a', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          (a) => {
+            return uint128Simulator.eq(a, a);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Greater than is inverse of less than: a > b = b < a', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          arbUint128(),
+          (a, b) => {
+            const gtResult = uint128Simulator.gt(a, b);
+            const ltResult = uint128Simulator.lt(b, a);
+            return gtResult === ltResult;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('U128 Less than is transitive', () => {
+      fc.assert(
+        fc.property(
+          arbU128(),
+          arbU128(),
+          arbU128(),
+          (a, b, c) => {
+            const aVal = uint128Simulator.fromU128(a);
+            const bVal = uint128Simulator.fromU128(b);
+            const cVal = uint128Simulator.fromU128(c);
+            
+            fc.pre(aVal < bVal && bVal < cVal);
+            return uint128Simulator.ltU128(a, c);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('IsZero Properties', () => {
+    test('isZero is true only for zero', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          (a) => {
+            const result = uint128Simulator.isZero(a);
+            return result === (a === 0n);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('isZeroU128 is true only for zero U128', () => {
+      fc.assert(
+        fc.property(
+          arbU128(),
+          (a) => {
+            const result = uint128Simulator.isZeroU128(a);
+            const value = uint128Simulator.fromU128(a);
+            return result === (value === 0n);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Boundary and Edge Cases', () => {
+    test('Operations with MAX_UINT128', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          (a) => {
+            // Multiplication with MAX_UINT128 (may overflow)
+            const mulResult = uint128Simulator.mul(a, MAX_UINT128);
+            
+            // Division by MAX_UINT128
+            const divResult = uint128Simulator.div(a, MAX_UINT128);
+            
+            // Should complete without error
+            return true;
+          }
+        ),
+        { numRuns: 500 }
+      );
+    });
+
+    test('Operations with zero', () => {
+      fc.assert(
+        fc.property(
+          arbUint128(),
+          (a) => {
+            // Add zero
+            const addZero = uint128Simulator.add(a, 0n);
+            // Multiply by zero
+            const mulZero = uint128Simulator.mul(a, 0n);
+            
+            return addZero === a && mulZero === 0n;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Operations with MAX_UINT64 boundaries', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          fc.bigUintN(64),
+          (a, b) => {
+            // Should handle 64-bit values gracefully
+            const sum = uint128Simulator.add(a, b);
+            const product = uint128Simulator.mul(a, b);
+            
+            return sum >= a && sum >= b && product >= 0n;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('U128 structure validation', () => {
+      fc.assert(
+        fc.property(
+          arbU128(),
+          (u128) => {
+            // Verify components are within valid range
+            return u128.low <= MAX_UINT64 && u128.high <= MAX_UINT64;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+});
diff --git a/contracts/math/src/test/Uint256.fuzz.test.ts b/contracts/math/src/test/Uint256.fuzz.test.ts
new file mode 100644
index 00000000..d7aa9ce3
--- /dev/null
+++ b/contracts/math/src/test/Uint256.fuzz.test.ts
@@ -0,0 +1,634 @@
+import { beforeEach, describe, test } from 'vitest';
+import * as fc from 'fast-check';
+import type { U256 } from '../artifacts/Index/contract/index.d.cts';
+import { MAX_UINT64, MAX_UINT128, MAX_UINT256 } from '../utils/consts';
+import { Uint256Simulator } from './Uint256Simulator';
+
+let uint256Simulator: Uint256Simulator;
+
+const setup = () => {
+  uint256Simulator = new Uint256Simulator();
+};
+
+// Maximum value that fits in 254 bits
+const MAX_UINT254 = 2n ** 254n - 1n;
+
+// Custom arbitrary for U256 structure
+const arbU256 = (): fc.Arbitrary<U256> => {
+  return fc.record({
+    low: fc.record({
+      low: fc.bigUintN(64),
+      high: fc.bigUintN(64),
+    }),
+    high: fc.record({
+      low: fc.bigUintN(64),
+      high: fc.bigUintN(64),
+    }),
+  });
+};
+
+// Arbitrary for Uint<256> values (limited to 254 bits as per contract constraints)
+const arbUint256 = (): fc.Arbitrary<bigint> => {
+  return fc.bigUint({ max: MAX_UINT254 });
+};
+
+// Helper to convert bigint to U256
+const toU256Helper = (value: bigint): U256 => {
+  const lowBigInt = value & ((1n << 128n) - 1n);
+  const highBigInt = value >> 128n;
+  return {
+    low: { low: lowBigInt & MAX_UINT64, high: lowBigInt >> 64n },
+    high: { low: highBigInt & MAX_UINT64, high: highBigInt >> 64n },
+  };
+};
+
+// Helper to convert U256 to bigint
+const fromU256Helper = (value: U256): bigint => {
+  return (
+    (value.high.high << 192n) +
+    (value.high.low << 128n) +
+    (value.low.high << 64n) +
+    value.low.low
+  );
+};
+
+/**
+ * Property-based fuzz tests for Uint256 operations
+ * Using fast-check for automated test case generation
+ */
+describe('Uint256 - Property-Based Fuzz Tests', () => {
+  beforeEach(setup);
+
+  describe('Conversion Properties', () => {
+    test('toU256 and fromU256 are inverses', () => {
+      fc.assert(
+        fc.property(
+          arbUint256(),
+          (value) => {
+            const u256 = uint256Simulator.toU256(value);
+            const reconstructed = uint256Simulator.fromU256(u256);
+            return reconstructed === value;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('fromU256 and toU256 are inverses for valid U256', () => {
+      fc.assert(
+        fc.property(
+          arbUint256(),
+          (value) => {
+            const u256 = toU256Helper(value);
+            const extracted = uint256Simulator.fromU256(u256);
+            const reconstructed = uint256Simulator.toU256(extracted);
+            
+            return (
+              reconstructed.low.low === u256.low.low &&
+              reconstructed.low.high === u256.low.high &&
+              reconstructed.high.low === u256.high.low &&
+              reconstructed.high.high === u256.high.high
+            );
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('toU256 produces valid component bounds', () => {
+      fc.assert(
+        fc.property(
+          arbUint256(),
+          (value) => {
+            const u256 = uint256Simulator.toU256(value);
+            return (
+              u256.low.low <= MAX_UINT64 &&
+              u256.low.high <= MAX_UINT64 &&
+              u256.high.low <= MAX_UINT64 &&
+              u256.high.high <= MAX_UINT64
+            );
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Addition Properties', () => {
+    test('Commutativity: a + b = b + a', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          arbU256(),
+          (a, b) => {
+            const resultAB = uint256Simulator.add(a, b);
+            const resultBA = uint256Simulator.add(b, a);
+            return (
+              resultAB.low.low === resultBA.low.low &&
+              resultAB.low.high === resultBA.low.high &&
+              resultAB.high.low === resultBA.high.low &&
+              resultAB.high.high === resultBA.high.high
+            );
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Associativity: (a + b) + c = a + (b + c)', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          arbU256(),
+          arbU256(),
+          (a, b, c) => {
+            const resultLeft = uint256Simulator.add(uint256Simulator.add(a, b), c);
+            const resultRight = uint256Simulator.add(a, uint256Simulator.add(b, c));
+            return (
+              resultLeft.low.low === resultRight.low.low &&
+              resultLeft.low.high === resultRight.low.high &&
+              resultLeft.high.low === resultRight.high.low &&
+              resultLeft.high.high === resultRight.high.high
+            );
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Identity: a + 0 = a', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          (a) => {
+            const zero = uint256Simulator.ZERO_U256();
+            const result = uint256Simulator.add(a, zero);
+            return (
+              result.low.low === a.low.low &&
+              result.low.high === a.low.high &&
+              result.high.low === a.high.low &&
+              result.high.high === a.high.high
+            );
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Subtraction Properties', () => {
+    test('Inverse of addition: (a + b) - b = a', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          arbU256(),
+          (a, b) => {
+            try {
+              const sum = uint256Simulator.add(a, b);
+              const result = uint256Simulator.sub(sum, b);
+              return (
+                result.low.low === a.low.low &&
+                result.low.high === a.low.high &&
+                result.high.low === a.high.low &&
+                result.high.high === a.high.high
+              );
+            } catch {
+              // Overflow cases are acceptable
+              return true;
+            }
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Identity: a - 0 = a', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          (a) => {
+            const zero = uint256Simulator.ZERO_U256();
+            const result = uint256Simulator.sub(a, zero);
+            return (
+              result.low.low === a.low.low &&
+              result.low.high === a.low.high &&
+              result.high.low === a.high.low &&
+              result.high.high === a.high.high
+            );
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Self-subtraction: a - a = 0', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          (a) => {
+            const result = uint256Simulator.sub(a, a);
+            const zero = uint256Simulator.ZERO_U256();
+            return (
+              result.low.low === zero.low.low &&
+              result.low.high === zero.low.high &&
+              result.high.low === zero.high.low &&
+              result.high.high === zero.high.high
+            );
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Multiplication Properties', () => {
+    test('Commutativity: a * b = b * a', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          arbU256(),
+          (a, b) => {
+            const resultAB = uint256Simulator.mul(a, b);
+            const resultBA = uint256Simulator.mul(b, a);
+            return (
+              resultAB.low.low === resultBA.low.low &&
+              resultAB.low.high === resultBA.low.high &&
+              resultAB.high.low === resultBA.high.low &&
+              resultAB.high.high === resultBA.high.high &&
+              resultAB.overflow === resultBA.overflow
+            );
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Identity: a * 1 = a', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          (a) => {
+            const one = toU256Helper(1n);
+            const result = uint256Simulator.mul(a, one);
+            return (
+              result.low.low === a.low.low &&
+              result.low.high === a.low.high &&
+              result.high.low === a.high.low &&
+              result.high.high === a.high.high
+            );
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Zero property: a * 0 = 0', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          (a) => {
+            const zero = uint256Simulator.ZERO_U256();
+            const result = uint256Simulator.mul(a, zero);
+            return (
+              result.low.low === zero.low.low &&
+              result.low.high === zero.low.high &&
+              result.high.low === zero.high.low &&
+              result.high.high === zero.high.high
+            );
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Distributivity: a * (b + c) = (a * b) + (a * c) when no overflow', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(84),
+          fc.bigUintN(84),
+          fc.bigUintN(84),
+          (aVal, bVal, cVal) => {
+            const a = toU256Helper(aVal);
+            const b = toU256Helper(bVal);
+            const c = toU256Helper(cVal);
+            
+            try {
+              const left = uint256Simulator.mul(a, uint256Simulator.add(b, c));
+              const right = uint256Simulator.add(
+                uint256Simulator.mul(a, b),
+                uint256Simulator.mul(a, c)
+              );
+              
+              return (
+                left.low.low === right.low.low &&
+                left.low.high === right.low.high &&
+                left.high.low === right.high.low &&
+                left.high.high === right.high.high
+              );
+            } catch {
+              // Overflow is acceptable
+              return true;
+            }
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Division Properties', () => {
+    test('Division by 1: a / 1 = a', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          (a) => {
+            const one = toU256Helper(1n);
+            const result = uint256Simulator.div(a, one);
+            return (
+              result.quotient.low.low === a.low.low &&
+              result.quotient.low.high === a.low.high &&
+              result.quotient.high.low === a.high.low &&
+              result.quotient.high.high === a.high.high
+            );
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Division by self: a / a = 1 (for non-zero a)', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          (a) => {
+            const aVal = fromU256Helper(a);
+            fc.pre(aVal > 0n);
+            
+            const result = uint256Simulator.div(a, a);
+            const one = toU256Helper(1n);
+            return (
+              result.quotient.low.low === one.low.low &&
+              result.quotient.low.high === one.low.high &&
+              result.quotient.high.low === one.high.low &&
+              result.quotient.high.high === one.high.high
+            );
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Zero dividend: 0 / a = 0 (for non-zero a)', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          (a) => {
+            const aVal = fromU256Helper(a);
+            fc.pre(aVal > 0n);
+            
+            const zero = uint256Simulator.ZERO_U256();
+            const result = uint256Simulator.div(zero, a);
+            return (
+              result.quotient.low.low === zero.low.low &&
+              result.quotient.low.high === zero.low.high &&
+              result.quotient.high.low === zero.high.low &&
+              result.quotient.high.high === zero.high.high
+            );
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Division quotient-remainder relationship: a = (a / b) * b + (a % b)', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          arbU256(),
+          (a, b) => {
+            const bVal = fromU256Helper(b);
+            fc.pre(bVal > 0n);
+            
+            const divResult = uint256Simulator.div(a, b);
+            const quotient = divResult.quotient;
+            const remainder = divResult.remainder;
+            
+            const mulResult = uint256Simulator.mul(quotient, b);
+            const reconstructed = uint256Simulator.add(mulResult, remainder);
+            
+            return (
+              reconstructed.low.low === a.low.low &&
+              reconstructed.low.high === a.low.high &&
+              reconstructed.high.low === a.high.low &&
+              reconstructed.high.high === a.high.high
+            );
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Remainder is always less than divisor: (a % b) < b', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          arbU256(),
+          (a, b) => {
+            const bVal = fromU256Helper(b);
+            fc.pre(bVal > 0n);
+            
+            const divResult = uint256Simulator.div(a, b);
+            const remainderVal = fromU256Helper(divResult.remainder);
+            
+            return remainderVal < bVal;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Comparison Properties', () => {
+    test('Equality is reflexive: a = a', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          (a) => {
+            return uint256Simulator.eq(a, a);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Equality is symmetric: a = b implies b = a', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          arbU256(),
+          (a, b) => {
+            const eqAB = uint256Simulator.eq(a, b);
+            const eqBA = uint256Simulator.eq(b, a);
+            return eqAB === eqBA;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Less than is transitive: if a < b and b < c, then a < c', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          arbU256(),
+          arbU256(),
+          (a, b, c) => {
+            const ltAB = uint256Simulator.lt(a, b);
+            const ltBC = uint256Simulator.lt(b, c);
+            
+            if (ltAB && ltBC) {
+              return uint256Simulator.lt(a, c);
+            }
+            return true;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Less than or equal is reflexive: a ≤ a', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          (a) => {
+            return uint256Simulator.lte(a, a);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Greater than is inverse of less than: a > b = b < a', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          arbU256(),
+          (a, b) => {
+            const gtAB = uint256Simulator.gt(a, b);
+            const ltBA = uint256Simulator.lt(b, a);
+            return gtAB === ltBA;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Trichotomy: exactly one of a < b, a = b, a > b is true', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          arbU256(),
+          (a, b) => {
+            const lt = uint256Simulator.lt(a, b);
+            const eq = uint256Simulator.eq(a, b);
+            const gt = uint256Simulator.gt(a, b);
+            
+            const count = (lt ? 1 : 0) + (eq ? 1 : 0) + (gt ? 1 : 0);
+            return count === 1;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Boundary and Edge Cases', () => {
+    test('Operations with MAX_UINT254', () => {
+      fc.assert(
+        fc.property(
+          arbUint256(),
+          (a) => {
+            const aU256 = toU256Helper(a);
+            const maxU256 = toU256Helper(MAX_UINT254);
+            
+            // Division by MAX_UINT254
+            const divResult = uint256Simulator.div(aU256, maxU256);
+            
+            // Comparison with MAX_UINT254
+            const ltResult = uint256Simulator.lte(aU256, maxU256);
+            
+            // Should complete without error
+            return true;
+          }
+        ),
+        { numRuns: 500 }
+      );
+    });
+
+    test('Operations with zero', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          (a) => {
+            const zero = uint256Simulator.ZERO_U256();
+            
+            // Add zero
+            const addZero = uint256Simulator.add(a, zero);
+            // Multiply by zero
+            const mulZero = uint256Simulator.mul(a, zero);
+            
+            const addResult = (
+              addZero.low.low === a.low.low &&
+              addZero.low.high === a.low.high &&
+              addZero.high.low === a.high.low &&
+              addZero.high.high === a.high.high
+            );
+            
+            const mulResult = (
+              mulZero.low.low === zero.low.low &&
+              mulZero.low.high === zero.low.high &&
+              mulZero.high.low === zero.high.low &&
+              mulZero.high.high === zero.high.high
+            );
+            
+            return addResult && mulResult;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('U256 structure validation', () => {
+      fc.assert(
+        fc.property(
+          arbU256(),
+          (u256) => {
+            // Verify all components are within valid range
+            return (
+              u256.low.low <= MAX_UINT64 &&
+              u256.low.high <= MAX_UINT64 &&
+              u256.high.low <= MAX_UINT64 &&
+              u256.high.high <= MAX_UINT64
+            );
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Conversion preserves value within 254-bit range', () => {
+      fc.assert(
+        fc.property(
+          arbUint256(),
+          (value) => {
+            fc.pre(value <= MAX_UINT254);
+            const u256 = uint256Simulator.toU256(value);
+            const converted = uint256Simulator.fromU256(u256);
+            return converted === value;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+});
diff --git a/contracts/math/src/test/Uint64.fuzz.test.ts b/contracts/math/src/test/Uint64.fuzz.test.ts
new file mode 100644
index 00000000..17e73fcf
--- /dev/null
+++ b/contracts/math/src/test/Uint64.fuzz.test.ts
@@ -0,0 +1,472 @@
+import { beforeEach, describe, test } from 'vitest';
+import * as fc from 'fast-check';
+import { MAX_UINT32, MAX_UINT64 } from '../utils/consts';
+import { Uint64Simulator } from './Uint64Simulator';
+
+let uint64Simulator: Uint64Simulator;
+
+const setup = () => {
+  uint64Simulator = new Uint64Simulator();
+};
+
+/**
+ * Property-based fuzz tests for Uint64 operations
+ * Using fast-check for automated test case generation
+ */
+describe('Uint64 - Property-Based Fuzz Tests', () => {
+  beforeEach(setup);
+
+  describe('Addition Properties', () => {
+    test('Commutativity: a + b = b + a', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          fc.bigUintN(64),
+          (a, b) => {
+            const resultAB = uint64Simulator.add(a, b);
+            const resultBA = uint64Simulator.add(b, a);
+            return resultAB === resultBA;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Associativity: (a + b) + c = a + (b + c)', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          fc.bigUintN(64),
+          fc.bigUintN(64),
+          (a, b, c) => {
+            const resultLeft = uint64Simulator.add(uint64Simulator.add(a, b), c);
+            const resultRight = uint64Simulator.add(a, uint64Simulator.add(b, c));
+            return resultLeft === resultRight;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Identity: a + 0 = a', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          (a) => {
+            const result = uint64Simulator.add(a, 0n);
+            return result === a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Addition is monotonic: if a < b, then a + c < b + c (when no overflow)', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(63), // Use smaller values to avoid overflow
+          fc.bigUintN(63),
+          fc.bigUintN(63),
+          (a, b, c) => {
+            fc.pre(a < b); // Precondition
+            const resultA = uint64Simulator.add(a, c);
+            const resultB = uint64Simulator.add(b, c);
+            return resultA < resultB;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Subtraction Properties', () => {
+    test('Inverse of addition: (a + b) - b = a', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(63),
+          fc.bigUintN(63),
+          (a, b) => {
+            const sum = uint64Simulator.add(a, b);
+            const result = uint64Simulator.sub(sum, b);
+            return result === a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Identity: a - 0 = a', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          (a) => {
+            const result = uint64Simulator.sub(a, 0n);
+            return result === a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Self-subtraction: a - a = 0', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          (a) => {
+            const result = uint64Simulator.sub(a, a);
+            return result === 0n;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Anti-commutativity fails for non-equal values: a - b ≠ b - a when a ≠ b', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          fc.bigUintN(64),
+          (a, b) => {
+            fc.pre(a !== b && a >= b && b <= a); // Ensure no underflow
+            try {
+              const resultAB = uint64Simulator.sub(a, b);
+              const resultBA = uint64Simulator.sub(b, a);
+              return resultAB !== resultBA || a === b;
+            } catch {
+              // Expected for underflow cases
+              return true;
+            }
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Multiplication Properties', () => {
+    test('Commutativity: a * b = b * a', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          fc.bigUintN(64),
+          (a, b) => {
+            const resultAB = uint64Simulator.mul(a, b);
+            const resultBA = uint64Simulator.mul(b, a);
+            return resultAB === resultBA;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Associativity: (a * b) * c = a * (b * c)', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(32),
+          fc.bigUintN(32),
+          fc.bigUintN(32),
+          (a, b, c) => {
+            const resultLeft = uint64Simulator.mul(uint64Simulator.mul(a, b), c);
+            const resultRight = uint64Simulator.mul(a, uint64Simulator.mul(b, c));
+            return resultLeft === resultRight;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Identity: a * 1 = a', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          (a) => {
+            const result = uint64Simulator.mul(a, 1n);
+            return result === a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Zero property: a * 0 = 0', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          (a) => {
+            const result = uint64Simulator.mul(a, 0n);
+            return result === 0n;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Distributivity: a * (b + c) = (a * b) + (a * c)', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(32),
+          fc.bigUintN(32),
+          fc.bigUintN(32),
+          (a, b, c) => {
+            const left = uint64Simulator.mul(a, uint64Simulator.add(b, c));
+            const right = uint64Simulator.add(
+              uint64Simulator.mul(a, b),
+              uint64Simulator.mul(a, c)
+            );
+            return left === right;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Division Properties', () => {
+    test('Division by 1: a / 1 = a', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          (a) => {
+            const result = uint64Simulator.div(a, 1n);
+            return result === a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Division by self: a / a = 1 (for non-zero a)', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          (a) => {
+            fc.pre(a > 0n);
+            const result = uint64Simulator.div(a, a);
+            return result === 1n;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Zero dividend: 0 / a = 0 (for non-zero a)', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          (a) => {
+            fc.pre(a > 0n);
+            const result = uint64Simulator.div(0n, a);
+            return result === 0n;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Division is less than or equal to dividend: a / b ≤ a (for b ≥ 1)', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          fc.bigUintN(64),
+          (a, b) => {
+            fc.pre(b > 0n);
+            const result = uint64Simulator.div(a, b);
+            return result <= a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Multiplication-division relationship: (a * b) / b = a (for non-zero b, no overflow)', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(32),
+          fc.bigUintN(32),
+          (a, b) => {
+            fc.pre(b > 0n);
+            const product = uint64Simulator.mul(a, b);
+            const result = uint64Simulator.div(product, b);
+            return result === a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Modulo Properties', () => {
+    test('Modulo is always less than divisor: a % b < b (for non-zero b)', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          fc.bigUintN(64),
+          (a, b) => {
+            fc.pre(b > 0n);
+            const result = uint64Simulator.mod(a, b);
+            return result < b;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Division-modulo relationship: a = (a / b) * b + (a % b)', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          fc.bigUintN(64),
+          (a, b) => {
+            fc.pre(b > 0n);
+            const quotient = uint64Simulator.div(a, b);
+            const remainder = uint64Simulator.mod(a, b);
+            const reconstructed = uint64Simulator.add(
+              uint64Simulator.mul(quotient, b),
+              remainder
+            );
+            return reconstructed === a;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Modulo by 1: a % 1 = 0', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          (a) => {
+            const result = uint64Simulator.mod(a, 1n);
+            return result === 0n;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Modulo by self: a % a = 0 (for non-zero a)', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          (a) => {
+            fc.pre(a > 0n);
+            const result = uint64Simulator.mod(a, a);
+            return result === 0n;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Comparison Properties', () => {
+    test('Less than is transitive: if a < b and b < c, then a < c', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          fc.bigUintN(64),
+          fc.bigUintN(64),
+          (a, b, c) => {
+            fc.pre(a < b && b < c);
+            return uint64Simulator.lt(a, c);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Less than or equal is reflexive: a ≤ a', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          (a) => {
+            return uint64Simulator.lte(a, a);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Equality is symmetric: a = b implies b = a', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          (a) => {
+            return uint64Simulator.eq(a, a);
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Greater than is inverse of less than: a > b = b < a', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          fc.bigUintN(64),
+          (a, b) => {
+            const gtResult = uint64Simulator.gt(a, b);
+            const ltResult = uint64Simulator.lt(b, a);
+            return gtResult === ltResult;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+
+  describe('Boundary and Edge Cases', () => {
+    test('Operations with MAX_UINT64', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          (a) => {
+            // Multiplication with MAX_UINT64
+            const mulResult = uint64Simulator.mul(a, MAX_UINT64);
+            
+            // Division by MAX_UINT64
+            const divResult = uint64Simulator.div(a, MAX_UINT64);
+            
+            // These should complete without error
+            return true;
+          }
+        ),
+        { numRuns: 500 }
+      );
+    });
+
+    test('Operations with zero', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(64),
+          (a) => {
+            // Add zero
+            const addZero = uint64Simulator.add(a, 0n);
+            // Multiply by zero
+            const mulZero = uint64Simulator.mul(a, 0n);
+            
+            return addZero === a && mulZero === 0n;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+
+    test('Operations with MAX_UINT32 boundaries', () => {
+      fc.assert(
+        fc.property(
+          fc.bigUintN(32),
+          fc.bigUintN(32),
+          (a, b) => {
+            // Should handle 32-bit values gracefully
+            const sum = uint64Simulator.add(a, b);
+            const product = uint64Simulator.mul(a, b);
+            
+            return sum >= a && sum >= b && product >= 0n;
+          }
+        ),
+        { numRuns: 1000 }
+      );
+    });
+  });
+});