I'm excited to announce `waterfall`, a new Lean tactic for ACL2-style automated proof search. It can automatically find proofs of the kind we do a lot in formal PL and software verification: lots of induction over data structures, case analysis, etc. samth.github.io/waterfall/
9
19
198
8,436
The whole idea is that you just write `waterfall` and then it proves the goal. Many PL proofs involve lots of annoying cases, none of which say that much that's interesting. I hope waterfall can make these proofs easier to write.
1
1
21
680
I've spent a lot of time with my automated friends developing this over the past several months, and much longer dreaming about creating this. It's finally a small core proof search engine, and I'm excited to see if it's useful for other people as well.

Sep 16, 2026 · 8:22 PM UTC

2
1
23
524
Sort replies: Relevant Recent Liked
Replying to @samth
the last example is a banger. big if true this looks so useful! can you ask your models to try applying this across CSlib / Langlib to see if it reduces proofs significantly?
1
1
33
This prompted me to try using the module system. :)
1
1
10
more replies
Replying to @samth
Repo could use a little cleanup. Some of the analysis artifacts that read like slop/AI psychosis, which makes me wonder if the options/tests are carrying their weight or Astra's inability to delete code. Very good idea at a high level, though :>
1
31
The options are all deliberately chosen. But I agree that some of those notes don't need to be in the repo. Nice username, btw.
1
18