Welcome to the repository for the Assembly, EVM Opcodes, and Formal Verification Course by Cyfrin Updraft!
This repository houses the written content of our courses, organized to facilitate easy access and contribution from our community. Please refer to this for an in-depth explanation of the content:
- Website - Join Cyfrin Updraft and enjoy 50+ hours of smart contract development courses
- Twitter - Stay updated with the latest course releases
- LinkedIn - Add Updraft to your learning experiences
- Discord - Join a community of 3000+ developers and auditors
- Newsletter - Weekly security research tips and resources to level up your career
- Codehawks - Smart contracts auditing competitions to help securing web3
This was considered part 2 of the security and auditing course, but now, it's it's own living breathing course!
- Assembly, EVM Opcodes, and Formal Verification
- Table of Contents
- Introduction, Resources, and Prerequisites
- Curriculum
- Section 0: Welcome
- Section 1: EVM Assembly, Opcodes, Yul, & Huff | Horse Store
- Section 2: Introduction to Formal Verification & Symbolic Execution | Math Master
- Section 3: Advanced Formal Verification | Gas Bad NFT Marketplace
- Congratulations
- Thank you
⚠️ All code associated with this course is for demo purposes only. They have been audited, but we do not recommend them for production use and should be used at your own risk.
Join Cyfrin Updraft for the best learning experience!
- AI Frens
- ChatGPT
- Just know that it will often get things wrong, but it's very fast!
- Phind
- Like ChatGPT, but it searches the web
- Bard
- Other AI extensions
- ChatGPT
- Github Discussions
- Ask questions and chat about the course here!
- Stack Exchange Ethereum
- Great place for asking technical questions about Ethereum
- Peeranha
- Decentralized Stack Exchange!
- Challenge Contracts (Arbitrum)
- Challenge Contracts (Sepolia)
- It's just numbers 11 -> 13
- The rest are from the security and auditing or the Web3 DevOps course.
An intermediate understanding of solidity. You don't need to be a pro, but you should be familiar with:
We assume you have a solid grasp of the following tools for this course.
- Foundry
- Solidity
- VSCode/Text Editor
- Basic Linux/Unix/Bash terminal commands
- Git & GitHub
- WSL (if you're on windows)
Note: You can get through this course with just having an advanced grasp of solidity & foundry. However, having at least a shallow understanding of security and low-level EVM will make this course much easier to grasp. And you doing the security coruse will make you a better EVM developer!
- Be able to decompile a smart contract right from the raw bytecode
- Be able to understand exactly how EVM opcodes work so you can write more gas-efficient code
- Learn the Huff smart contract programming language
- Be able to write formal verification in Halmos & Certora
- Be able to understand the difference between Fuzzing & Formal Verification
- Have an intermediate understanding of how to write Formal Verification tests for solidity
- TODO: Add link to "how to ask a question" and "how to answer a question" and "how to work with AI"
- Register for Cyfrin Updraft
- USE THIS SITE!!! It's specfically made to make learning easier
- Follow the repository: While going through the course be 100% certain to follow along with the github repository. If you run into in an issue check the chronological-updates in the repo.
- Be Active in the community: Ask questions and engage with other developers going through the course in the discussions tab, be sure to go and say hello or gm! This space is different from the other industries, you don't have to be secretive; communicate, network and learn with others :)
- Learn at your own pace: It doesn't matter if it takes you a day, a week, a month or even a year. Progress >>> Perfection
- Take Breaks: You will exhaust your mind and recall less if you go all out and watch the entire course in one sitting. Suggested Strategy every 25 minutes take a 5 min break, and every 2 hours take a longer 30 min break
- Refer to Documentation: Things are constantly being updated, so whenever Patrick opens up some documentation, open it your end and maybe even have the code sample next to you.
- Use ChatGPT and/or the course chat
🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯
🎯 Exercise: Write yourself a message about why you want this
- This will be important for when things get hard
- Is it money? Save web3? Become someone? Write down as many reasons as possible.
- No section 0 challenge NFT for this one!
🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯🎯
(back to top) ⬆️
🧑🏾💻 Horse Store Code: https://github.com/Cyfrin/1-horse-store-s23
| Horse StoreV1 (Solidity) | Horse StoreV2 (Solidity) |
|---|---|
| View in Remix | View in Remix |
- Huff Documentation
- EVM Opcodes
- View of Places the EVM can hold info
- HEVM
- Foundry libraries
- Introduction to Yul
- Security considerations (compiler doesn’t keep you safe anymore!)
- Introduction to Huff
- Forge debugger
- Tenderly Debugger
- Decompilers
- Metadock
🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴
🐴 Exercises:
- Convert a minimal contract of your own into Huff or Yul
🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴🐴
(back to top) ⬆️
🧑🏾💻 Code: https://github.com/Cyfrin/2-math-master-audit
- What is WAD?
- Introduction to FV & SE
- How to quit concrete testing with FV
- sc-exploits-minimized
- Z3 Solution with AI
- Solidity SMT Checker
- Halmos
- Case Study: PRBMath
click me :)
- Rules
- Harnessing
- Methods Block
- Config Files / Scene
- Linking
- Invariants
- Prover Args
- Path Explosion
- Halting Problem
🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮
🧮 Exercises:
- Attempt to use another FV tool
- Look into the Solady LibClone.sol
- It's a really cool codebase
- Watch this awesome video 🎥
- Audit this! 🪙
- I accidentally verified the helper contract so this one is a bit easier (Arbitrum)
- Since I verified the arbitrum one, I also verified the sepolia one
🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮
(back to top) ⬆️
🧑🏾💻 Code: https://github.com/Cyfrin/3-gas-bad-nft-marketplace-audit
- Parametric rules
- Ghosts
- Hooks
- Dispatching & Summaries
- Sanity
🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮
🧮 Exercises:
- Compete in a formal verification contest!
🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮🧮
(back to top) ⬆️
🎊🎊🎊🎊🎊🎊🎊🎊🎊🎊🎊🎊 Completed The Course! 🎊🎊🎊🎊🎊🎊🎊🎊🎊🎊🎊🎊
Coming soon: The EVM, Assembly, and Formal Verification Course!!
- Competititve Audits
- CodeHawks
- We are working on many things to get you more deals. Stay tuned...
- Code4rena
- Hats Finance
- CodeHawks
- CodeHawks Discord
- Start marketing your services
- Twitter, Farcaster, LinkedIn, etc
- Blogging: Medium, Mirror, etc
- Bug Bounties
- Patrick Collins YouTube
- Solodit
- Block Threat Intelligence (Referral Link)
- Consensys Diligence Newsletter
- Owen Thurm YouTube
- The Red Guild YouTube
- Cyfrin YouTube
The Cyfrin team runs CodeHawks, Cyfrin Updraft, and private security reviews. They are an advisor to the Peeranha project, and run various blockchain nodes like Chainlink & Ethereum. Additionally, they are responsible for the creation of the Aderyn and Solodit tools.
Thanks to everyone who is taking, participating in, and working on this course. These courses are passion project data dumps for everyone in the web3 ecosystem.
Let's level up so we can keep web3 safer, and thank you again for taking this course!
(back to top) ⬆️