LCLilian Cariouinrasengansec.hashnode.dev·Mar 12 · 19 min readThe Complete Math & Cryptography Reference for Zero-Knowledge Proofs 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 every00
LCLilian Cariouinrasengansec.hashnode.dev·Feb 1 · 14 min readMum, 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...00
LCLilian Cariouinrasengansec.hashnode.dev·Apr 8, 2025 · 3 min readLearning 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...00
LCLilian Cariouinrasengansec.hashnode.dev·Apr 6, 2025 · 2 min readLearning 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...00
LCLilian Cariouinrasengansec.hashnode.dev·Apr 4, 2025 · 5 min readLearning 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...00
