I am a 3rd-year Computer Science PhD student at Stanford University, advised by Clark Barrett.
My interests center on combining automated reasoning with large language models (LLMs). More specifically, I work on the faithfulness of LLMs in autoformalization (translating natural language into machine-checkable formal statements).
Previously, I worked on a range of formal methods topics: SMT solvers, theorem provers, loop invariant generation, program synthesis, and verifying software network functions.
Email: daneshvar [at] cs [dot] stanford [dot] edu
News
[06.2026]: Joining Uber Technologies, Inc. as a PhD Software Engineer Intern in Seattle, Washington.
[06.2026]: AI Coding Benchmarks Need Proofs, Not Just Tests accepted at DL4C and AI for Math, ICML 2026.
[06.2026]: Faithful Autoformalization via Roundtrip Verification and Repair accepted at AI for Math, ICML 2026.
[06.2026]: VeriBench: End-to-End Formal Verification Benchmark for AI Coding Agents in Lean 4 accepted at DL4C and AI for Math, ICML 2026.
[06.2026]: Know Your Limits: On the Faithfulness and Failure Modes of LLM Autoformalization accepted at AI for Math and AI4Law, ICML 2026.
[07.2025]: Towards Improved Stability for SMT Solvers via Input Normalization accepted at FMCAD 2025.
[06.2025]: Joined the Automated Reasoning Group at AWS in Santa Clara, California as an Applied Science Intern.
[06.2025]: Passed my PhD qualifying exam and earned a Master’s in Computer Science.
[08.2024]: Gave a talk Towards Improved Stability for SMT Solvers at the CENTAUR annual meeting, Stanford University.
[03.2024]: Synthesis of Recursive Programs in Saturation accepted at IJCAR 2024.
[01.2024]: Started my PhD in Computer Science at Stanford University.