diff --git a/src/main/java/org/cprover/MustNotThrow.java b/src/main/java/org/cprover/MustNotThrow.java
new file mode 100644
index 0000000..7be14b1
--- /dev/null
+++ b/src/main/java/org/cprover/MustNotThrow.java
@@ -0,0 +1,8 @@
+package org.cprover;
+
+/**
+ * This can be added to methods to indicate they aren't allowed to throw
+ * exceptions. JBMC and related tools will truncate any execution path on which
+ * they do with an ASSUME FALSE instruction.
+ */
+public @interface MustNotThrow { }