## 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/)**