Solidus Builds Verified Solidity Compiler, Launches Optimization Puzzles

Solidus: collaborative automated research project to build formally verified Solidity compiler in Lean. Backend from Yul to EVM is built and verified. Two optimization puzzles launched: Spec Hunt for Solidity 0.8.35 semantics, Compiler Optimization for 3x bytecode reduction vs solc. Took 1,700+ hours, ~$150,000 at API rates. Pre-alpha, unaudited.