diff --git a/assets/why3/assignment05/README.md b/assets/why3/assignment05/README.md
new file mode 100644
index 0000000..245b94f
--- /dev/null
+++ b/assets/why3/assignment05/README.md
@@ -0,0 +1,15 @@
+# Assignment 5: Program correctness and logic
+
+* The primary goal of this assignment is to grasp basic concepts about proving a program's correctness with deductive reasoning.
+
+* You should fill in `TODO`s in three files: `max.mlw`, `binary_search.mlw`, `pascal.mlw`.
+
+* You may use [Why3 in your browser](https://why3.lri.fr/try/). 
+  * Clicking `Verify` button at the top will open a panel on the right side.
+  * For each task in the panel (e.g. `loop invariant preservation`), you can right-click it and run the prover.
+  * Fill in `TODO`s until the prover can verify all tasks, notified with green check-marks.
+
+* To submit your solution, run `./scripts/submit.sh` and submit `assignment05.zip` in the `target` directory to gg.
+
+* More on Why3: <https://why3.lri.fr/doc/index.html>
+* Why3 standard library: <https://why3.lri.fr/stdlib/index.html>