zlib × Lean November 7, 2026 Languages: EN / ZH Follow the data through the algorithm, then the implementation through the proof. → Inside the V8 Sandbox May 24, 2026 Notes on V8's sandbox threat model, attack boundary, and the browser code that still has to treat sandbox data carefully. → Learning Lean as a Programmer January 14, 2026 Learning Lean from the perspective of a programmer: types as propositions, proofs as programs, and raw induction machinery. → Bitcoin From the Top Down January 10, 2026 Languages: EN / ZH A top-down walkthrough of Bitcoin's data model, from peer-to-peer state to transactions, UTXOs, and script validation. →