projects
Research projects in Programming Languages, Formal Methods, and Neurosymbolic AI.
Our group is involved in several interesting projects across Programming Languages, Type systems, Program Verification and Synthesis, and Neurosymbolic programming/AI. Below, I list some of these:
Formal Methods for Verification and Synthesis
This umbrella project aims to make fundamental contributions to the use of Formal Methods (e.g., Refinement Types) to aid programmers in writing correct, safe and coverage complete programs.
- Coverage Types: Under-approximate properties.
- Morpheus: Higher-order parser combinators.
- Hegel: Novel tree automata for synthesis.
- Lean: Formal Verification.
Trustworthy AI: Guardrailing & Neuro-Formal Methods
Read full project overview
Bridging the gap between AI/ML and Formal Verification, this project introduces a neuro-symbolic/neuro formal framework that uses formal methods to mathematically guardrail AI systems. By integrating neural architectures (LLMs in particular) with theorem provers like Lean, automated SMT solvers, and symbolic reasoning engines, the system replaces soft probabilistic guardrails with provably correct runtime constraints. This hybrid pipeline continuously validates neural outputs against formally defined safety specifications, effectively preventing hallucinations, logical contradictions, and policy violations in high-stakes domains. Ultimately, it provides a deterministic, mathematically sound foundation for deploying trustworthy AI where empirical evaluation alone is insufficient.
Symbolic and Neurosymbolic Program Synthesis
Solving challenging, error-prone programming tasks across various domains using verified program synthesis using a combination of PL and AI/ML techniques.
- DUNE: NeuroSymbolic Synthesis for Automatic Data Transformation.
- TANTRA: Correct low-level network configurations.
- Review the Curated List of synthesis applications.
Trustworthy Concurrency
Programming and reasoning about concurrent programs is notoriously challenging. We develop scalable reasoning methods for hardware and compilers that support weaker memory models than sequential consistency.