What the Interns Built This Summer
We hosted eight interns this summer, including three through IIT Madras’s Summer Fellowship Programme. Here is some of what they built.
Learn2Lean
Anubhav Paul, an undergraduate at IIT Delhi, formalized the arithmetic algorithms every schoolchild learns in Lean 4, and turned the proofs into a teaching tool. He built one representation, a digit list checked against a single toNat correctness function, and proved nine algorithms against it: addition, subtraction, multiplication, long division, divisibility tests, Euclid’s GCD, and square roots.
The result is Learn2Lean, an interactive web book. Each chapter pairs a worked example with a ProofWidgets visualization inside the Lean infoview, plus worksheets that check a reader’s own attempt against a live local Lean checker. Anubhav built it with Pranav Ramesh, aimed at readers who don’t yet think like type theorists. A talk based on the project was accepted at IndiaFOSS 2026.
Repo Book (live) Talk (IndiaFOSS)
CoRE Stack biodiversity
S Naveen, from IIIT Manipur, and Uttkarsh Tiwari, from NIT Mizoram, built a biodiversity layer for CoRE Stack, the environmental-planning platform our ESG group builds with Prof. Aaditeshwar Seth’s team at IIT Delhi. They used GBIF, the Global Biodiversity Information Facility’s archive of georeferenced species occurrences: download and clean occurrences around a block’s micro-watershed layer, look up IUCN Red List status per species, and join everything spatially inside Google Earth Engine, the same engine every other CoRE Stack layer runs in.
Sixteen indicators are now validated end to end on two real blocks, Jamui in Bihar and Hassan in Karnataka, rendering correctly as a GeoServer choropleth from the computing/gbif module. It is still on a feature branch of core-stack-backend, awaiting merge. Naveen is continuing the work as an exchange student for his final year of BTech at IIT Madras, and we are beginning closer, more frequent collaboration with Seth’s team in Delhi.
Tombstone-free CRDTs
Harisankar Binod, from NISER Bhubaneswar, worked on the part of distributed systems that makes Google Docs and Notion-style collaborative editing possible: RGA and its tombstones, the permanent record of deleted-but-unremovable characters that a heavily-edited document accumulates. Working in Sal, our Lean 4 verification framework for replicated data types, he designed a tombstone-free “rehoming” variant and proved it RA-linearizable with zero uses of sorry. Then he found a counterexample: four sequential edits on a single replica where a character the user never touched silently changes position.
The bug survived the proof because both sides of the correctness comparison were built from the same step function. Catching it required comparing against RGA’s own published specification instead. The fix, EmbedRGA, replaces mutable anchors with immutable birth coordinates computed once at insertion. It extends for free to rich text (Peritext), where the same bug would otherwise let a delete silently reformat untouched text. Harisankar wrote up the full story, including a week at the LeanLang Summer School, on his own blog, and gave an internal talk on it.
Repo (Sal) Blog post Slides (PDF)
Cryptography in OxCaml
V. Krishnan, from NIT Jamshedpur, measured how close OCaml, and its OxCaml extension, can get to C for performance-critical cryptography, without giving up OCaml’s safety guarantees. Every optimization in his technical report was assembly-guided: a throughput change with no assembly explanation was treated as noise.
The project moved from an XOR stream cipher (about 0.50x C) through AES and Rijndael (parity with C, once Int32 boxing was eliminated) to ChaCha20 and SHA-256, where OCaml’s tagged-integer representation forces a mask after nearly every 32-bit operation. OxCaml’s unboxed int32# type removed that overhead directly, for a 39% throughput gain on SHA-256. Neither compiler recognizes the rotate idiom (x lsl n) lor (x lsr (32-n)): it compiles to three instructions instead of a single roll. That is now a concrete request with the OxCaml compiler team. The full report and code are public, and a related effort implementing crypto natively in OxCaml continues with Avik Shakhari and Anirudh Sudhir.
Repo Report (PDF) Continuing work
Concurrent data structures
Zeeshan Mohammed Rangrej, from IIT Palakkad, took CS6868, our concurrent programming course, before writing any test code. Working with Navaneeth Nambiar, he wrote DSCheck test cases for a lock-free Treiber stack. Using DSCheck’s TracedAtomic, he exhaustively explored every valid interleaving of concurrent push and pop operations on OCaml domains. No counterexample trace means a sequential ordering exists that explains every concurrent execution: the definition of linearizability. He extended the same approach to a lock-free linked list.
He validated the checks against a deliberately buggy implementation of the list, and confirmed DSCheck caught the injected fault every time. Reading Godefroid’s thesis on systematic exploration of concurrent programs pointed at DSCheck’s next gap: extending it from safety properties to liveness properties, now an open issue on the course repository. Zeeshan is currently reading how Software Transactional Memory implementations track read and write sets and detect conflicts, with an eye toward implementing and testing one himself. His internship has ended, but he continues as a remote collaborator.
Pull request Report (PDF) Open issue
Separation logic
Chaitanya Agarwal, a PhD student at NYU, visited for the summer to explore formal-verification angles connected to his PhD thesis, working with Prof. Aishwarya and KC. His most visible contribution was two internal talks, Introduction to Separation Logic and its sequel a week later, both adapted from the Iris tutorial at POPL 2021, the ACM symposium where Iris itself was introduced.