Building an Unverified Compiler with Agents
Four agents spent 14 days and 93,000 lines of Lean building a verified JS-to-WASM compiler from scratch. The compiler ran; the proofs didn’t close.
People
Kiran Gopinathan
Research Scientist
Kiran Gopinathan is a research scientist at Basis. She previously completed her postdoc with Talia Ringer at UIUC, and before that earned her PhD in Programming Languages Research from the National University of Singapore on automating the maintenance of formally verified software. Her research interests cover formal verification, program synthesis, type systems, language design and proof engineering.
Articles
Basis essays and updates this person wrote or contributed to.