The AI auditor ended up flagging a medium that two audits missed. A malicious proposal can permanently brick the timelock by setting the expiration period to uint256 max, which stops all future and current proposals from being executed.

We ran the auditor mode against the @KleidiWallet codebase benchmarked at the commit before our @code4rena audit.

@Certora recently launched their newest AI Auditor, and we wanted to try it out. When tested against a codebase our engineers developed, it surfaced a unique vulnerability two rounds of audits missed!! Let's dive in.

A useful mental model for thinking about security is a stack of tools, processes, and procedures used to find bugs, with each type deployed at different stages of the development lifecycle. The lower in the stack a tool or process, typically the cheaper it is to find bugs.