Grounded Deduction
Summer Research Fellow · EPFL, Switzerland · May 2026 – Present (onsite May – July 2026; remote after)
Adviser: Prof. Bryan Ford, DEDIS Lab
- Developing Grounded Arithmetic, a non-classical logic that admits arbitrary recursive definitions without prior termination proofs, and mechanising its metatheory in Isabelle.
- Proved truth preservation and primitive recursiveness for the inference rules of Basic Grounded Arithmetic (BGA). Contributed to the design of Propositional Grounded Arithmetic (PGA).
- Built a quantified extension of Grounded Arithmetic as a usable object logic in Isabelle/Pure, and established the consistency of BGA within it.
- Designing automated proof-search tactics for the Isabelle/Pure development, which inherits none of the automation built for classical and intuitionistic logics.
Verification Modulo Tested Library Contracts
Student Researcher · IISc · May 2025 – Apr 2026
Advisers: Prof. D. D’Souza (IISc), Prof. P. Madhusudan (UIUC), Prof. A. Murali (UW-Madison)
- Co-developed VMTLC, a hybrid framework that verifies client programs by synthesizing library specifications that are formally proven against the client but validated via testing against the library.
- Designed the Learner component within a Teacher-Learner CEGIS loop, developing two distinct LLM-integrated architectures (a pure LLM learner and an LLM-seeded ICE learner) to leverage semantic intuition, synthesizing valid contracts where traditional enumerative baselines could not.
- Designed and built the core LLM pipeline responsible for generating contracts from logical rules and integrated it into a feedback loop with formal verifiers and testing engines to ensure correctness.
Paper
Code
Enhancing Formal Verification with LLMs
Research Intern · University of Virginia, USA (Remote) · Aug 2025 – Oct 2025
Adviser: Prof. Wenxi Wang, The University of Virginia
- Developed ACPRO, a framework that uses a multi-agent LLM pipeline to transform low-level Z3 proofs into interpretable, high-level Verus verification steps.
- This work also produced the VSVerus dataset, a new resource for studying fine-grained LLM reasoning in formal verification.
Formalization of Group Theoretic Algorithms
Summer Research Fellow · Krea University, India (Onsite) · May 2025 – July 2025
Advisers: Prof. Rishi Vyas (KREA), Prof. T.V.H Prathamesh (KREA)
- Formalized proofs for decision problems in geometric group theory (including the word, conjugacy, and subgroup membership problems) using the Lean 4 proof assistant.
- Key contributions include formalizing two definitions of the Dehn function and proving their equivalence and verifying the algorithm for the conjugacy problem in free groups.
- Current work focuses on the computability of the Dehn function for hyperbolic groups.
Game Theory and Automata
Student Researcher · IISc · Jan 2026 – Present
- Investigating supergames played by finite automata under finite costs for complexity to analyze the sequential collapse of equilibrium states.
- Deriving critical phase change thresholds that characterize these equilibrium dynamics.
Causal Discovery in Time Series
Student Researcher · IISc · Aug 2025 – Present
Adviser: Prof. Deepak N. Subramani, Computational and Data Sciences, IISc
- Proposed and developed Mask2Cause, an end-to-end Transformer that recovers the causal graph during the forecasting forward pass via a learnable sparse adjacency injected as a log-barrier into masked attention over inverted variable embeddings.
- Formulated causal discovery under volatility spillover, where one variable governs the conditional variance rather than the mean of another. Motivated the heteroscedastic objective through the theory of directed information graphs and showed neural Granger causality to be its additive-noise special case.
- Built Mixed Physics, the first benchmark separating mean-parents from variance-parents, and the first model to recover variance-mediated edges explicitly. Attained state-of-the-art accuracy at reduced parameter count.
Paper
Code
