diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6cdea08d79f189fdcb5962578a19da5586ac4c04..aff5d2f3f046f1c2f0702d843251c4b71765c5e4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,10 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 
 ## Iris master
 
+Changes in and extensions of the theory:
+
+* [#] Weakestpre for total program correctness.
+
 Changes in Coq:
 
 * Rename `timelessP` -> `timeless` (projection of the `Timeless` class)