I am currently seeking research and engineering roles in formal methods. I focus on automated verification, specification languages, model checking, and developer-facing tools for safety-critical software. I am also interested in projects at the intersection of AI and formal methods, including AI-assisted specification and verification tools, and formal methods for specifying, verifying, and evaluating AI-agent behavior.

Until April 2026, I built production blockchain infrastructure at Informal Systems. Most recently, I was part of the team developing Emerald, a modular framework for institutional blockchains. Emerald uses EVM with Solidity contracts on top of consensus engines like Malachite and Commonware Simplex. I previously developed Inter-Blockchain Communication in Rust and Cairo (Starknet), and conducted security audits for Cosmos SDK, Tendermint, IBC, and CosmWasm smart contracts.

My applied work combines protocol engineering, automated testing, and security audits for distributed systems. In that work, I developed model-based testing tooling for audits and internal software development, using TLA+ specifications and model checking to compare implementations against their specifications and uncover protocol correctness issues.

My formal methods background comes from my Ph.D. in Computer Science at Université Paris Cité (formerly Université de Paris), where I worked in the Modeling and verification team at IRIF under Prof. Constantin Enea. My thesis focused on automated formal testing of distributed databases, leading to 4 publications on this topic. I defended it on March 30, 2021.

My B.Sc. and M.Sc. in Computer Science are from Chennai Mathematical Institute.

For my detailed experience and career history, see my CV: ranadeep_cv.pdf.