A Very Small SAT Solver (From Haskell) Now in Dafny, Proved Correct with LLMs (opens in new tab)

(github.com)

4 pointsnamin4mo ago2 comments

2 comments

2 comments · 1 top-level

vdupras4mo ago· 1 in thread

I asked the LLM whether my program was correct and it answered: you're absolutely right!

naminOP4mo ago

Ha. At least you can check the theorem statements and see that the proofs verify :)

j / k navigate · click thread line to collapse