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

2 comments

• $vdupras 9 hours ago

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

  [-]
  • $namin 9 hours ago

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