diff --git a/certora/specs/ERC1155Burnable.spec b/certora/specs/ERC1155Burnable.spec
index 3e67c1919..344d25380 100644
--- a/certora/specs/ERC1155Burnable.spec
+++ b/certora/specs/ERC1155Burnable.spec
@@ -1,7 +1,28 @@
+methods {
+    balanceOf(address, uint256) returns uint256 envfree
+    isApprovedForAll(address,address) returns bool envfree
+}
+
+/// If a method call reduces account balances, the caller should be either the 
+/// owner of the account or approved by the owner to act on its behalf.
+rule onlyApprovedCanReduceBalance {
+    address holder; uint256 token; uint256 amount;
+    uint256 balanceBefore = balanceOf(holder, token);
+
+    env e;
+    burn(e, holder, token, amount); // TODO Replace burn with appropriate general function
+
+    uint256 balanceAfter = balanceOf(holder, token);
+
+    assert balanceAfter < balanceBefore => e.msg.sender == holder || isApprovedForAll(holder, e.msg.sender);
+}
+
+/// This rule should always fail.
 rule sanity {
     method f; env e; calldataarg args;
 
     f(e, args);
 
-    assert false;
+    assert false, 
+        "This rule should always fail";
 }
\ No newline at end of file