_Follow along with this video:_ --- ### Course Introduction Welcome to the ultimate **Assembly, EVM Opcode and Formal Verification** course! Once upon a time, this was intended to be Part 2 of the security course, but this course contained a lot more general knowledge than security researchers may be interested in, so I decided to split this into its own thing. With that said, this course is pretty intense and is for those developers and security researchers that want to hit the `top 1%` of their field. We'll be covering a number of advanced concepts such as: ### Contract Disassembly and Opcodes We'll learn all about the `EVM` and the `Opcodes` that power it. We're going to get low level and code our own implementations of contracts written in `Yul`, `Huff` and `Assembly`. Through the exercises in this course, you'll walk away being able to read low-level code and super gas optimize your protocols. As always on `Cyfrin Updraft`, we'll accomplish this through project based work and the completion of 3 projects which we'll dive deep into. - **Horse Store**: Learn how to use `Huff` to optimize a smart contract protocol - **Math Masters**: Leverage `Formal Verification` to mathematically prove the results of low-level code - **Gas Bad Nft Marketplace**: Using Certora `Formal Verification`, compare `Solidity` and `Assembly` implementations of the same code base to assure identical functionality and save users gas! ### Formal Verification If you're taking this course, you should already be familiar with `fuzzing`. `Fuzzing` should always be a step taken _before_ `formal verification`. `Fuzzing` is a powerful tool in testing a wide range of possible scenarios, but `formal verification` will mathematically prove or disprove if a situation exists in which an invariant can break. `Formal Verification` comes with its own set of pros and cons, but I believe the future of smart contract development will be comprised of `formal verification and fuzzing testing` standards as these methodologies become easier and easier to employ. We'll be learning about 2 very powerful `formal verification` tools, `Halmos` and `Certora`. ### Motivations Now, this course is going to be much more advanced/low-level than the other content on `Updraft`, the tone may be a little more serious (but I promise we'll still have fun). In the real-world, you'll see `Assembly` and `Yul` implemented for one reason or another _all the time_, so it's important to know these things and to be familiar with them if you hope to expand your skill set in the space. The value of knowing how to formally verify a protocol can be seen regardless of your ultimate goals. Including `formal verification` in your test suite as a developer will only enhance the security of your project, and as a security researcher ... well some have leveraged these tools to snag some serious audit and bug bounty pay outs. ### Wrap Up As I mentioned, this is going to be the most advanced content we've offered yet and it's specifically tailered to those of you who want to take their development or their security skills to the next level A sincere thank you for taking this course. This is how we scale Web3 in a sustainable and secure way. Let's get started with best practices, in the next lesson. See you soon!