diff --git a/frontends/benchmarks/verification/valid/MonadicTry1.scala b/frontends/benchmarks/verification/valid/MonadicTry1.scala
new file mode 100644
index 000000000..513523c67
--- /dev/null
+++ b/frontends/benchmarks/verification/valid/MonadicTry1.scala
@@ -0,0 +1,19 @@
+/* Copyright 2009-2024 EPFL, Lausanne */
+
+import stainless.lang._
+import stainless.proof._
+
+object MonadicTry1 {
+
+  def success(): Try[Unit] = Success[Unit](())
+  def failure(): Try[Unit] = Failure[Unit](Exception("failure"))
+
+  def checkVal(b: Boolean): Try[Unit] = {
+    if (b) Success[Unit](())
+    else Failure[Unit](Exception("checkVal failed"))
+  } ensuring(res => res match {
+    case Success(_) => b
+    case Failure(_) => !b
+  })
+
+}
diff --git a/frontends/benchmarks/verification/valid/MonadicTry2.scala b/frontends/benchmarks/verification/valid/MonadicTry2.scala
new file mode 100644
index 000000000..52c0b7e10
--- /dev/null
+++ b/frontends/benchmarks/verification/valid/MonadicTry2.scala
@@ -0,0 +1,39 @@
+/* Copyright 2009-2024 EPFL, Lausanne */
+
+import stainless.lang._
+import stainless.proof._
+
+object MonadicTry2 {
+
+  def checkPositive(i: BigInt): Try[BigInt]= {
+    if (i > 0) Success[BigInt](i)
+    else Failure[BigInt](Exception("i is not positive"))
+  } ensuring(res => res match {
+    case Success(ii) => i > 0 && i == ii
+    case Failure(_) => i <= 0
+  })
+
+  def checkEven(i: BigInt): Try[BigInt] = {
+    if (i % 2 == 0) Success[BigInt](i)
+    else Failure[BigInt](Exception("i is not even"))
+  } ensuring(res => res match {
+    case Success(ii) => i % 2 == 0 && i == ii
+    case Failure(_) => i % 2 != 0
+  })
+
+  def checkEvenPositive(i: BigInt): Try[BigInt] = {
+    checkPositive(i).flatMap(ii => checkEven(ii))
+  } ensuring(res => res match {
+    case Success(ii) => i > 0 && i % 2 == 0 && i == ii
+    case Failure(_) => i <= 0 || i % 2 != 0
+  })
+
+  def evenPlusOne(i: BigInt): Try[BigInt] = {
+    checkEven(i).flatMap(ii => checkPositive(ii)).map(ii => ii + 1)
+  } ensuring(res => res match {
+    case Success(ii) => i % 2 == 0 && i > 0 && ii == i  + 1  && ii % 2 == 1
+    case Failure(_) => i % 2 != 0 || i <= 0
+  })
+
+
+}
diff --git a/frontends/library/stainless/lang/package.scala b/frontends/library/stainless/lang/package.scala
index 2f16dcefd..8accfdbe5 100644
--- a/frontends/library/stainless/lang/package.scala
+++ b/frontends/library/stainless/lang/package.scala
@@ -41,6 +41,25 @@ package object lang {
   @library
   abstract class Exception extends Throwable
 
+  @library
+  @extern
+  def Exception(msg: String): Exception = new Exception{}
+
+  @library
+  sealed abstract class Try[T]{
+    def map[U](f: T => U): Try[U] = this match {
+      case Success(t) => Success(f(t))
+      case Failure(exc: Exception) => Failure(exc)
+    }
+
+    def flatMap[U](f: T => Try[U]): Try[U] = this match {
+      case Success(t) => f(t)
+      case Failure(exc: Exception) => Failure(exc)
+    }
+  }
+  @library case class Success[T](t: T) extends Try[T]
+  @library case class Failure[T](exc: Exception) extends Try[T]
+
   @ignore
   implicit class Throwing[T](underlying: => T) {
     def throwing(pred: Exception => Boolean): T = try {