Basis logotype

Kiran Gopinathan

People

Kiran Gopinathan

Research Scientist, New York, NY

Kiran Gopinathan is a research scientist at Basis focused on formal verification, program synthesis, type systems, language design, and proof engineering. Her work spans proof repair, verified compilation, and formal coordination languages for trustworthy AI systems. She pioneered the field of proof repair for imperative programs (Sisyphus, PLDI 2023 Distinguished Paper) and produced the first formally verified proof of the probabilistic properties of the Bloom Filter.

Website Google Scholar GitHub Email

Education

  • PhD, Programming Languages Research
    National University of Singapore, 2023
  • BSc, Computer Science
    University College London

Previous Appointments

  • Postdoctoral Researcher
    University of Illinois Urbana-Champaign

About

I am a research scientist at Basis, where I work on formal methods for trustworthy AI systems, including verified compilation and formal coordination languages for multi-agent ecosystems.

My academic research pioneered the field of proof repair for imperative programs, building tools and techniques for keeping verified software correct as it evolves. This work produced the first practical proof repair system for imperative code (Sisyphus, PLDI 2023 Distinguished Paper) and invented proof-driven testing, exploiting the Curry-Howard correspondence to repair proofs of real-world programs.

I am broadly interested in developing tools for the maintenance and automation of formal verification—the process of using computers to construct mathematical proofs about software correctness. My techniques span proof repair, invariant inference, and automated verification.

Before joining Basis, I was a postdoctoral researcher with Talia Ringer at the University of Illinois Urbana-Champaign. I completed my PhD at the National University of Singapore under the supervision of Ilya Sergey in the VERSE Lab, and my undergraduate degree in Computer Science at University College London.

Projects

Current and recent Basis projects.

Pact

A formal coordination language for multi-agent systems, unifying ideas from game theory, distributed systems and cryptography to enable trustworthy autonomous agent interactions.

Verified Compilation

Exploring the use of AI agents to build formally verified compilers, investigating the limits of current LLM-based agents on rigorous proof construction tasks.

Collaborations

Ways to work with Kiran at Basis.

Collaborative research projects

I am interested in collaborating with researchers working on formal verification, proof automation, programming language design, and trustworthy AI systems.

Co-advising postdocs and trainees

I am open to co-advising postdoctoral researchers and trainees working at the intersection of formal methods, programming languages, and AI safety.

Awards & Service

Recognition and community contributions.

ACM SIGPLAN Distinguished Paper Award, PLDI 2023

For “Mostly Automated Proof Repair for Verified Libraries.”

NUS School of Computing Dean's Graduate Research Excellence Award, 2023

Awarded for outstanding doctoral research.

Chair, OCaml Workshop 2025

Program chair for the OCaml Users and Developers Workshop.

Program Committee Member

OOPSLA 2026, ICFP 2025, OCaml Workshop 2023, AIPLANS 2021.

Software

Tools for formal verification and programming languages.

Sisyphus

Automated proof repair tool for OCaml programs.

Ceramist

Verified hash-based Bloom Filters in Coq—the first formal proof of the probabilistic properties of the Bloom Filter.

Petrol

A typed SQL DSL for OCaml providing compile-time type safety for database queries.

Ego

A pure OCaml implementation of E-graphs and equality saturation.

Gopcaml

A structural editing mode for OCaml in Emacs.

Recent Publications

Recent papers and preprints.

Selected Publications

Earlier selected work.

Articles

Basis essays and updates this person wrote or contributed to.

Pact: Trustworthy Coordination for Multi-Agentic Ecosystems

April 23, 2026

Multi-agentic ecosystems are becoming commonplace, but how can we trust them? We propose Pact, a formal coordination language that unifies ideas from game theory, distributed systems and cryptography to enable trustworthy multi-agent coordination.