From e65a52a250f586ab093b02e89f346bb11a88b22a Mon Sep 17 00:00:00 2001
From: Josef Widder <44643235+josef-widder@users.noreply.github.com>
Date: Fri, 28 Jun 2024 11:42:02 +0200
Subject: [PATCH] Add links to new documents

---
 specs/english/forced-updates/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/specs/english/forced-updates/README.md b/specs/english/forced-updates/README.md
index ca90577fa..63432ae84 100644
--- a/specs/english/forced-updates/README.md
+++ b/specs/english/forced-updates/README.md
@@ -141,7 +141,7 @@ Once L2 is rolled-back to latest L2's provenHeight, say h, a new block is append
 
 ### Invariants and temporal formulas
 
-For details we refer to the Quint file, and the upcoming analysis documentation (Points (c) and (d) in the SoW. TODO).
+For details we refer to the [state machine in Quint](https://github.com/informalsystems/malachite/blob/main/specs/quint/specs/reset/resetSystem.qnt), and the [analysis documentation](https://github.com/informalsystems/malachite/blob/main/specs/quint/specs/reset/README.md).
 
 ## Issues