diff --git a/src/col/vct/col/origin/Blame.scala b/src/col/vct/col/origin/Blame.scala
index cf7431a27..a3e676626 100644
--- a/src/col/vct/col/origin/Blame.scala
+++ b/src/col/vct/col/origin/Blame.scala
@@ -359,6 +359,16 @@ case class ContextEverywhereFailedInPost(
   override def inlineDescWithSource(node: String, failure: String): String =
     s"Context of `$node` may not hold in the postcondition, since $failure."
 }
+case class ContextEverywhereFailedInRunPost(
+    failure: ContractFailure,
+    node: RunMethod[_],
+) extends ContractedFailure with WithContractFailure {
+  override def baseCode: String = "contextRunPostFailed"
+  override def descInContext: String =
+    "Context may not hold in postcondition, since"
+  override def inlineDescWithSource(node: String, failure: String): String =
+    s"Context of `$node` may not hold in the postcondition, since $failure."
+}
 case class AutoValueLeakCheckFailed(
     failure: ContractFailure,
     node: ContractApplicable[_],
diff --git a/src/rewrite/vct/rewrite/PropagateContextEverywhere.scala b/src/rewrite/vct/rewrite/PropagateContextEverywhere.scala
index 814326d68..6549ed8e8 100644
--- a/src/rewrite/vct/rewrite/PropagateContextEverywhere.scala
+++ b/src/rewrite/vct/rewrite/PropagateContextEverywhere.scala
@@ -24,6 +24,12 @@ case object PropagateContextEverywhere extends RewriterBuilder {
     override def blame(error: PostconditionFailed): Unit =
       app.blame.blame(ContextEverywhereFailedInPost(error.failure, app))
   }
+
+  case class ContextEverywhereRunPostconditionFailed(app: RunMethod[_])
+    extends Blame[PostconditionFailed] {
+    override def blame(error: PostconditionFailed): Unit =
+      app.blame.blame(ContextEverywhereFailedInRunPost(error.failure, app))
+  }
 }
 
 case class PropagateContextEverywhere[Pre <: Generation]()
@@ -60,6 +66,19 @@ case class PropagateContextEverywhere[Pre <: Generation]()
             }
           },
         ))
+      case runMethod: RunMethod[Pre] =>
+        allScopes.anyDeclare(allScopes.anySucceedOnly(
+          runMethod,
+          invariants.having(
+            invariants.top ++ unfoldStar(runMethod.contract.contextEverywhere)
+          ) {
+                runMethod.rewrite(blame =
+                  PostBlameSplit
+                    .left(ContextEverywhereRunPostconditionFailed(runMethod), runMethod.blame)
+                )
+          },
+        ))
+
       case other => rewriteDefault(other)
     }
 
diff --git a/test/main/vct/test/integration/examples/ForkJoinSpec.scala b/test/main/vct/test/integration/examples/ForkJoinSpec.scala
index 6f9085244..47503fbb1 100644
--- a/test/main/vct/test/integration/examples/ForkJoinSpec.scala
+++ b/test/main/vct/test/integration/examples/ForkJoinSpec.scala
@@ -9,4 +9,27 @@ class ForkJoinSpec extends VercorsSpec {
   vercors should verify using anyBackend example "concepts/forkjoin/fibonacci.pvl"
   vercors should verify using anyBackend examples("concepts/forkjoin/OwickiGries.pvl", "concepts/forkjoin/Worker.pvl")
   vercors should error withCode "runnableMethodMissing" example "concepts/forkjoin/TestFork.pvl"
+  vercors should verify using anyBackend in "The context_everywhere of a run method" pvl
+    """
+    pure int f();
+
+    class C {
+      context_everywhere f() == 3;
+      run {
+        assert f() == 3;
+      }
+    }
+
+    requires f() == 3;
+    void main() {
+        C c = new C();
+        fork c;
+        join c;
+    }
+    """
+
+
+
+
+
 }