diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/stdlib_replacement_tests.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/good_contracts/stdlib_replacement_tests.fir.diag.txt
new file mode 100644
index 00000000000000..9ed691b44279b1
--- /dev/null
+++ b/plugins/formal-verification/testData/diagnostics/good_contracts/stdlib_replacement_tests.fir.diag.txt
@@ -0,0 +1,16 @@
+/stdlib_replacement_tests.kt:(151,160): info: Generated Viper text for useRepeat:
+method global$fun_useRepeat$fun_take$$return$T_Unit() returns (ret$0: Ref)
+  ensures dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(ret$0), dom$RuntimeType$unitType())
+  ensures true
+{
+  var ret$1: Ref
+  var anonymous$0: Ref
+  var ret$2: Ref
+  var anonymous$1: Ref
+  ret$0 := dom$RuntimeType$unitValue()
+  anonymous$0 := dom$RuntimeType$boolToRef(true)
+  label label$ret$1
+  anonymous$1 := dom$RuntimeType$boolToRef(true)
+  label label$ret$2
+  label label$ret$0
+}
diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/stdlib_replacement_tests.kt b/plugins/formal-verification/testData/diagnostics/good_contracts/stdlib_replacement_tests.kt
new file mode 100644
index 00000000000000..abe7fe347cb277
--- /dev/null
+++ b/plugins/formal-verification/testData/diagnostics/good_contracts/stdlib_replacement_tests.kt
@@ -0,0 +1,17 @@
+// REPLACE_STDLIB_EXTENSIONS
+
+import kotlin.contracts.contract
+import kotlin.contracts.ExperimentalContracts
+
+@OptIn(ExperimentalContracts::class)
+fun <!VIPER_TEXT!>useRepeat<!>(): Unit {
+    contract {
+        returns()
+    }
+    check(true)
+    check(true) { "Lazy message" }
+}
+
+// TODO: add test for `repeat` (we actually have a bug there because we require unsatisfied precondition in loops)
+
+// TODO: add tests for `let`, `apply`, `with`, `run`, `also`
diff --git a/plugins/formal-verification/testData/stdlibReplacements.kt b/plugins/formal-verification/testData/stdlibReplacements.kt
index 6cdbed45bc37b9..4184c246074ccf 100644
--- a/plugins/formal-verification/testData/stdlibReplacements.kt
+++ b/plugins/formal-verification/testData/stdlibReplacements.kt
@@ -1,4 +1,5 @@
 import org.jetbrains.kotlin.formver.plugin.NeverConvert
+import org.jetbrains.kotlin.formver.plugin.verify
 
 @NeverConvert
 inline fun <T> run(block: () -> T): T = block()
@@ -23,3 +24,23 @@ inline fun <T> T.apply(block: T.() -> Unit): T = {
 
 @NeverConvert
 inline fun <T, R> with(receiver: T, block: T.() -> R): R = receiver.block()
+
+@NeverConvert
+inline fun repeat(times: Int, action: (Int) -> Unit) {
+    var counter: Int = 0
+    while (counter < times) {
+        action(counter)
+        counter = counter + 1
+    }
+}
+
+// `check`s are intended for runtime, we have our own `verify` to check static properties
+@NeverConvert
+inline fun check(value: Boolean) {
+}
+
+@NeverConvert
+inline fun check(value: Boolean, lazyMessage: () -> Any) {
+}
+
+
diff --git a/plugins/formal-verification/tests-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java b/plugins/formal-verification/tests-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java
index 4854b9eec27b52..38154ea9acfdd7 100644
--- a/plugins/formal-verification/tests-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java
+++ b/plugins/formal-verification/tests-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java
@@ -192,6 +192,12 @@ public void testReturns_null() {
     public void testSimple() {
       runTest("plugins/formal-verification/testData/diagnostics/good_contracts/simple.kt");
     }
+
+    @Test
+    @TestMetadata("stdlib_replacement_tests.kt")
+    public void testStdlib_replacement_tests() {
+      runTest("plugins/formal-verification/testData/diagnostics/good_contracts/stdlib_replacement_tests.kt");
+    }
   }
 
   @Nested