diff --git a/specs/BitSnark.tla b/specs/BitSnark.tla
index d6d5180..1fd4d56 100644
--- a/specs/BitSnark.tla
+++ b/specs/BitSnark.tla
@@ -61,7 +61,7 @@ StartingBalances ==
      prover |-> PROVER_STAKE,
      verifier |-> VERIFIER_PAYMENT]
 
-IsProofValid == CHOOSE v \in {TRUE, FALSE} : TRUE
+IsProofValid == FALSE
 
 Init ==
     /\ outputs = {"Stakable Funds", "Payable Funds", "Locked Funds"}
@@ -227,6 +227,10 @@ Safe ==
 
 THEOREM Spec => [] Safe
 
+(* An invalid proof must never consume the externally locked funds. *)
+InvalidProofSafety ==
+    IsProofValid \/ "Locked Funds" \in outputs
+
 
 (* Liveness Helpers. *)