@0xlil
smart contract auditor
Nothing here yet.
Nothing here yet.
Mar 12 · 19 min read · Currently I'm deep in the ZK security rabbit hole. I've spent months going through the math, the circuits, the protocolsn and honestly, the hardest part isn't any single concept. It's seeing how every
Join discussionFeb 1 · 14 min read · I spent 3 days including saturday and sunday deriving formulas from the Gyro ECLP whitepaper. Line by line. Variable by variable. By Sunday night, I understood the math beautifully, and had found exactly zero bugs. That weekend taught me something im...
Join discussion
Apr 8, 2025 · 3 min read · Formal verification is critical for ensuring smart contract security. Certora Verification Language (CVL) provides powerful tools for this task, with ghost variables and storage hooks being especially useful for tracking contract state and proving co...
Join discussion
Apr 6, 2025 · 2 min read · Key Formal Verification Concepts for Smart Contracts 1. Logical Implications and Direction The direction of logical implications is crucial. Consider a rule restricting actions to owners: // Incorrect: Only checks if owners can change supply assert o...
Join discussion
Apr 4, 2025 · 5 min read · Preconditions By adding preconditions, one can eliminate infeasible states and put constraints on values. The Rule totalSupplyAfterMintWithPrecondition is a copy of totalSupplyAfterMint with an additional constraint, shown in emphasis below: /** @tit...
Join discussion
