diff --git a/Makefile b/Makefile
index fb007e3..ad9e18b 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,7 @@
-.PHONY: test test-hash256 test-xof128 test-cxof128 test-aead128
+.PHONY: test test-hash256 test-xof128 test-cxof128 test-aead128 saw-proofs
 
 CRYPTOL ?= cryptol
+SAW ?= saw
 
 test: test-hash256 test-xof128 test-cxof128 test-aead128
 
@@ -15,3 +16,6 @@ test-cxof128:
 
 test-aead128:
 	$(CRYPTOL) -c :exhaust TestAsconAEAD128.cry
+
+saw-proofs:
+	$(SAW) verify.saw
\ No newline at end of file
diff --git a/verify.saw b/verify.saw
new file mode 100644
index 0000000..e541c6c
--- /dev/null
+++ b/verify.saw
@@ -0,0 +1,12 @@
+import "Ascon.cry";
+
+for [0,1,2,16,63,64,65,127,128,129,255,256] (\a ->
+for [0,1,2,16,63,64,65,127,128,129,255,256] (\p -> do {
+    print ("decrypt_encrypt",a,p);
+    prove_print (unint_yices ["Ascon::Ascon_p"]) {{
+        \K N (A : [a]) (P : [p]) ->
+        case AEAD128_decrypt K N A (AEAD128_encrypt K N A P) of
+            None -> False
+            Some p' -> p' == P
+    }};
+}));