Dafny usability research
I investigate how AI and better tool feedback can improve the experience of writing and proving programs in Dafny. The aim is clearer proof workflows, stronger automation, and more approachable formal development.
I investigate how AI and better tool feedback can improve the experience of writing and proving programs in Dafny. The aim is clearer proof workflows, stronger automation, and more approachable formal development.
Research on automated repair for verification-aware languages, starting with Dafny. The goal is to narrow the gap between verifier errors and actionable fixes.
Verus is a useful comparison point for thinking about how verification integrates with systems programming. It helps frame a broader usability story for formal methods.
As verification lead engineer, I built constrained-random environments, temporal assertions, and formal checks for CSI-2 camera controllers in automotive-oriented contexts.
My industry work focused on turning specifications into checks, assertions, and verification environments that supported practical, high-confidence hardware design.
Recent work explores how language models can assist with proof development in verification-aware languages while keeping the human in control of the workflow.