diff --git a/rfc/src/SUMMARY.md b/rfc/src/SUMMARY.md
index 2fb7d0b133cd..0c63cd4242aa 100644
--- a/rfc/src/SUMMARY.md
+++ b/rfc/src/SUMMARY.md
@@ -19,3 +19,4 @@
 - [0011-source-coverage](rfcs/0011-source-coverage.md)
 - [0012-loop-contracts](rfcs/0012-loop-contracts.md)
 - [0013-list](rfcs/0013-list.md)
+- [0014-may-panic-if-attr](rfcs/0014-may-panic-if-attr.md)
diff --git a/rfc/src/rfcs/0014-may-panic-if-attr.md b/rfc/src/rfcs/0014-may-panic-if-attr.md
new file mode 100644
index 000000000000..e4d5ad159f1c
--- /dev/null
+++ b/rfc/src/rfcs/0014-may-panic-if-attr.md
@@ -0,0 +1,75 @@
+- **Feature Name:** Attribute to distinguish safety preconditions from panic freedom (`may-panic-if-attribute`)
+- **Feature Request Issue:** [#3567](https://github.com/model-checking/kani/issues/3567)
+- **RFC PR:** [#3893](https://github.com/model-checking/kani/pull/3893)
+- **Status:** Under Review
+- **Version:** 0
+- **Proof-of-concept:** Not yet
+
+-------------------
+
+## Summary
+
+Kani users want to prove absence of undefined behavior ("safety") while
+distinguishing it from panic freedom.
+
+## User Impact
+
+With the `requires` clauses of function contracts we have enabled modular safety
+verification, permitting users to prove the absence of undefined behavior when
+preconditions are met.
+In some cases, however, users may want to go further and
+1. prove the absence of unexpected panics in presence of expected panics
+   (the presence of the latter can already be demonstrated with the
+   `should_panic` attribute);
+2. formally describe the conditions under which a panic is possible;
+3. prove total correctness by precisely describing the conditions under which a
+   panic occur, upon which the post-conditions are no longer guaranteed.
+
+## User Experience
+
+Users will be able to add an attribute
+`#[kani::may_panic_if(<Boolean expression>)]`
+to any function that has a contract (i.e., at least one of `ensures` or
+`requires`) clause.
+When such an attribute is present, users will add `-Z may-panic-if-attribute` to
+change Kani's verification behavior as follows:
+1. Kani will report successful verification when all properties hold and no
+   panic can occur. (This behavior is unchanged.)
+2. Kani will also report successful verification when all properties hold, no
+   panic occurs when the negation of the condition given with `may_panic_if`
+   holds, yet some panic occurs when the condition holds.
+3. Else Kani reports verification failure. (This behavior is unchanged.)
+
+The following example describes what the overall contract for `unwrap` would
+thus look like:
+```rust
+#[kani::requires(true)] // the function is safe
+#[kani::may_panic_if(self.is_none())]
+#[kani::ensures(|result| Some(result) == self)]
+```
+
+## Software Design
+
+**We recommend that you leave the Software Design section empty for the first version of your RFC**.
+
+Initial implementation suggestion: we will run Kani twice for any such harness
+(unless the condition is trivially `true` or `false`), once while assuming the
+condition (and then checking that no properties other than reachability checks
+fail); if that run succeeded we remove the assumptions and, similarly to
+`should_panic`, check that the only failing properties are panics and not safety
+checks.
+
+## Rationale and alternatives
+
+The linked issue contains suggestions for alternative means to describe panic
+conditions, most notably `panic_if`. This was ruled out as it may at times not
+be possible to exactly describe the conditions under which a panic _must_ occur
+with the syntactic elements in scope at the point of stating the condition.
+
+## Open questions
+
+- Should we permit multiple occurrences of `may_panic_if`?
+
+## Out of scope / Future Improvements
+
+n/a