rasengansec.hashnode.devMum, I'm auditing a math heavy codebase, what do I do ?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...Feb 1·14 min read
rasengansec.hashnode.devLearning CVL Language (Part 4)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...Apr 8, 2025·3 min read
rasengansec.hashnode.devLearning CVL Language (Part 3)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...Apr 6, 2025·2 min read
rasengansec.hashnode.devLearning Certora Prover (Part 2)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...Apr 4, 2025·5 min read
rasengansec.hashnode.devLearning Certora Prover (Part 1)Introduction Predicates, propositional logic and quantifiers are basic concepts of mathematical logic useful and needed when doing formal verification. Propositional Logic : basis of mathematical logic, dealing with boolean variables and operations....Mar 29, 2025·5 min read
