I formally proved an important 2025 CS paper (which I did not write) in Lean last month, it took like 2 or 3 weeks of intermittently poking at claude to keep going. AFAIK, it is the first rust-like borrow checker completely formally proven in Lean.

I'm currently using it as a basis for building a systems language with Rust's memory guarantees, but with new features like generators and co-routines, and effects instead of colored functions. The fact that the borrow checker's properties are formally proven means I can trust more of what Claude is doing than you normally would be able to do.