While working on a sideproject I explored lean 4 a bit and figured it actually something that can be very easily integrated into any project if one wants to prove correctness.

The implications of this for AI agents are pretty exciting. I guess you can kind of prove that an agent builds the right thing, no matter the language?

Thanks! This is exactly what I was after for my projects