diff --git a/docs/spec/lightclient/README.md b/docs/spec/lightclient/README.md
index 0dfd11c67..08af28cce 100644
--- a/docs/spec/lightclient/README.md
+++ b/docs/spec/lightclient/README.md
@@ -65,11 +65,7 @@ $DIR/apalache-tests/scripts/parse-logs.py --human .
 ```
 
 The following table summarizes the experimental results. The TLA+ properties can be found in the
-[TLA+ specification](verification/Lightclient_A_1.tla). 
- The experiments were run in an AWS instance equipped with 32GB
-RAM and a 4-core Intel® Xeon® CPU E5-2686 v4 @ 2.30GHz CPU.
-We write “✗=k” when a bug is reported at depth k, and “✓<=k” when
-no bug is reported up to depth k.
+[TLA+ specification](verification/Lightclient_A_1.tla).
 
 ![Experimental results](experiments.png)
 
diff --git a/docs/spec/lightclient/verification/verification.md b/docs/spec/lightclient/verification/verification.md
index 575a82531..5444d7df3 100644
--- a/docs/spec/lightclient/verification/verification.md
+++ b/docs/spec/lightclient/verification/verification.md
@@ -1179,15 +1179,15 @@ func Main (primary PeerID, lightStore LightStore, targetHeight Height)
 
 [block]: https://github.com/tendermint/spec/blob/d46cd7f573a2c6a2399fcab2cde981330aa63f37/spec/core/data_structures.md
 
-[TMBC-HEADER-link]: #tmbc-header1
-[TMBC-SEQ-link]: #tmbc-seq1
-[TMBC-CorrFull-link]: #tmbc-corr-full1
-[TMBC-Auth-Byz-link]: #tmbc-auth-byz1
-[TMBC-TIME_PARAMS-link]: tmbc-time-params1
-[TMBC-FM-2THIRDS-link]: #tmbc-fm-2thirds1
-[TMBC-VAL-CONTAINS-CORR-link]: tmbc-val-contains-corr1
-[TMBC-VAL-COMMIT-link]: #tmbc-val-commit1
-[TMBC-SOUND-DISTR-POSS-COMMIT-link]: #tmbc-sound-distr-poss-commit1
+[TMBC-HEADER-link]: #tmbc-header.1
+[TMBC-SEQ-link]: #tmbc-seq.1
+[TMBC-CorrFull-link]: #tmbc-corr-full.1
+[TMBC-Auth-Byz-link]: #tmbc-auth-byz.1
+[TMBC-TIME_PARAMS-link]: tmbc-time-params.1
+[TMBC-FM-2THIRDS-link]: #tmbc-fm-2thirds.1
+[TMBC-VAL-CONTAINS-CORR-link]: tmbc-val-contains-corr.1
+[TMBC-VAL-COMMIT-link]: #tmbc-val-commit.1
+[TMBC-SOUND-DISTR-POSS-COMMIT-link]: #tmbc-sound-distr-poss-commit.1
 
 [lightclient]: https://github.com/interchainio/tendermint-rs/blob/e2cb9aca0b95430fca2eac154edddc9588038982/docs/architecture/adr-002-lite-client.md
 [fork-detector]: https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/detection.md