diff --git a/prompts/dafny_eval/ask_for_fixed.txt b/prompts/dafny_eval/ask_for_fixed.txt
new file mode 100644
index 0000000..cbb6770
--- /dev/null
+++ b/prompts/dafny_eval/ask_for_fixed.txt
@@ -0,0 +1,5 @@
+This answer got Dafny verification error:
+{error}
+Please try again by taking the Dafny feedback.
+
+If an error appears in one of method ending with `_valid`, that means annotations of an existing function were altered.
diff --git a/prompts/dafny_eval/rewrite.txt b/prompts/dafny_eval/rewrite.txt
new file mode 100644
index 0000000..97b3c00
--- /dev/null
+++ b/prompts/dafny_eval/rewrite.txt
@@ -0,0 +1,6 @@
+Given a Dafny program with function signature, preconditions, postconditions, and code, but with annotations missing.
+Please return a complete Dafny program with the strongest possible annotations (loop invariants, assert statements, etc.) filled back in.
+Do not explain.
+Please use exactly the same function signature, preconditions, and postconditions. Do not ever modify the given lines.
+Below is the program:
+{program}
diff --git a/prompts/dafny_eval/sys.txt b/prompts/dafny_eval/sys.txt
new file mode 100644
index 0000000..43043a1
--- /dev/null
+++ b/prompts/dafny_eval/sys.txt
@@ -0,0 +1,3 @@
+You are an expert in Dafny.
+You will be given tasks dealing with Dafny programs including precise annotations.
+You respond only with code blocks.
\ No newline at end of file
diff --git a/prompts/dafny_eval_comment/ask_for_fixed.txt b/prompts/dafny_eval_comment/ask_for_fixed.txt
new file mode 100644
index 0000000..cbb6770
--- /dev/null
+++ b/prompts/dafny_eval_comment/ask_for_fixed.txt
@@ -0,0 +1,5 @@
+This answer got Dafny verification error:
+{error}
+Please try again by taking the Dafny feedback.
+
+If an error appears in one of method ending with `_valid`, that means annotations of an existing function were altered.
diff --git a/prompts/dafny_eval_comment/rewrite.txt b/prompts/dafny_eval_comment/rewrite.txt
new file mode 100644
index 0000000..399fb93
--- /dev/null
+++ b/prompts/dafny_eval_comment/rewrite.txt
@@ -0,0 +1,6 @@
+Given a Dafny program with function signature, preconditions, postconditions, and code, but with annotations missing.
+Please return a complete Dafny program with the strongest possible annotations (loop invariants, assert statements, etc.) filled back in.
+Use extensive comments in the code, but don't explain anything outside of it.
+Please use exactly the same function signature, preconditions, and postconditions. Do not ever modify the given lines.
+Below is the program:
+{program}
diff --git a/prompts/dafny_eval_comment/sys.txt b/prompts/dafny_eval_comment/sys.txt
new file mode 100644
index 0000000..6522a1c
--- /dev/null
+++ b/prompts/dafny_eval_comment/sys.txt
@@ -0,0 +1,4 @@
+You are an expert in Dafny.
+You will be given tasks dealing with Dafny programs including precise annotations.
+You respond only with code blocks.
+You will write a comment explaining each significant point of the program on a line before.
\ No newline at end of file
diff --git a/prompts/dafny_eval_comment_without_impls/ask_for_fixed.txt b/prompts/dafny_eval_comment_without_impls/ask_for_fixed.txt
new file mode 100644
index 0000000..cbb6770
--- /dev/null
+++ b/prompts/dafny_eval_comment_without_impls/ask_for_fixed.txt
@@ -0,0 +1,5 @@
+This answer got Dafny verification error:
+{error}
+Please try again by taking the Dafny feedback.
+
+If an error appears in one of method ending with `_valid`, that means annotations of an existing function were altered.
diff --git a/prompts/dafny_eval_comment_without_impls/rewrite.txt b/prompts/dafny_eval_comment_without_impls/rewrite.txt
new file mode 100644
index 0000000..8d5718d
--- /dev/null
+++ b/prompts/dafny_eval_comment_without_impls/rewrite.txt
@@ -0,0 +1,6 @@
+Given a Dafny program with function signature, preconditions and postconditions, but with some implementations and annotations missing.
+Please return a complete Dafny program with all functions implemented, and annotated using the strongest possible annotations (loop invariants, assert statements, etc.).
+Use extensive comments in the code, but don't explain anything outside of it.
+Please use exactly the same function signature, preconditions, and postconditions. Do not ever modify the given lines.
+Below is the program:
+{program}
diff --git a/prompts/dafny_eval_comment_without_impls/sys.txt b/prompts/dafny_eval_comment_without_impls/sys.txt
new file mode 100644
index 0000000..6522a1c
--- /dev/null
+++ b/prompts/dafny_eval_comment_without_impls/sys.txt
@@ -0,0 +1,4 @@
+You are an expert in Dafny.
+You will be given tasks dealing with Dafny programs including precise annotations.
+You respond only with code blocks.
+You will write a comment explaining each significant point of the program on a line before.
\ No newline at end of file