From May 1, 2023 to May 12, 2023, Privacy and Scaling Exploration engaged Veridise to review the security of the circuits for Rate Limiting Nullifier. The review covered their Zero Knowledge Circuit (ZK-circuits), written in Circom. Veridise conducted the assessment over 8 person-weeks, with 4 engineers reviewing code over 2 weeks. In response to issues raised by Veridise auditors (RLN-003), the circuits were modified before formal verification. As a result, formal verification was performed on commit 0x10437bc2. The auditing strategy involved a tool-assisted analysis of the source code performed by Veridise engineers as well as extensive manual auditing. In parallel, the auditors wrote specifications of several key correctness properties. Following the manual audit, the Veridise engineers formally verified these properties.