Divide-before-multiply pattern
Kamino Lend's assessment for RD-F-016 — scored yellow on the v1.7.0 rubric. The evidence below is the curator's reasoning for this score.
Evidence summary #
Certora audit identified a precision loss bug in exchange rate calculations (divide-before-multiply rounding); confirmed patched via Mul-Div pattern. v1.18.0 and v1.19.0 not re-audited for arithmetic paths.
Detail #
The Certora formal verification identified the specific divide-before-multiply analog in fixed-point math (60-bit fractional precision rounding). The fix (Mul-Div pattern with downward rounding) was confirmed implemented. However, v1.18.0 and v1.19.0 have no public re-audit coverage of arithmetic paths. Scored yellow because the known instance was fixed and the audit trail through v1.17.0 is strong, but the two-version gap means this class cannot be affirmatively cleared for current deployed code.
Sources #
- URLCertora Securing Kamino LendingCertora blog — precision loss bug in exchange rate calculations, fixed with Mul-Div patternretrieved 2026-04-27
Methodology #
Determine whether Slither's `divide-before-multiply` detector fires on the deployed verified source.
See the full factor methodology and distribution across all protocols →