diff --git a/frontends/benchmarks/verification/valid/RequireEnsuringMessages.scala b/frontends/benchmarks/verification/valid/RequireEnsuringMessages.scala
new file mode 100644
index 0000000000..202f4d08a4
--- /dev/null
+++ b/frontends/benchmarks/verification/valid/RequireEnsuringMessages.scala
@@ -0,0 +1,15 @@
+object RequireEnsuringMessages {
+  case class MyClass(a: Int) {
+    require(a > 0, "a must be strictly positive")
+  }
+
+  def useMyClass(mc: MyClass): Int = {
+    assert(mc.a > 0, "a is surely strictly positive")
+    mc.a
+  }.ensuring(_ > -42, "trivially trivial")
+
+  def createMyClass(a: Int): MyClass = {
+    require(a > 0, "To create MyClass, a must be strictly positive")
+    MyClass(a)
+  }
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/verification/valid/RequireEnsuringMessagesStaticChecks.scala b/frontends/benchmarks/verification/valid/RequireEnsuringMessagesStaticChecks.scala
new file mode 100644
index 0000000000..ffb84b2ade
--- /dev/null
+++ b/frontends/benchmarks/verification/valid/RequireEnsuringMessagesStaticChecks.scala
@@ -0,0 +1,17 @@
+import stainless.lang.StaticChecks._
+
+object RequireEnsuringMessages {
+  case class MyClass(a: Int) {
+    require(a > 0, "a must be strictly positive")
+  }
+
+  def useMyClass(mc: MyClass): Int = {
+    assert(mc.a > 0, "a is surely strictly positive")
+    mc.a
+  }.ensuring(_ > -42, "trivially trivial")
+
+  def createMyClass(a: Int): MyClass = {
+    require(a > 0, "To create MyClass, a must be strictly positive")
+    MyClass(a)
+  }
+}
\ No newline at end of file
diff --git a/frontends/dotty/src/main/scala/stainless/frontends/dotc/ASTExtractors.scala b/frontends/dotty/src/main/scala/stainless/frontends/dotc/ASTExtractors.scala
index a01fccb3bf..59a90ce881 100644
--- a/frontends/dotty/src/main/scala/stainless/frontends/dotc/ASTExtractors.scala
+++ b/frontends/dotty/src/main/scala/stainless/frontends/dotc/ASTExtractors.scala
@@ -1026,10 +1026,12 @@ trait ASTExtractors {
       * first call in the block). */
     object ExRequiredExpression {
       def unapply(tree: tpd.Apply): Option[(tpd.Tree, Boolean)] = tree match {
-        case Apply(ExSymbol("scala", "Predef$", "require"), Seq(body)) =>
+        // An optional message may comes after `body`, but we do not make use of it.
+        case Apply(ExSymbol("scala", "Predef$", "require"), body +: _) =>
           Some((body, false))
 
-        case Apply(ExSymbol("stainless", "lang", "StaticChecks$", "require"), Seq(body)) =>
+        // Ditto
+        case Apply(ExSymbol("stainless", "lang", "StaticChecks$", "require"), body +: _) =>
           Some((body, true))
 
         case _ => None
@@ -1106,14 +1108,16 @@ trait ASTExtractors {
 
     object ExEnsuredExpression {
       def unapply(tree: tpd.Tree): Option[(tpd.Tree, tpd.Tree, Boolean)] = tree match {
+        // An optional message may comes after `contract`, but we do not make use of it.
         case ExCall(Some(rec),
           ExSymbol("scala", "Predef$", "Ensuring", "ensuring"),
-          _, Seq(contract)
+          _, contract +: _
         ) => Some((rec, contract, false))
 
+        // Ditto
         case ExCall(Some(rec),
           ExSymbol("stainless", "lang", "StaticChecks$", "Ensuring", "ensuring"),
-          _, Seq(contract)
+          _, contract +: _
         ) => Some((rec, contract, true))
 
         case _ => None
diff --git a/frontends/dotty/src/main/scala/stainless/frontends/dotc/FragmentChecker.scala b/frontends/dotty/src/main/scala/stainless/frontends/dotc/FragmentChecker.scala
index 052290e476..846a657a41 100644
--- a/frontends/dotty/src/main/scala/stainless/frontends/dotc/FragmentChecker.scala
+++ b/frontends/dotty/src/main/scala/stainless/frontends/dotc/FragmentChecker.scala
@@ -247,7 +247,7 @@ class FragmentChecker(inoxCtx: inox.Context)(using override val dottyCtx: DottyC
 
     val RequireMethods =
       defn.ScalaPredefModule.info.decl(Names.termName("require")).alternatives.toSet
-        + Symbols.requiredModule("stainless.lang.StaticChecks").info.decl(Names.termName("require"))
+        ++ Symbols.requiredModule("stainless.lang.StaticChecks").info.decl(Names.termName("require")).alternatives.toSet
 
     private val stainlessReplacement = mutable.Map(
       defn.ListClass -> "stainless.collection.List",
diff --git a/frontends/library/stainless/lang/StaticChecks.scala b/frontends/library/stainless/lang/StaticChecks.scala
index 7e4749d1df..26492947f4 100644
--- a/frontends/library/stainless/lang/StaticChecks.scala
+++ b/frontends/library/stainless/lang/StaticChecks.scala
@@ -6,7 +6,9 @@ object StaticChecks {
 
   @library
   implicit class Ensuring[A](val x: A) extends AnyVal {
-    def ensuring(@ghost cond: (A) => Boolean): A = x
+    def ensuring(@ghost cond: A => Boolean): A = x
+
+    def ensuring(@ghost cond: A => Boolean, msg: => String): A = x
   }
 
   @library @ignore
@@ -28,8 +30,14 @@ object StaticChecks {
   @library
   def require(@ghost pred: => Boolean): Unit = ()
 
+  @library
+  def require(@ghost pred: => Boolean, msg: => String): Unit = ()
+
   @library
   def assert(@ghost pred: => Boolean): Unit = ()
 
+  @library
+  def assert(@ghost pred: => Boolean, msg: => String): Unit = ()
+
 }
 
diff --git a/frontends/scalac/src/main/scala/stainless/frontends/scalac/ASTExtractors.scala b/frontends/scalac/src/main/scala/stainless/frontends/scalac/ASTExtractors.scala
index 9a786815c4..5c8d378581 100644
--- a/frontends/scalac/src/main/scala/stainless/frontends/scalac/ASTExtractors.scala
+++ b/frontends/scalac/src/main/scala/stainless/frontends/scalac/ASTExtractors.scala
@@ -236,14 +236,16 @@ trait ASTExtractors(val global: Global) {
     /** Extracts the 'ensuring' contract from an expression. */
     object ExEnsuredExpression {
       def unapply(tree: Apply): Option[(Tree,Tree,Boolean)] = tree match {
+        // An optional message may comes after `contract`, but we do not make use of it.
         case Apply(Select(Apply(TypeApply(
               ExSelected("scala", "Predef", "Ensuring"),
-              _ :: Nil), body :: Nil), ExNamed("ensuring")), contract :: Nil)
+              _ :: Nil), body :: Nil), ExNamed("ensuring")), contract :: _)
           => Some((body, contract, false))
 
+        // Ditto
         case Apply(Select(Apply(TypeApply(
               ExSelected("stainless", "lang", "StaticChecks", "Ensuring"),
-              _ :: Nil), body :: Nil), ExNamed("ensuring")), contract :: Nil)
+              _ :: Nil), body :: Nil), ExNamed("ensuring")), contract :: _)
           => Some((body, contract, true))
 
         case _ => None
@@ -381,10 +383,12 @@ trait ASTExtractors(val global: Global) {
      * first call in the block). */
     object ExRequiredExpression {
       def unapply(tree: Apply): Option[(Tree, Boolean)] = tree match {
-        case Apply(ExSelected("scala", "Predef", "require"), contractBody :: Nil) =>
+        // An optional message may comes after `contractBody`, but we do not make use of it.
+        case Apply(ExSelected("scala", "Predef", "require"), contractBody :: _) =>
           Some((contractBody, false))
 
-        case Apply(ExSelected("stainless", "lang", "StaticChecks", "require"), contractBody :: Nil) =>
+        // Ditto
+        case Apply(ExSelected("stainless", "lang", "StaticChecks", "require"), contractBody :: _) =>
           Some((contractBody, true))
 
         case _ => None
diff --git a/frontends/scalac/src/main/scala/stainless/frontends/scalac/FragmentChecker.scala b/frontends/scalac/src/main/scala/stainless/frontends/scalac/FragmentChecker.scala
index 63aa62594c..4a76abe01a 100644
--- a/frontends/scalac/src/main/scala/stainless/frontends/scalac/FragmentChecker.scala
+++ b/frontends/scalac/src/main/scala/stainless/frontends/scalac/FragmentChecker.scala
@@ -209,8 +209,8 @@ trait FragmentChecker extends SubComponent { self: StainlessExtraction =>
       ++ rootMirror.getRequiredModule("scala.math.BigInt").info.decl(nme.apply).alternatives).toSet
 
     val RequireMethods =
-      (definitions.PredefModule.info.decl(newTermName("require")).alternatives.toSet
-        + rootMirror.getRequiredModule("stainless.lang.StaticChecks").info.decl(newTermName("require")))
+      definitions.PredefModule.info.decl(newTermName("require")).alternatives.toSet
+        ++ rootMirror.getRequiredModule("stainless.lang.StaticChecks").info.decl(newTermName("require")).alternatives.toSet
 
 
     private val stainlessReplacement = mutable.Map(