this post was submitted on 07 Jul 2025
1 points (100.0% liked)

Formal Methods

190 readers
1 users here now

founded 2 years ago
MODERATORS
 

One of the many exciting new features in the upcoming Lean 4.22 release is a preview of the new verification infrastructure for proving properties of imperative programs. In this post, I’ll take a first look at this feature, show a simple example of what it can do, and compare it to similar tools.

no comments (yet)
sorted by: hot top controversial new old
there doesn't seem to be anything here