diff --git a/README.md b/README.md
index 6d184b5..828fddf 100644
--- a/README.md
+++ b/README.md
@@ -42,6 +42,7 @@ C++
 C#
 CSS
 CUDA
+Dafny
 Dart
 Elixir
 Elm
diff --git a/implementations/main.dfy b/implementations/main.dfy
new file mode 100644
index 0000000..750fb4b
--- /dev/null
+++ b/implementations/main.dfy
@@ -0,0 +1,11 @@
+predicate is_prime(number: int)
+{
+    false
+}
+
+// Because Dafny is a formal verification language, assertions to prove correctness
+// are necessary for the program to have any meaning.
+method {:test} test()
+{
+    assert forall n :: n in [4, 6, 8, 9, 10] ==> !is_prime(n);
+}
diff --git a/optimized_implementations/main.dfy b/optimized_implementations/main.dfy
new file mode 100644
index 0000000..148c24a
--- /dev/null
+++ b/optimized_implementations/main.dfy
@@ -0,0 +1,2 @@
+predicate is_prime(n:int){false}
+method{:test}test(){assert forall n::n in [4,6,8,9,10] ==> !is_prime(n);}