[namin]

Thanks, we will provide case studies. Already today, lemmafit doesn't need familiarity with Dafny. It is used under the hood, so you just use Claude Code normally and lemmafit adds the verification harness. You don't need to interact with Dafny or the proofs at all.