Formal Verification in Any Language for Everybody (lean 4)

#1

Post by wazHFsRy » Thu, Apr 09, 2026, 4:56 AM UTC

Formal Verification in Any Language for Everybody (lean 4)
dev-log.me

Re: Formal Verification in Any Language for Everybody (lean 4)

#2

Post by wazHFsRy » Thu, Apr 09, 2026, 4:56 AM UTC

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.

Re: Formal Verification in Any Language for Everybody (lean 4)

#3

Post by yfk999 » Thu, Apr 09, 2026, 5:00 AM UTC

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?

Re: Formal Verification in Any Language for Everybody (lean 4)

#4

Post by Freewheelin » Thu, Apr 09, 2026, 5:49 AM UTC

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

Re: Formal Verification in Any Language for Everybody (lean 4)

#5

Post by wazHFsRy » Thu, Apr 09, 2026, 6:08 AM UTC

Freewheelin wrote: post #4

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

Awesome, I am finding so little actual experience reports on this, if you build something similar, I'd be very happy to hear about how it's going. Feel free to reach out directly to me.