A Very Small SAT Solver (From Haskell) Now in Dafny, Proved Correct with LLMs(github.com)

4 pointsby naminil y a 5 mois2 comments

https://github.com/namin/dafny-sandbox/blob/master/Sat.dfy

2 comments

vduprasil y a 5 mois

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

naminil y a 5 mois

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