Round 1 Q1 2025

The Saturation library had the lowest finding per line of code and so we engaged with a formal verification team to focus specifically on this library (half the code base) due to the complexity.

Pruvendo added Lean formal verification for the library and added 2,313 new tests, which included both invariant and fuzz tests.

Pruvendo: formal verification and security audit suite
Comprehensive fuzz testing, formal verification, and security audit
for Ammalgam protocol, developed by Pruvendo.

Test suite (2313 tests):
- test/spec/: 2001 tests across 15 modules (Saturation, Liquidation,
  GeometricTWAP, Validation, Interest, Pair, Convert, TickMath,
  QuadraticSwapFees, DebtToken, TokenController, Constants,
  TokenSymbol, Proxy, Uint16Set)
- test/audit/: 305 tests (findings PoC + QC investigations)
- 870 formalized invariants (INV-XXX markers)
- 225 reference implementations (REF-XXX markers)

Lean 4 formal specification:
- Definitions: Saturation, Liquidation, Pricing, Solvency
- Proofs: SaturationProofs (20 files), LiquidationProofs (10 files),
  LiquidationBoundaryProofs, PricingProofs, SolvencyProofs

Security findings (22 total):
- 6 FIXED: AUDIT-005, 006, 012, 013, 014a, 014c
- 6 CONFIRMED (open): AUDIT-015, 016, 017, 018, 019, 021
- 1 OPEN (defense-in-depth): AUDIT-014b
- 2 FUNCTION-ONLY: AUDIT-004, 020
- 1 DESIGN ISSUE: AUDIT-001
- 1 BY DESIGN: AUDIT-002
- 6 NOT A BUG: AUDIT-003, 007, 008, 009, 010, 011

AI Scanners

It is important to note that AI scanners can have a high false positive rate. We have used our own internal tools to eliminate 80% or more of these findings as false positives or duplicates, and we continue to review the findings to identify potential issues. However, many issues found in our manual review and formal verification were also caught by these tools as well.