diff --git a/Strata/Languages/Laurel/HeapParameterization.lean b/Strata/Languages/Laurel/HeapParameterization.lean
index fecaf5350c..886756cc65 100644
--- a/Strata/Languages/Laurel/HeapParameterization.lean
+++ b/Strata/Languages/Laurel/HeapParameterization.lean
@@ -471,6 +471,10 @@ def heapTransformProcedure (model: SemanticModel) (proc : Procedure) : Transform
     -- Preconditions use $heap_in (the input state)
     let preconditions' ← proc.preconditions.mapM (·.mapM (heapTransformExpr heapInName model))
 
+    let inHeapRef := mkMd $ .StaticCall "Heap..nextReference!" [mkMd $ .Var (.Local heapInName)]
+    let outHeapRef := mkMd $ .StaticCall "Heap..nextReference!" [mkMd $ .Var (.Local heapName)]
+    let monoCond : Condition := {condition:= {val:= .PrimitiveOp .Geq [outHeapRef, inHeapRef], source:= proc.name.source}, summary := s!"Heap reference counter monotone ({proc.name.text})"}
+
     let bodyValueIsUsed := !proc.outputs.isEmpty
     let body' ← match proc.body with
       | .Transparent bodyExpr =>
@@ -488,10 +492,15 @@ def heapTransformProcedure (model: SemanticModel) (proc : Procedure) : Transform
                 pure (some (mkMd (.Block [assignHeap, implExpr'] none)))
             | none => pure none
           let modif' ← modif.mapM (heapTransformExpr heapName model ·)
-          pure (.Opaque postconds' impl' modif')
+          -- When impl' = none, monoCond is axiomatic; it's safe to assume
+          -- because heapTransformExpr only uses updateField (preserves
+          -- nextReference) and increment (increases it by 1).
+          pure (.Opaque (monoCond::postconds') impl' modif')
       | .Abstract postconds =>
           let postconds' ← postconds.mapM (·.mapM (heapTransformExpr heapName model))
-          pure (.Abstract postconds')
+          -- monoCond is safe to assume because heapTransformExpr only uses
+          -- updateField (preserves nextReference) and increment (increases it by 1)
+          pure (.Abstract (monoCond::postconds'))
       | .External => pure .External
 
     return { proc with
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
index 7dbf35022d..d139fa0045 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
@@ -158,6 +158,23 @@ procedure datatypeField()
 //   assert x == 4;
 // }
 
+procedure someWriteHeapProcedure(c: Container) returns ()
+  opaque
+  modifies c
+{
+  c#intValue := 5
+}
+;
+
+procedure callerUsesAllocateTwo()
+  opaque
+{
+  var c: Container;
+  var d: Container;
+  c := new Container;
+  someWriteHeapProcedure(c);
+  d := new Container;
+  assert c != d
 procedure modifyHeapAndReturnMultiple(c: Container) returns (x: int, y: int, z: int)
   opaque
   ensures x == 1 && y == 2 && z == 3
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean b/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean
index 52a16146c5..7c23902247 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean
@@ -68,7 +68,7 @@ procedure modifyContainerWildcard(c: Container) returns (i: int)
 };
 
 procedure modifyContainerWithoutPermission1(c: Container, d: Container)
-//        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: modifies clause does not hold
+//        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: modifies clause could not be proved
   opaque
 {
     var i: int := modifyContainerWildcard(c)
@@ -127,7 +127,7 @@ procedure modifiesWildcardBodilessCaller()
   var x: int := d#value;
   modifiesWildcardBodiless(c, d);
   assert x == d#value // this should fail because modifies * means anything can change
-//^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
+//^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
 };
 
 procedure modifiesWildcardWithBody(c: Container, d: Container)
@@ -152,7 +152,7 @@ procedure modifiesWildcardAndSpecificCaller()
   var x: int := d#value;
   modifiesWildcardAndSpecific(c, d);
   assert x == d#value // fails because modifies * subsumes modifies c
-//^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
+//^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
 };
 "
 
diff --git a/StrataTest/Languages/Python/expected_interpret/test_heap_reference_monotone.expected b/StrataTest/Languages/Python/expected_interpret/test_heap_reference_monotone.expected
new file mode 100644
index 0000000000..2410119fac
--- /dev/null
+++ b/StrataTest/Languages/Python/expected_interpret/test_heap_reference_monotone.expected
@@ -0,0 +1 @@
+\[ERROR\] procedure '__main__': expected 1 arguments, got 0
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected b/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected
index 2583076f7e..9190988a33 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected
@@ -1,3 +1,5 @@
 test_class_decl.py(9, 4): ✅ pass - (CircularBuffer@__init__ requires) Type constraint of n
-DETAIL: 1 passed, 0 failed, 0 inconclusive
+test_class_decl.py(8, 0): ✅ pass - Heap reference counter monotone (main)
+unknown location: ✅ pass - Heap reference counter monotone (__main__)
+DETAIL: 3 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_empty.expected b/StrataTest/Languages/Python/expected_laurel/test_class_empty.expected
index aab04f3a0d..d2842ee32f 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_empty.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_empty.expected
@@ -1,4 +1,6 @@
 test_class_empty.py(5, 4): ✅ pass - callElimAssert_requires_4
 test_class_empty.py(6, 4): ✅ pass - empty class instantiated
-DETAIL: 2 passed, 0 failed, 0 inconclusive
+test_class_empty.py(4, 0): ✅ pass - Heap reference counter monotone (test)
+unknown location: ✅ pass - Heap reference counter monotone (__main__)
+DETAIL: 4 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_field_any.expected b/StrataTest/Languages/Python/expected_laurel/test_class_field_any.expected
index c6e5abb610..88670bc3af 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_field_any.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_field_any.expected
@@ -1,3 +1,5 @@
+test_class_field_any.py(2, 4): ✅ pass - Heap reference counter monotone (MyClass@__init__)
 test_class_field_any.py(6, 0): ❓ unknown - assert(113)
-DETAIL: 0 passed, 0 failed, 1 inconclusive
+unknown location: ✅ pass - Heap reference counter monotone (__main__)
+DETAIL: 2 passed, 0 failed, 1 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected b/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected
index 7cb1e2fc89..3d6f55d3c5 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected
@@ -1,2 +1,3 @@
-DETAIL: 0 passed, 0 failed, 0 inconclusive
+unknown location: ✔️ always true if reached - Heap reference counter monotone (__main__)
+DETAIL: 1 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected b/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected
index 0caaf75c9f..177bd78e77 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected
@@ -1,5 +1,6 @@
 test_class_field_use.py(14, 4): ✔️ always true if reached - Check PMul exception
 test_class_field_use.py(14, 4): ✔️ always true if reached - assert(302)
 test_class_field_use.py(15, 4): ✔️ always true if reached - Doubling of buffer did not work
-DETAIL: 3 passed, 0 failed, 0 inconclusive
+test_class_field_use.py(12, 0): ✔️ always true if reached - Heap reference counter monotone (main)
+DETAIL: 4 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_inheritance_no_dispatch.expected b/StrataTest/Languages/Python/expected_laurel/test_class_inheritance_no_dispatch.expected
index 703165c2c1..da1cfa6d99 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_inheritance_no_dispatch.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_inheritance_no_dispatch.expected
@@ -1,3 +1,4 @@
 test_class_inheritance_no_dispatch.py(25, 4): ❓ unknown - assert(714)
-DETAIL: 0 passed, 0 failed, 1 inconclusive
+unknown location: ✅ pass - Heap reference counter monotone (__main__)
+DETAIL: 1 passed, 0 failed, 1 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_method_call_from_main.expected b/StrataTest/Languages/Python/expected_laurel/test_class_method_call_from_main.expected
index 0047be2edb..46eebf0224 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_method_call_from_main.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_method_call_from_main.expected
@@ -1,6 +1,8 @@
+test_class_method_call_from_main.py(6, 4): ✅ pass - Heap reference counter monotone (Greeter@__init__)
 test_class_method_call_from_main.py(10, 8): ❓ unknown - name must not be empty
 test_class_method_call_from_main.py(9, 23): ❓ unknown - (Greeter@greet ensures) Return type constraint
 test_class_method_call_from_main.py(14, 4): ✅ pass - (Greeter@__init__ requires) Type constraint of name
 test_class_method_call_from_main.py(15, 4): ✅ pass - assert(415)
-DETAIL: 2 passed, 0 failed, 2 inconclusive
+unknown location: ✅ pass - Heap reference counter monotone (__main__)
+DETAIL: 4 passed, 0 failed, 2 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected b/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected
index 36c53a8361..2b0c6197f0 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected
@@ -7,5 +7,6 @@ test_class_methods.py(34, 4): ✔️ always true if reached - set_balance should
 test_class_methods.py(31, 4): ✔️ always true if reached - assert_name_is_foo
 test_class_methods.py(31, 4): ✔️ always true if reached - assert_opt_name_none_or_str
 test_class_methods.py(31, 4): ✔️ always true if reached - assert_opt_name_none_or_bar
-DETAIL: 9 passed, 0 failed, 0 inconclusive
+unknown location: ✔️ always true if reached - Heap reference counter monotone (__main__)
+DETAIL: 10 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_mixed_init.expected b/StrataTest/Languages/Python/expected_laurel/test_class_mixed_init.expected
index 766329f9a4..66f7a0fcbe 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_mixed_init.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_mixed_init.expected
@@ -1,4 +1,5 @@
 test_class_mixed_init.py(19, 0): ✔️ always true if reached - class with init
 test_class_mixed_init.py(19, 0): ❓ unknown - class with init
-DETAIL: 1 passed, 0 failed, 1 inconclusive
+unknown location: ✔️ always true if reached - Heap reference counter monotone (__main__)
+DETAIL: 2 passed, 0 failed, 1 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_no_init.expected b/StrataTest/Languages/Python/expected_laurel/test_class_no_init.expected
index 7228247375..49482d21be 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_no_init.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_no_init.expected
@@ -1,4 +1,6 @@
 test_class_no_init.py(5, 4): ✅ pass - callElimAssert_requires_4
 test_class_no_init.py(6, 4): ❓ unknown - class without __init__
-DETAIL: 1 passed, 0 failed, 1 inconclusive
+test_class_no_init.py(4, 0): ✅ pass - Heap reference counter monotone (test)
+unknown location: ✅ pass - Heap reference counter monotone (__main__)
+DETAIL: 3 passed, 0 failed, 1 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_no_init_multi_field.expected b/StrataTest/Languages/Python/expected_laurel/test_class_no_init_multi_field.expected
index 3dbe40b3b6..be65a205d6 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_no_init_multi_field.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_no_init_multi_field.expected
@@ -1,4 +1,6 @@
 test_class_no_init_multi_field.py(7, 4): ✅ pass - callElimAssert_requires_4
 test_class_no_init_multi_field.py(8, 4): ✅ pass - class with multiple annotated fields no init
-DETAIL: 2 passed, 0 failed, 0 inconclusive
+test_class_no_init_multi_field.py(6, 0): ✅ pass - Heap reference counter monotone (test)
+unknown location: ✅ pass - Heap reference counter monotone (__main__)
+DETAIL: 4 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_no_init_with_method.expected b/StrataTest/Languages/Python/expected_laurel/test_class_no_init_with_method.expected
index 29b6682a29..e92760fa12 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_no_init_with_method.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_no_init_with_method.expected
@@ -1,5 +1,7 @@
 test_class_no_init_with_method.py(4, 23): ❓ unknown - (WithMethod@get_x ensures) Return type constraint
 test_class_no_init_with_method.py(8, 4): ✅ pass - callElimAssert_requires_4
 test_class_no_init_with_method.py(9, 4): ✅ pass - class with method but no __init__
-DETAIL: 2 passed, 0 failed, 1 inconclusive
+test_class_no_init_with_method.py(7, 0): ✅ pass - Heap reference counter monotone (test)
+unknown location: ✅ pass - Heap reference counter monotone (__main__)
+DETAIL: 4 passed, 0 failed, 1 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected b/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected
index 1085e02e58..4b88850343 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected
@@ -5,5 +5,6 @@ test_class_with_methods.py(32, 4): ✔️ always true if reached - get_name shou
 test_class_with_methods.py(29, 4): ✔️ always true if reached - assert_name_is_foo
 test_class_with_methods.py(29, 4): ✔️ always true if reached - assert_opt_name_none_or_str
 test_class_with_methods.py(29, 4): ✔️ always true if reached - assert_opt_name_none_or_bar
-DETAIL: 7 passed, 0 failed, 0 inconclusive
+unknown location: ✔️ always true if reached - Heap reference counter monotone (__main__)
+DETAIL: 8 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_composite_return.expected b/StrataTest/Languages/Python/expected_laurel/test_composite_return.expected
index 9380a52945..d538b61731 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_composite_return.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_composite_return.expected
@@ -1,3 +1,5 @@
+test_composite_return.py(6, 4): ✅ pass - Heap reference counter monotone (MyService@__init__)
 test_composite_return.py(10, 4): ✅ pass - (MyService@__init__ requires) Type constraint of name
-DETAIL: 1 passed, 0 failed, 0 inconclusive
+test_composite_return.py(9, 0): ✅ pass - Heap reference counter monotone (create_service)
+DETAIL: 3 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_field_write.expected b/StrataTest/Languages/Python/expected_laurel/test_field_write.expected
index cb51cb69f9..b1dd518103 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_field_write.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_field_write.expected
@@ -1,4 +1,7 @@
+test_field_write.py(4, 4): ✅ pass - Heap reference counter monotone (Cell@__init__)
 test_field_write.py(8, 4): ✅ pass - (Cell@__init__ requires) Type constraint of val
 test_field_write.py(10, 4): ✅ pass - field overwritten
-DETAIL: 2 passed, 0 failed, 0 inconclusive
+test_field_write.py(7, 0): ✅ pass - Heap reference counter monotone (test_oop_field_write)
+unknown location: ✅ pass - Heap reference counter monotone (__main__)
+DETAIL: 5 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected b/StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected
index 9a320c707c..f4bc06f272 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected
@@ -6,5 +6,6 @@ test_havoc_callee_after_hole_call.py(25, 0): ✔️ always true if reached - com
 test_havoc_callee_after_hole_call.py(30, 0): ❓ unknown - expected unknown because argument locals should be havocked
 test_havoc_callee_after_hole_call.py(36, 0): ❓ unknown - assume_assume(1193)_calls_PIn_0
 test_havoc_callee_after_hole_call.py(37, 4): ✔️ always true if reached - for-loop over unmodeled iterator should not crash
-DETAIL: 4 passed, 0 failed, 4 inconclusive
+unknown location: ✔️ always true if reached - Heap reference counter monotone (__main__)
+DETAIL: 5 passed, 0 failed, 4 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_heap_reference_monotone.expected b/StrataTest/Languages/Python/expected_laurel/test_heap_reference_monotone.expected
new file mode 100644
index 0000000000..dd0f48839b
--- /dev/null
+++ b/StrataTest/Languages/Python/expected_laurel/test_heap_reference_monotone.expected
@@ -0,0 +1,7 @@
+test_heap_reference_monotone.py(2, 4): ✅ pass - Heap reference counter monotone (ClassA@__init__)
+test_heap_reference_monotone.py(5, 0): ✅ pass - (ClassA@__init__ requires) Type constraint of n
+test_heap_reference_monotone.py(6, 0): ✅ pass - (ClassA@__init__ requires) Type constraint of n
+test_heap_reference_monotone.py(11, 0): ✅ pass - assert(128)
+unknown location: ✅ pass - Heap reference counter monotone (__main__)
+DETAIL: 5 passed, 0 failed, 0 inconclusive
+RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_method_call_with_kwargs.expected b/StrataTest/Languages/Python/expected_laurel/test_method_call_with_kwargs.expected
index 315f62f13d..78bb62e30e 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_method_call_with_kwargs.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_method_call_with_kwargs.expected
@@ -5,5 +5,6 @@ test_method_call_with_kwargs.py(8, 0): ✅ pass - (MyClass@__init__ requires) Ty
 test_method_call_with_kwargs.py(9, 0): ✅ pass - (MyClass@some_method requires) Type constraint of ip1
 test_method_call_with_kwargs.py(9, 0): ✅ pass - (MyClass@some_method requires) Type constraint of ip2
 test_method_call_with_kwargs.py(9, 0): ✅ pass - (MyClass@some_method requires) Type constraint of ip3
-DETAIL: 7 passed, 0 failed, 0 inconclusive
+unknown location: ✅ pass - Heap reference counter monotone (__main__)
+DETAIL: 8 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_method_kwargs_no_hierarchy.expected b/StrataTest/Languages/Python/expected_laurel/test_method_kwargs_no_hierarchy.expected
index 56de827e26..2595da4443 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_method_kwargs_no_hierarchy.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_method_kwargs_no_hierarchy.expected
@@ -1,3 +1,4 @@
+test_method_kwargs_no_hierarchy.py(2, 4): ✅ pass - Heap reference counter monotone (Calculator@__init__)
 test_method_kwargs_no_hierarchy.py(5, 41): ❓ unknown - (Calculator@add ensures) Return type constraint
 test_method_kwargs_no_hierarchy.py(9, 4): ✅ pass - (Calculator@__init__ requires) Type constraint of base
 unknown location: ✅ pass - assert_assert(0)_calls_Any_get_or_none_0
@@ -7,6 +8,7 @@ test_method_kwargs_no_hierarchy.py(11, 18): ✅ pass - (Calculator@add requires)
 test_method_kwargs_no_hierarchy.py(11, 18): ✅ pass - (Calculator@add requires) Type constraint of y
 test_method_kwargs_no_hierarchy.py(11, 4): ✅ pass - assert(254)
 test_method_kwargs_no_hierarchy.py(12, 4): ❓ unknown - assert(286)
+test_method_kwargs_no_hierarchy.py(8, 0): ✅ pass - Heap reference counter monotone (main)
 test_method_kwargs_no_hierarchy.py(8, 14): ✅ pass - (main ensures) Return type constraint
-DETAIL: 8 passed, 0 failed, 2 inconclusive
+DETAIL: 10 passed, 0 failed, 2 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected b/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected
index c73e76d8cb..f3576755b0 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected
@@ -1,9 +1,12 @@
 test_with_statement.py(17, 4): ✔️ always true if reached - assert(364)
 test_with_statement.py(20, 4): ✔️ always true if reached - assert(426)
+test_with_statement.py(15, 0): ✔️ always true if reached - Heap reference counter monotone (test_with_as)
 test_with_statement.py(25, 8): ✔️ always true if reached - assert(525)
 test_with_statement.py(26, 8): ✔️ always true if reached - assert(558)
+test_with_statement.py(22, 0): ✔️ always true if reached - Heap reference counter monotone (test_with_no_as)
 test_with_statement.py(32, 21): ✔️ always true if reached - Check PAdd exception
 test_with_statement.py(32, 8): ✔️ always true if reached - assert(697)
 test_with_statement.py(33, 8): ✔️ always true if reached - assert(724)
-DETAIL: 7 passed, 0 failed, 0 inconclusive
+test_with_statement.py(28, 0): ✔️ always true if reached - Heap reference counter monotone (test_with_multiple)
+DETAIL: 10 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_with_void_enter.expected b/StrataTest/Languages/Python/expected_laurel/test_with_void_enter.expected
index 86faeff6d1..63482f483c 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_with_void_enter.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_with_void_enter.expected
@@ -1,4 +1,8 @@
+test_with_void_enter.py(2, 4): ✅ pass - Heap reference counter monotone (VoidManager@__init__)
+test_with_void_enter.py(5, 4): ✅ pass - Heap reference counter monotone (VoidManager@__enter__)
+test_with_void_enter.py(8, 4): ✅ pass - Heap reference counter monotone (VoidManager@__exit__)
 test_with_void_enter.py(14, 8): ✅ pass - assert(272)
 test_with_void_enter.py(15, 4): ✅ pass - assert(287)
-DETAIL: 2 passed, 0 failed, 0 inconclusive
+test_with_void_enter.py(11, 0): ✅ pass - Heap reference counter monotone (test_void_enter)
+DETAIL: 6 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/run_py_analyze_sarif.py b/StrataTest/Languages/Python/run_py_analyze_sarif.py
index 1e12630061..d4150519f3 100755
--- a/StrataTest/Languages/Python/run_py_analyze_sarif.py
+++ b/StrataTest/Languages/Python/run_py_analyze_sarif.py
@@ -43,6 +43,7 @@
     "test_dict_operations",
     "test_for_loop",
     "test_func_input_type_constraints",
+    "test_heap_reference_monotone",
     "test_if_elif",
     "test_ifexpr",
     "test_list",
diff --git a/StrataTest/Languages/Python/tests/test_heap_reference_monotone.py b/StrataTest/Languages/Python/tests/test_heap_reference_monotone.py
new file mode 100644
index 0000000000..18993e817d
--- /dev/null
+++ b/StrataTest/Languages/Python/tests/test_heap_reference_monotone.py
@@ -0,0 +1,11 @@
+class ClassA:
+    def __init__(self, n: int):
+        self.val : int = n
+
+a1 = ClassA(1)
+a2 = ClassA(2)
+
+a1.val = 1
+a2.val = 2
+
+assert a1.val != a2.val