diff --git a/hacking_tools/formal_ verification/README.md b/hacking_tools/formal_ verification/README.md
new file mode 100644
index 0000000..6497181
--- /dev/null
+++ b/hacking_tools/formal_ verification/README.md	
@@ -0,0 +1,38 @@
+## formal verification
+
+<br>
+
+### tl; dr
+
+<br>
+
+#### yul
+
+<br>
+
+* yul (previously also called julia) is an intermediate statically-typed language that can be compiled to bytecode for different backends. 
+* it's a good target for high-level optimisation stages, as it provides flexibility, speed, and interoperates easily with high-level solidity.
+* programs written in yul are readable even if the code is generated by a compiler from solidity. 
+* because yul needs to be compiled to bytecode, it requires additional time to complete the entire compilation process, making it time-consuming during development.
+
+<br>
+
+<p align="center">
+<img src="https://user-images.githubusercontent.com/1130416/219821226-9f9b8a05-7d66-4d34-841e-774e0365d50c.png" width="70%" align="center" style="padding:1px;border:1px solid black;" />
+</p>
+
+<br>
+
+----
+
+### external resources
+
+<br>
+
+* **[lean prover](https://leanprover.github.io/)**
+* **[solidity docs on yul](https://docs.soliditylang.org/en/v0.8.18/yul.html)**
+* **[evm.codes (evm opcodes, by fork)](https://www.evm.codes/?fork=arrowGlacier)**
+* **[solady, optimized solidy snippets](https://github.com/Vectorized/solady)**
+* **[the darks arts of yul, by vectorized](https://www.youtube.com/watch?v=ew3pfnb2_V8)**
+* **[optimising gas efficient whitelist contract in yul, by 0xmonsoon](https://mirror.xyz/0xCdC75C7d65d5c4cD0329DA74f979C6E1613d57A5/0ZsbpDeEzQhqFNRnsJhhkmPg1oXJCxH0SMkr5EZbaNc)**
+* **[ethernaut solutions in yul](https://github.com/teddav/ethernaut-yul/)**