From 098a4ddf8ff5c4449a61051c42a1a2527adc0531 Mon Sep 17 00:00:00 2001
From: kamal <kamal@noreply-vcs@mail.lo.sh>
Date: Thu, 23 Apr 2026 05:15:47 +0000
Subject: [PATCH] Update Audit and Testing

---
 Audit-and-Testing.md | 8 ++++++++
 1 file changed, 8 insertions(+)

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 |