diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra
index 656cef538..0660b663c 100644
--- a/router/dataplane_spec.gobra
+++ b/router/dataplane_spec.gobra
@@ -200,7 +200,7 @@ func (d *DataPlane) getForwardingMetrics() {
 ghost
 requires acc(d.Mem(), _)
 // The termination of this method is assumed. The reason is that the termination
-// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
+// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
 // followed by a fold of the same invariant with the same permission amount.
 // Gobra requires intermediate assertions to make this verify,
 // which is not possible to add here.
@@ -212,7 +212,7 @@ pure func (d *DataPlane) getValForwardingMetrics() map[uint16]forwardingMetrics
 ghost
 requires acc(d.Mem(), _)
 // The termination of this method is assumed. The reason is that the termination
-// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
+// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
 // followed by a fold of the same invariant with the same permission amount.
 // Gobra requires intermediate assertions to make this verify,
 // which is not possible to add here.
@@ -228,7 +228,7 @@ pure func (d *DataPlane) getDomForwardingMetrics() set[uint16] {
 ghost
 requires acc(d.Mem(), _)
 // The termination of this method is assumed. The reason is that the termination
-// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
+// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
 // followed by a fold of the same invariant with the same permission amount.
 // Gobra requires intermediate assertions to make this verify,
 // which is not possible to add here.
@@ -244,7 +244,7 @@ pure func (d *DataPlane) GetDomInternalNextHops() set[uint16] {
 ghost
 requires acc(d.Mem(), _)
 // The termination of this method is assumed. The reason is that the termination
-// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
+// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
 // followed by a fold of the same invariant with the same permission amount.
 // Gobra requires intermediate assertions to make this verify,
 // which is not possible to add here.
@@ -343,7 +343,7 @@ func (d *DataPlane) getSvcMem() {
 ghost
 requires acc(d.Mem(), _)
 // The termination of this method is assumed. The reason is that the termination
-// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
+// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
 // followed by a fold of the same invariant with the same permission amount.
 // Gobra requires intermediate assertions to make this verify,
 // which is not possible to add here.
@@ -355,7 +355,7 @@ pure func (d *DataPlane) getValSvc() *services {
 ghost
 requires acc(d.Mem(), _)
 // The termination of this method is assumed. The reason is that the termination
-// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
+// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
 // followed by a fold of the same invariant with the same permission amount.
 // Gobra requires intermediate assertions to make this verify,
 // which is not possible to add here.
@@ -418,7 +418,7 @@ requires acc(d.Mem(), _)
 requires acc(&d.running, _)
 ensures  d.IsRunning() == d.running
 // The termination of this method is assumed. The reason is that the termination
-// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
+// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
 // followed by a fold of the same invariant with the same permission amount.
 // Gobra requires intermediate assertions to make this verify,
 // which is not possible to add here.
@@ -431,7 +431,7 @@ ghost
 pure
 requires acc(d.Mem(), _)
 // The termination of this method is assumed. The reason is that the termination
-// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
+// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
 // followed by a fold of the same invariant with the same permission amount.
 // Gobra requires intermediate assertions to make this verify,
 // which is not possible to add here.
@@ -444,7 +444,7 @@ ghost
 pure
 requires acc(d.Mem(), _)
 // The termination of this method is assumed. The reason is that the termination
-// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
+// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
 // followed by a fold of the same invariant with the same permission amount.
 // Gobra requires intermediate assertions to make this verify,
 // which is not possible to add here.
@@ -460,7 +460,7 @@ requires acc(d.Mem(), _)
 requires acc(&d.internal, _)
 ensures  d.InternalConnIsSet() == (d.internal != nil)
 // The termination of this method is assumed. The reason is that the termination
-// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
+// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
 // followed by a fold of the same invariant with the same permission amount.
 // Gobra requires intermediate assertions to make this verify,
 // which is not possible to add here.
@@ -473,7 +473,7 @@ ghost
 pure
 requires acc(d.Mem(), _)
 // The termination of this method is assumed. The reason is that the termination
-// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
+// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
 // followed by a fold of the same invariant with the same permission amount.
 // Gobra requires intermediate assertions to make this verify,
 // which is not possible to add here.
@@ -489,7 +489,7 @@ requires acc(d.Mem(), _)
 requires acc(&d.macFactory, _)
 ensures  d.KeyIsSet() == (d.macFactory != nil)
 // The termination of this method is assumed. The reason is that the termination
-// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
+// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
 // followed by a fold of the same invariant with the same permission amount.
 // Gobra requires intermediate assertions to make this verify,
 // which is not possible to add here.
@@ -502,7 +502,7 @@ ghost
 pure
 requires acc(d.Mem(), _)
 // The termination of this method is assumed. The reason is that the termination
-// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
+// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
 // followed by a fold of the same invariant with the same permission amount.
 // Gobra requires intermediate assertions to make this verify,
 // which is not possible to add here.
@@ -734,7 +734,7 @@ pure func (d *DataPlane) domainForwardingMetrics() set[uint16] {
 ghost
 requires acc(d.Mem(), _)
 // The termination of this method is assumed. The reason is that the termination
-// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
+// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
 // followed by a fold of the same invariant with the same permission amount.
 // Gobra requires intermediate assertions to make this verify,
 // which is not possible to add here.
diff --git a/router/io-spec.gobra b/router/io-spec.gobra
index a78d00391..1b65176f4 100644
--- a/router/io-spec.gobra
+++ b/router/io-spec.gobra
@@ -632,14 +632,14 @@ pure func (d *DataPlane) dpSpecWellConfiguredLinkTypes(dp io.DataPlaneSpec) bool
 }
 
 ghost 
-requires acc(MutexInvariant(d), _)
+requires acc(d.Mem(), _)
 // The termination of this method is assumed. The reason is that the termination
-// proof generated by this method is, essentially, an unfold acc(MutexInvariant(d), _)
+// proof generated by this method is, essentially, an unfold acc(d.Mem(), _)
 // followed by a fold of the same invariant with the same permission amount.
 // As shown in methods SimplifyPermInv and ElaboratePermInv, Gobra requires intermediate
 // assertions to make this verify, which is not easy to add here.
 decreases _
 pure func (d *DataPlane) dpSpecWellConfigured(dp io.DataPlaneSpec) bool {
-	return unfolding acc(MutexInvariant(d), _) in d.dpSpecWellConfiguredLocalIA(dp) &&
+	return unfolding acc(d.Mem(), _) in d.dpSpecWellConfiguredLocalIA(dp) &&
 		d.dpSpecWellConfiguredNeighborIAs(dp) && d.dpSpecWellConfiguredLinkTypes(dp)
 }