diff --git a/README.md b/README.md
index 2a7c110..341f1a2 100644
--- a/README.md
+++ b/README.md
@@ -35,19 +35,19 @@ The directory `tools` contains the version of KeY to be used for the tutorial.
 
 ### Interactively
 
-If you want to run KeY interactively, the KeY UI can be started by launcing the jar file, e.g., using the command
+If you want to run KeY interactively, the KeY UI can be started by launching the jar file, e.g., using the command
 ```
 $ java -jar tools/key-2.13.0-exe.jar
 ```
-or using the shell script `startkey.sh` in the toplevel directory.
+or using the shell script `startkey.sh` in the toplevel directory which suppresses some log messages.
 
 When the UI opens[^1] you can load a project (via the menu File > Open). Choose one of the `project.key` files from the example directories to load one of the two examples. A window will open afterwards from which you can choose which contract you would like to verify. For an introduction and tips on how to use the system, see the tutorial notes and videos for details (links at the tutorial page mentioned above).
 
 [^1]: It may be that you have to close the example choice window first.
 
-### Verifying from the commandline
+### Verifying from the command line
 
-In case you want to verify the examples fully automatically from the command line, the repository also contains linux shell scripts that can do this.
+In case you want to verify the examples fully automatically from the command line, the repository also contains Linux shell scripts that can do this.
 You can use the command
 ```
 $ cd BinarySearch; ./prove.sh
@@ -56,36 +56,8 @@ for the binary search example and the command
 ```
 $ cd ArrayList; ./prove.sh
 ```
-for the list example.
+for the list example. Both commands should w/o errors. The last should be
 
-**License: GPL-v2-only**
+> "[INFO] Summary for project.key: (successful/ignored/failure) (X/0/0)"
 
-## TODOs
-
-Deadline: next kakey meeting, 21.06.2024
-
-* MU:
-  * Readme
-    * [x] Add link to the FM tutorial webpage
-    * [x] Description of the two case studies.
-    * [x] Interactive use
-  * [x] Beweis von sort()
-  * [x] Beweis von List::add():
-  
-* AW: 
-  * [ ] Zenodo DOI, vorbereitet, upload fehlt
-        Reserved DOI: 10.5281/zenodo.11669182
-  * [x] Log level
-  * [ ] Proof reading: Readme
-
-* RB: 
-  * [ ] tentative screencast on the FM tutoral web page.
-  * [ ] Beweis von List::add()
-  
-* WP:
-  * [ ] seqSwap auf main
-  * [ ] Integer Semantics/Overflows
-  * [x] Test[Test::test()].JML normal_behavior operation contract.0
-    Test::test() w/o Z3
-  
-  
+**License: GPL-v2-only**