Crellvm: verifying LLVM optimisations with Coq: https://sf.snu.ac.kr/crellvm/
Impressively, they find bugs with optimisation passes which showed no bugs with fuzz testing!
Related Posts
Bril is a cute intermediate language for teaching (think simplified LLVM IR): https://www.cs.cornell.edu/~asampson/blog/bril.html
The idea of providing a standard JSON format to help students write basic passes is really elegant.
I've started keeping a list of particularly interesting bugs and patches that I've worked on: https://github.com/Wilfred/interesting-code
The time that I once removed *a single closing paren* in Emacs is still my favourite.
Do any tech streamers try new software live? It'd be a really fun way of doing UX testing.