diff --git a/src/command/dispatch.rs b/src/command/dispatch.rs
index 29eeb47..efa43cb 100644
--- a/src/command/dispatch.rs
+++ b/src/command/dispatch.rs
@@ -80,8 +80,8 @@ pub fn dispatch(model: &mut Model, cmd: &Command) -> CommandResult {
             }
         }
 
-        Command::RemoveFormula { target } => {
-            model.remove_formula(target);
+        Command::RemoveFormula { target, target_category } => {
+            model.remove_formula(target, target_category);
             CommandResult::ok()
         }
 
diff --git a/src/command/types.rs b/src/command/types.rs
index ece8abd..283c8f6 100644
--- a/src/command/types.rs
+++ b/src/command/types.rs
@@ -31,8 +31,8 @@ pub enum Command {
     /// `target_category` names the category that owns the formula target.
     AddFormula { raw: String, target_category: String },
 
-    /// Remove a formula by its target name.
-    RemoveFormula { target: String },
+    /// Remove a formula by its target name and category.
+    RemoveFormula { target: String, target_category: String },
 
     /// Create a new view.
     CreateView { name: String },
diff --git a/src/model/model.rs b/src/model/model.rs
index 24441b2..519b051 100644
--- a/src/model/model.rs
+++ b/src/model/model.rs
@@ -72,16 +72,18 @@ impl Model {
     }
 
     pub fn add_formula(&mut self, formula: Formula) {
-        // Replace if same target
-        if let Some(pos) = self.formulas.iter().position(|f| f.target == formula.target) {
+        // Replace if same target within the same category
+        if let Some(pos) = self.formulas.iter().position(|f| {
+            f.target == formula.target && f.target_category == formula.target_category
+        }) {
             self.formulas[pos] = formula;
         } else {
             self.formulas.push(formula);
         }
     }
 
-    pub fn remove_formula(&mut self, target: &str) {
-        self.formulas.retain(|f| f.target != target);
+    pub fn remove_formula(&mut self, target: &str, target_category: &str) {
+        self.formulas.retain(|f| !(f.target == target && f.target_category == target_category));
     }
 
     pub fn active_view(&self) -> Option<&View> {
@@ -156,10 +158,11 @@ impl Model {
 
         // Check WHERE filter first
         if let Some(filter) = &formula.filter {
-            if let Some(item_val) = context.get(&filter.category) {
-                if item_val != filter.item.as_str() {
-                    return self.data.get(context).clone();
-                }
+            let matches = context.get(&filter.category)
+                .map(|v| v == filter.item.as_str())
+                .unwrap_or(false);
+            if !matches {
+                return self.data.get(context).clone();
             }
         }
 
@@ -198,8 +201,16 @@ impl Model {
                     })
                 }
                 Expr::UnaryMinus(e) => Some(-eval_expr(e, context, model, target_category)?),
-                Expr::Agg(func, _inner, _filter) => {
-                    let partial = context.without(target_category);
+                Expr::Agg(func, inner, agg_filter) => {
+                    let mut partial = context.without(target_category);
+                    if let Expr::Ref(item_name) = inner.as_ref() {
+                        if let Some(cat) = find_item_category(model, item_name) {
+                            partial = partial.with(cat, item_name.as_str());
+                        }
+                    }
+                    if let Some(f) = agg_filter {
+                        partial = partial.with(&f.category, &f.item);
+                    }
                     let values: Vec<f64> = model.data.matching_cells(&partial.0)
                         .into_iter()
                         .filter_map(|(_, v)| v.as_f64())
@@ -570,7 +581,7 @@ mod formula_tests {
     fn remove_formula() {
         let mut m = revenue_cost_model();
         m.add_formula(parse_formula("Profit = Revenue - Cost", "Measure").unwrap());
-        m.remove_formula("Profit");
+        m.remove_formula("Profit", "Measure");
         assert!(m.formulas.is_empty());
         let k = coord(&[("Measure", "Profit"), ("Region", "East")]);
         assert_eq!(m.evaluate(&k), CellValue::Empty);
@@ -582,7 +593,8 @@ mod formula_tests {
         m.add_formula(parse_formula("Total = SUM(Revenue)", "Measure").unwrap());
         if let Some(cat) = m.category_mut("Measure") { cat.add_item("Total"); }
         let val = m.evaluate(&coord(&[("Measure", "Total"), ("Region", "East")])).as_f64().unwrap();
-        assert!(val > 0.0, "SUM should be positive, got {val}");
+        // Revenue(East)=1000 only — Cost must not be included
+        assert_eq!(val, 1000.0);
     }
 
     #[test]
@@ -627,6 +639,126 @@ mod formula_tests {
         m.add_formula(parse_formula("Result = IF(X > 5, 1, 0)", "Measure").unwrap());
         assert_eq!(m.evaluate(&coord(&[("Measure", "Result")])), CellValue::Number(0.0));
     }
+
+    // ── Bug regression tests ─────────────────────────────────────────────────
+
+    /// Bug: WHERE filter falls through when its category is absent from the key.
+    /// A formula `Profit = 42 WHERE Region = "East"` evaluated against a key
+    /// with no Region coordinate should NOT apply the formula — the WHERE
+    /// condition cannot be satisfied, so the raw cell value (Empty) must be
+    /// returned.  Currently the `if let Some(item_val)` in eval_formula fails
+    /// to bind (category absent → None) and falls through, applying the formula
+    /// unconditionally.
+    #[test]
+    fn where_filter_absent_category_does_not_apply_formula() {
+        let mut m = Model::new("Test");
+        m.add_category("Measure").unwrap();
+        m.add_category("Region").unwrap();
+        if let Some(cat) = m.category_mut("Measure") {
+            cat.add_item("Profit");
+        }
+        if let Some(cat) = m.category_mut("Region") {
+            cat.add_item("East");
+        }
+        // Formula only applies WHERE Region = "East"
+        m.add_formula(parse_formula("Profit = 42 WHERE Region = \"East\"", "Measure").unwrap());
+        // Key has no Region coordinate — WHERE clause cannot be satisfied
+        let key_no_region = coord(&[("Measure", "Profit")]);
+        // Expected: Empty (formula should not apply)
+        // Bug: returns Number(42) — formula applied because absent category falls through
+        assert_eq!(m.evaluate(&key_no_region), CellValue::Empty);
+    }
+
+    /// Bug: SUM(Revenue) ignores its inner expression and sums all numeric
+    /// cells matching the partial key, including unrelated items (e.g. Cost).
+    /// With Revenue=100 and Cost=50 both stored for Region=East, evaluating
+    /// `Total = SUM(Revenue)` at {Measure=Total, Region=East} should return
+    /// 100 (only Revenue), not 150 (Revenue + Cost).
+    #[test]
+    fn sum_inner_expression_constrains_which_cells_are_summed() {
+        let mut m = Model::new("Test");
+        m.add_category("Measure").unwrap();
+        m.add_category("Region").unwrap();
+        if let Some(cat) = m.category_mut("Measure") {
+            cat.add_item("Revenue");
+            cat.add_item("Cost");
+            cat.add_item("Total");
+        }
+        if let Some(cat) = m.category_mut("Region") {
+            cat.add_item("East");
+        }
+        m.set_cell(coord(&[("Measure", "Revenue"), ("Region", "East")]), CellValue::Number(100.0));
+        m.set_cell(coord(&[("Measure", "Cost"),    ("Region", "East")]), CellValue::Number(50.0));
+        m.add_formula(parse_formula("Total = SUM(Revenue)", "Measure").unwrap());
+        // Expected: 100 (SUM constrainted to Revenue only)
+        // Bug: returns 150 — inner Ref("Revenue") is ignored, Cost is also summed
+        assert_eq!(
+            m.evaluate(&coord(&[("Measure", "Total"), ("Region", "East")])),
+            CellValue::Number(100.0),
+        );
+    }
+
+    /// Bug: add_formula deduplicates by `target` name alone, ignoring
+    /// `target_category`.  Two formulas for the same item name in different
+    /// categories should coexist; adding the second should not silently
+    /// replace the first.
+    #[test]
+    fn add_formula_same_target_name_different_category_both_coexist() {
+        let mut m = Model::new("Test");
+        m.add_category("Measure").unwrap();
+        m.add_category("KPI").unwrap();
+        if let Some(c) = m.category_mut("Measure") { c.add_item("Profit"); }
+        if let Some(c) = m.category_mut("KPI")     { c.add_item("Profit"); }
+
+        m.add_formula(parse_formula("Profit = 1", "Measure").unwrap());
+        m.add_formula(parse_formula("Profit = 2", "KPI").unwrap());
+
+        // Both formulas target different categories — they must coexist.
+        // Bug: len == 1 because the second replaced the first.
+        assert_eq!(m.formulas.len(), 2);
+    }
+
+    /// Consequence of the same bug: evaluating the formula that was silently
+    /// dropped returns Empty instead of the expected computed value.
+    #[test]
+    fn add_formula_same_target_name_different_category_evaluates_independently() {
+        let mut m = Model::new("Test");
+        m.add_category("Measure").unwrap();
+        m.add_category("KPI").unwrap();
+        if let Some(c) = m.category_mut("Measure") { c.add_item("Profit"); }
+        if let Some(c) = m.category_mut("KPI")     { c.add_item("Profit"); }
+
+        m.add_formula(parse_formula("Profit = 1", "Measure").unwrap());
+        m.add_formula(parse_formula("Profit = 2", "KPI").unwrap());
+
+        // Measure formula → 1, KPI formula → 2
+        // Bug: first formula was replaced; {Measure=Profit} evaluates to Empty.
+        assert_eq!(m.evaluate(&coord(&[("Measure", "Profit")])), CellValue::Number(1.0));
+        assert_eq!(m.evaluate(&coord(&[("KPI",     "Profit")])), CellValue::Number(2.0));
+    }
+
+    /// Bug: remove_formula matches by target name alone, so removing "Profit"
+    /// in "Measure" also destroys the "Profit" formula in "KPI".
+    /// After targeted removal, the other category's formula must survive.
+    #[test]
+    fn remove_formula_only_removes_specified_target_category() {
+        let mut m = Model::new("Test");
+        m.add_category("Measure").unwrap();
+        m.add_category("KPI").unwrap();
+        if let Some(c) = m.category_mut("Measure") { c.add_item("Profit"); }
+        if let Some(c) = m.category_mut("KPI")     { c.add_item("Profit"); }
+
+        m.add_formula(parse_formula("Profit = 1", "Measure").unwrap());
+        m.add_formula(parse_formula("Profit = 2", "KPI").unwrap());
+
+        // Remove only the Measure formula
+        m.remove_formula("Profit", "Measure");
+
+        // KPI formula must survive
+        // Bug: remove_formula("Profit") wipes both; formulas.len() == 0
+        assert_eq!(m.formulas.len(), 1);
+        assert_eq!(m.evaluate(&coord(&[("KPI", "Profit")])), CellValue::Number(2.0));
+    }
 }
 
 #[cfg(test)]
@@ -883,3 +1015,157 @@ mod five_category {
     }
 }
 
+#[cfg(test)]
+mod prop_tests {
+    use proptest::prelude::*;
+    use super::Model;
+    use crate::model::cell::{CellKey, CellValue};
+    use crate::formula::parse_formula;
+
+    fn finite_f64() -> impl Strategy<Value = f64> {
+        prop::num::f64::NORMAL.prop_filter("finite", |f| f.is_finite())
+    }
+
+    proptest! {
+        /// evaluate() on a plain cell (no formula) returns exactly what was stored.
+        #[test]
+        fn evaluate_returns_stored_value_when_no_formula_applies(
+            item_a in "[a-z]{1,6}",
+            item_b in "[a-z]{1,6}",
+            val in finite_f64(),
+        ) {
+            let mut m = Model::new("T");
+            m.add_category("Cat").unwrap();
+            if let Some(c) = m.category_mut("Cat") {
+                c.add_item(&item_a);
+                c.add_item(&item_b);
+            }
+            let key = CellKey::new(vec![("Cat".into(), item_a.clone())]);
+            m.set_cell(key.clone(), CellValue::Number(val));
+            prop_assert_eq!(m.evaluate(&key), CellValue::Number(val));
+        }
+
+        /// Writing to cell A does not change cell B when the keys differ.
+        #[test]
+        fn cells_with_different_items_are_independent(
+            item_a in "[a-z]{1,5}",
+            item_b in "[g-z]{1,5}",
+            val_a in finite_f64(),
+            val_b in finite_f64(),
+        ) {
+            prop_assume!(item_a != item_b);
+            let mut m = Model::new("T");
+            m.add_category("Cat").unwrap();
+            if let Some(c) = m.category_mut("Cat") {
+                c.add_item(&item_a);
+                c.add_item(&item_b);
+            }
+            let key_a = CellKey::new(vec![("Cat".into(), item_a)]);
+            let key_b = CellKey::new(vec![("Cat".into(), item_b)]);
+            m.set_cell(key_a.clone(), CellValue::Number(val_a));
+            m.set_cell(key_b.clone(), CellValue::Number(val_b));
+            prop_assert_eq!(m.evaluate(&key_a), CellValue::Number(val_a));
+            prop_assert_eq!(m.evaluate(&key_b), CellValue::Number(val_b));
+        }
+
+        /// Adding a category does not overwrite previously stored cell values.
+        #[test]
+        fn adding_category_preserves_existing_cells(
+            val in finite_f64(),
+            new_cat in "[g-z]{1,6}",
+        ) {
+            let mut m = Model::new("T");
+            m.add_category("Measure").unwrap();
+            if let Some(c) = m.category_mut("Measure") { c.add_item("Revenue"); }
+            let key = CellKey::new(vec![("Measure".into(), "Revenue".into())]);
+            m.set_cell(key.clone(), CellValue::Number(val));
+            let _ = m.add_category(&new_cat); // may succeed or hit the 12-cat limit
+            prop_assert_eq!(m.evaluate(&key), CellValue::Number(val));
+        }
+
+        /// evaluate() is deterministic: calling it twice on the same key and model
+        /// yields the same result.
+        #[test]
+        fn evaluate_is_deterministic(val_rev in finite_f64(), val_cost in finite_f64()) {
+            let mut m = Model::new("T");
+            m.add_category("Measure").unwrap();
+            m.add_category("Region").unwrap();
+            if let Some(c) = m.category_mut("Measure") {
+                c.add_item("Revenue");
+                c.add_item("Cost");
+                c.add_item("Profit");
+            }
+            if let Some(c) = m.category_mut("Region") { c.add_item("East"); }
+            m.set_cell(
+                CellKey::new(vec![("Measure".into(),"Revenue".into()),("Region".into(),"East".into())]),
+                CellValue::Number(val_rev),
+            );
+            m.set_cell(
+                CellKey::new(vec![("Measure".into(),"Cost".into()),("Region".into(),"East".into())]),
+                CellValue::Number(val_cost),
+            );
+            m.add_formula(parse_formula("Profit = Revenue - Cost", "Measure").unwrap());
+            let key = CellKey::new(vec![
+                ("Measure".into(), "Profit".into()),
+                ("Region".into(), "East".into()),
+            ]);
+            prop_assert_eq!(m.evaluate(&key), m.evaluate(&key));
+        }
+
+        /// Formula result equals Revenue − Cost for arbitrary finite inputs.
+        #[test]
+        fn formula_arithmetic_correct(
+            rev in finite_f64(),
+            cost in finite_f64(),
+        ) {
+            let mut m = Model::new("T");
+            m.add_category("Measure").unwrap();
+            m.add_category("Region").unwrap();
+            if let Some(c) = m.category_mut("Measure") {
+                c.add_item("Revenue");
+                c.add_item("Cost");
+                c.add_item("Profit");
+            }
+            if let Some(c) = m.category_mut("Region") { c.add_item("East"); }
+            let rev_key = CellKey::new(vec![("Measure".into(),"Revenue".into()),("Region".into(),"East".into())]);
+            let cost_key = CellKey::new(vec![("Measure".into(),"Cost".into()),("Region".into(),"East".into())]);
+            let profit_key = CellKey::new(vec![("Measure".into(),"Profit".into()),("Region".into(),"East".into())]);
+            m.set_cell(rev_key, CellValue::Number(rev));
+            m.set_cell(cost_key, CellValue::Number(cost));
+            m.add_formula(parse_formula("Profit = Revenue - Cost", "Measure").unwrap());
+            let expected = rev - cost;
+            prop_assert_eq!(m.evaluate(&profit_key), CellValue::Number(expected));
+        }
+
+        /// Removing a formula restores the raw stored value (or Empty).
+        #[test]
+        fn removing_formula_restores_raw_value(rev in finite_f64(), cost in finite_f64()) {
+            let mut m = Model::new("T");
+            m.add_category("Measure").unwrap();
+            m.add_category("Region").unwrap();
+            if let Some(c) = m.category_mut("Measure") {
+                c.add_item("Revenue"); c.add_item("Cost"); c.add_item("Profit");
+            }
+            if let Some(c) = m.category_mut("Region") { c.add_item("East"); }
+            let profit_key = CellKey::new(vec![
+                ("Measure".into(),"Profit".into()),("Region".into(),"East".into()),
+            ]);
+            m.set_cell(
+                CellKey::new(vec![("Measure".into(),"Revenue".into()),("Region".into(),"East".into())]),
+                CellValue::Number(rev),
+            );
+            m.set_cell(
+                CellKey::new(vec![("Measure".into(),"Cost".into()),("Region".into(),"East".into())]),
+                CellValue::Number(cost),
+            );
+            m.add_formula(parse_formula("Profit = Revenue - Cost", "Measure").unwrap());
+            // Formula active — result is rev - cost
+            let with_formula = m.evaluate(&profit_key);
+            prop_assert_eq!(with_formula, CellValue::Number(rev - cost));
+            // Remove formula — cell has no raw value, so Empty
+            m.remove_formula("Profit", "Measure");
+            prop_assert_eq!(m.evaluate(&profit_key), CellValue::Empty);
+        }
+    }
+}
+