diff --git a/Audit-and-Testing.md b/Audit-and-Testing.md
index 6c97ab9..f487cd1 100644
--- a/Audit-and-Testing.md
+++ b/Audit-and-Testing.md
@@ -2,6 +2,14 @@
 
 Trust signals for evaluating libsoliton's reliability and security posture.
 
+## Formal Verification
+
+8 Tamarin models (55 lemmas) and 5 CryptoVerif models (7 queries) provide
+machine-checked proofs of all 13 security theorems from the
+[Formal Analysis](Formal-Analysis) specification. See
+**[Formal Verification](Formal-Verification)** for full results, bounds,
+and reproduction instructions.
+
 ## Test Suite
 
 | Location | Count | Description |