diff git a/CHANGELOG.md b/CHANGELOG.md
index 928f2ae5bd844d48ceaa8ac255e949d482ae376c..892ad8cc2dfd8338ed0d984388edb083cdcc0623 100644
 a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ 7,26 +7,30 @@ Coq development, but not every APIbreaking change is listed. Changes marked
* [#] View shifts are radically simplified to just internalize framepreserving
updates. Weakestpre is defined inside the logic, and invariants and view
 shifts with masks are also coded up inside Iris.
+ shifts with masks are also coded up inside Iris. Adequacy of weakestpre
+ is proven in the logic.
* [#] The language can now fork off multiple threads at once.
## Iris 2.0
This version accompanies the final ICFP paper.

* [algebra] Make the core of an RA or CMRA a partial function.
* [heap_lang] No longer use dependent types for expressions. Instead, values
carry a proof of closedness. Substitution, closedness and valueness proofs
are performed by computation after reflecting into a term langauge that knows
about values and closed expressions.
* [program_logic/language] The language does not define its own "atomic"
predicate. Instead, atomicity is defined as reducing in one step to a value.
+* [program_logic] Due to a lack of maintenance and usefulness, lifting lemmas
+ for Hoare triples are removed.
+
+## Iris 2.0rc2
+
+This version matches the final ICFP paper.
+
+* [algebra] Make the core of an RA or CMRA a partial function.
* [program_logic/lifting] Lifting lemmas no longer roundtrip through a
userchosen predicate to define the configurations we can reduce to; they
directly relate to the operational semantics. This is equivalent and
much simpler to read.
 Due to a lack of maintenance and usefulness, lifting lemmas for Hoare triples
 are removed.
## Iris 2.0rc1