diff --git a/mvds.md b/mvds.md
index 3110c3e3..82c4acf2 100644
--- a/mvds.md
+++ b/mvds.md
@@ -15,8 +15,9 @@
     1. [State](#state)
     2. [Flow](#flow)
     3. [Retransmission](#retransmission)
-5. [Footnotes](#footnotes)
-6. [Acknowledgements](#acknowledgements)
+5. [Formal Specification](#formal-Specification)
+6. [Footnotes](#footnotes)
+7. [Acknowledgements](#acknowledgements)
 
 ## Abstract
 
@@ -141,6 +142,10 @@ The record of the type `Type` SHOULD be retransmitted every time `Send Epoch` is
 
 > ***NOTE:** We do not retransmission `ACK`s as we do not know when they have arrived, therefore we simply resend them every time we receive a `MESSAGE`.*
 
+## Formal Specification
+
+MVDS has been formally specified using TLA+: <https://github.com/vacp2p/formalities/tree/master/MVDS>.
+
 ## Footnotes
 
 1. <https://code.briarproject.org/briar/briar-spec/blob/master/protocols/BSP.md>