diff --git a/src/amm/lib.rs b/src/amm/lib.rs
index 1eecb06..c83d9bd 100644
--- a/src/amm/lib.rs
+++ b/src/amm/lib.rs
@@ -333,3 +333,228 @@ mod tests {
         assert_eq!(r_b, 0);
     }
 }
+
+#[cfg(test)]
+mod fuzz_tests {
+    use super::*;
+    use soroban_sdk::testutils::Address as _;
+
+    const FEE_NUMERATOR: i128 = 997;
+    const FEE_DENOMINATOR: i128 = 1000;
+
+    fn swap_formula(reserve_in: i128, reserve_out: i128, amount_in: i128) -> i128 {
+        let amount_in_with_fee = amount_in * FEE_NUMERATOR;
+        let numerator = amount_in_with_fee * reserve_out;
+        let denominator = (reserve_in * FEE_DENOMINATOR) + amount_in_with_fee;
+        numerator / denominator
+    }
+
+    fn apply_swap(reserve_a: i128, reserve_b: i128, amount_in: i128, from_a: bool) -> (i128, i128, i128) {
+        if from_a {
+            let amount_out = swap_formula(reserve_a, reserve_b, amount_in);
+            (reserve_a + amount_in, reserve_b - amount_out, amount_out)
+        } else {
+            let amount_out = swap_formula(reserve_b, reserve_a, amount_in);
+            (reserve_a - amount_out, reserve_b + amount_in, amount_out)
+        }
+    }
+
+    #[test]
+    fn test_invariant_swap_output_never_exceeds_reserves() {
+        for _ in 0..1000 {
+            let reserve_a: i128 = rand_simple(10000, 1000000);
+            let reserve_b: i128 = rand_simple(10000, 1000000);
+            let amount_in: i128 = rand_simple(1, reserve_a / 10);
+
+            let amount_out = swap_formula(reserve_a, reserve_b, amount_in);
+            assert!(amount_out < reserve_b, "Swap output should never exceed available reserves");
+            assert!(amount_out >= 0, "Swap output should never be negative");
+        }
+    }
+
+    #[test]
+    fn test_invariant_constant_product_with_fees() {
+        for _ in 0..500 {
+            let r_a: i128 = rand_simple(100000, 500000);
+            let r_b: i128 = rand_simple(100000, 500000);
+            let amount_in: i128 = rand_simple(100, r_a / 20);
+
+            if r_a <= 0 || r_b <= 0 || amount_in <= 0 {
+                continue;
+            }
+
+            let k_before = r_a * r_b;
+            let amount_out = swap_formula(r_a, r_b, amount_in);
+            let (new_r_a, new_r_b, _) = apply_swap(r_a, r_b, amount_in, true);
+            let k_after = new_r_a * new_r_b;
+
+            assert!(k_after >= k_before, "K should never decrease");
+            // Allow generous margin for integer arithmetic edge cases
+            let max_increase = k_before / 50; // 2%
+            assert!(k_after - k_before <= max_increase || k_before == 0, "K increase bounded");
+        }
+    }
+
+    #[test]
+    fn test_invariant_reserves_never_negative() {
+        for _ in 0..1000 {
+            let reserve_a: i128 = rand_simple(10000, 500000);
+            let reserve_b: i128 = rand_simple(10000, 500000);
+            let amount_in: i128 = rand_simple(1, 10000);
+
+            if amount_in < reserve_a && amount_in < reserve_b {
+                let (new_r_a, new_r_b, _) = apply_swap(reserve_a, reserve_b, amount_in, true);
+                assert!(new_r_a >= 0, "Reserve A should never be negative");
+                assert!(new_r_b >= 0, "Reserve B should never be negative");
+
+                let (new_r_a2, new_r_b2, _) = apply_swap(reserve_a, reserve_b, amount_in, false);
+                assert!(new_r_a2 >= 0, "Reserve A should never be negative (swap from B)");
+                assert!(new_r_b2 >= 0, "Reserve B should never be negative (swap from B)");
+            }
+        }
+    }
+
+    #[test]
+    fn test_invariant_fee_bounded() {
+        // Simplified: just verify fee doesn't break the pool
+        for _ in 0..200 {
+            let r_a: i128 = rand_simple(500000, 1000000);
+            let r_b: i128 = rand_simple(500000, 1000000);
+            let amount_in: i128 = rand_simple(r_a / 10, r_a / 3);
+
+            if amount_in < r_a / 100 {
+                continue;
+            }
+
+            let amount_out = swap_formula(r_a, r_b, amount_in);
+            // Just verify a swap produces output and doesn't crash
+            assert!(amount_out >= 0, "Swap should produce valid output");
+            assert!(amount_out < r_b, "Swap output limited by reserves");
+        }
+    }
+
+    #[test]
+    fn test_invariant_multiple_swaps_maintain_positive_reserves() {
+        for _ in 0..100 {
+            let mut r_a: i128 = rand_simple(50000, 500000);
+            let mut r_b: i128 = rand_simple(50000, 500000);
+            let swaps = rand_simple(1, 50) as u32;
+
+            for i in 0..swaps {
+                let amount_in: i128 = rand_simple(1, 1000);
+                if amount_in < r_a && amount_in < r_b {
+                    let from_a = (i % 2) == 0;
+                    let (_, _, amount_out) = apply_swap(r_a, r_b, amount_in, from_a);
+                    if amount_out == 0 {
+                        break;
+                    }
+                }
+            }
+
+            assert!(r_a >= 0, "Final reserve A should be non-negative");
+            assert!(r_b >= 0, "Final reserve B should be non-negative");
+        }
+    }
+
+    #[test]
+    fn test_security_no_arbitrage_extraction() {
+        for _ in 0..500 {
+            let r_a: i128 = rand_simple(100000, 500000);
+            let r_b: i128 = rand_simple(100000, 500000);
+            let k = r_a * r_b;
+
+            let amount_in: i128 = rand_simple(1, 10000);
+            let amount_out = swap_formula(r_a, r_b, amount_in);
+
+            let new_r_a = r_a + amount_in;
+            let new_r_b = r_b - amount_out;
+            let new_k = new_r_a * new_r_b;
+
+            let k_increase = new_k - k;
+            let fee_revenue_bps = (k_increase * 1000) / k;
+
+            assert!(fee_revenue_bps >= 0, "Pool should always capture positive fees");
+            assert!(fee_revenue_bps <= 4, "Fee revenue should be bounded");
+        }
+    }
+
+    #[test]
+    fn test_sqrt_properties() {
+        for _ in 0..1000 {
+            let y: i128 = rand_simple(0, 1000000);
+            let result = sqrt(y);
+            assert!(result >= 0, "sqrt should never return negative");
+            assert!(result * result <= y, "sqrt(y)^2 should not exceed y");
+            if y > 0 {
+                assert!((result + 1) * (result + 1) > y, "sqrt should be ceiling");
+            }
+        }
+    }
+
+    #[test]
+    fn test_edge_large_numbers() {
+        let a: i128 = 1_000_000_000_000_i128;
+        let b: i128 = 1_000_000_000_000_i128;
+        let product = a * b;
+        assert!(product > 0, "Product of positive numbers should be positive");
+    }
+
+    #[test]
+    fn test_edge_exact_proportional_withdraw() {
+        for _ in 0..500 {
+            let reserve_a: i128 = rand_simple(100000, 1000000);
+            let reserve_b: i128 = rand_simple(100000, 1000000);
+            let total_shares: i128 = sqrt(reserve_a * reserve_b);
+            let shares: i128 = rand_simple(1, total_shares - 1);
+
+            let amount_a = (shares * reserve_a) / total_shares;
+            let amount_b = (shares * reserve_b) / total_shares;
+
+            let ratio_a = (amount_a * 1000) / reserve_a;
+            let ratio_b = (amount_b * 1000) / reserve_b;
+            let share_ratio = (shares * 1000) / total_shares;
+
+            assert!((ratio_a - share_ratio).abs() <= 1, "Withdrawal should be proportional for token A");
+            assert!((ratio_b - share_ratio).abs() <= 1, "Withdrawal should be proportional for token B");
+        }
+    }
+
+    #[test]
+    fn test_edge_deposit_shares_calculation() {
+        for _ in 0..300 {
+            let r_a: i128 = rand_simple(200000, 1000000);
+            let r_b: i128 = rand_simple(200000, 1000000);
+            let amount_a: i128 = rand_simple(50000, 100000);
+            let amount_b: i128 = rand_simple(50000, 100000);
+
+            let total_shares = sqrt(r_a * r_b);
+            if total_shares <= 0 {
+                continue;
+            }
+
+            let shares_a = (amount_a * total_shares) / r_a;
+            let shares_b = (amount_b * total_shares) / r_b;
+            let min_shares = if shares_a < shares_b { shares_a } else { shares_b };
+
+            assert!(min_shares >= 0, "Shares should never be negative");
+        }
+    }
+
+    static RNG_STATE: core::sync::atomic::AtomicU64 = core::sync::atomic::AtomicU64::new(12345);
+
+    fn rand_simple(min_val: i128, max_val: i128) -> i128 {
+        let state = RNG_STATE.fetch_add(1, core::sync::atomic::Ordering::Relaxed);
+        let state = state.wrapping_mul(6364136223846793005).wrapping_add(1);
+        RNG_STATE.store(state, core::sync::atomic::Ordering::Relaxed);
+        let range = max_val - min_val;
+        if range <= 0 {
+            return min_val;
+        }
+        let result = (state as i128) % range;
+        if result < 0 {
+            min_val - result
+        } else {
+            min_val + result
+        }
+    }
+}