Viewing profile — namin

I created LemmaScript to compile TypeScript to a verification backend (Dafny or Lean) and prove properties on the systematically derived model. I'll keep developing this, but I hav…

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…

Since around Opus 4.5, systems like Claude Code are very good at Dafny proofs. They don’t get everything right in one shot but can iterate with verifier feedback. Some proofs take …

Hey HN! We've been experimenting with Dafny formal verification in web apps. We've been using AI to write verified state machines, proving undo/redo preserves invariants, verifying…

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

Harvard SEAS | https://metareflection.seas.harvard.edu and https://namin.seas.harvard.edu | Postdoctoral Fellow | Greater Boston Area | ONSITE I am looking for a postdoctoral fello…

I want to share this live playground for FOL, an old system from the late 70s. It has many precursor ideas about reasoning at the meta-level, including the now common proof by refl…

Harvard SEAS, ONSITE (Boston area, MA, US) I have one opening in a new project around AI for precision medicine. One thrust is about combining biomedical knowledge graphs and large…

Awesome, thank you! I'll check it out.

This seems cool! Is there a way to try it locally with an open LLM? If you provide a way to set the OpenAI server URL and other parameters, that would be enough. Is the API_URL ser…