I had attended EuroSys 2026 held in Edinburgh, Scotland, which was my first ever conference I had either attended or participated in. My work titled Sal: Multi-modal Verification of Replicated Data Types, co-authored with Prof. KC Sivaramakrishnan and Vimala Soundarapandian was accepted into the 13th Workshop on Principles and Practice of Consistency for Distributed Data (PaPoc), which was co-hosted with EuroSys 2026.

Travel to Edinburgh

I was particularly excited to travel to Edinburgh, since it would mark my first visit to anywhere in Europe. The initial travel was tumultous, since I was travelling via Germany without knowing that a transit visa was required! Luckily, I had obtained a Schengen visa for a different purpose, which helped me board the aircraft!

The last part of the journey to Frankfurt was overlooking the beatiful Austrian and Swiss alps, before the short flight to Edinburgh took me to the site of the conference. I landed one day earlier, so I immediately set out sightseeing with the time I had. Boarding the typical Double Decker Bus in the UK was an experience in itself. I visited the regal Holyrood Castle, which still is used by the Royals of the UK.

PaPoC 2026

The next day, I turned up at the Edinburgh International Conference Centre to participate in the PaPoC 2026 workshop. The event was kick-started with a keynote speech by Prof. Rachid Guerraoui. The talk was about State Machine Replication, an area with which I was completely unfamiliar. As a result, I learnt quite a lot about the terms and ideas used in the world of consensus and distributed computing, especially in the theoretical side.

Subsequently. Prof. Ken Birman talked about the challenges of distributed data collection in the domain of power grid collection, and the work demonstrated the surprising result that ensuring consistency through linearizability improved performance!

Then, Kegan Dougal presented interesting work on Duelling Admins in blockchain, where admins could concurrently demote each other, leading to an inconsistent state. The solution involved using an Epoch-Resolved-Arbiter, a separate entity which decided which concurrent operation occurs first, and also garbage-collecting any histories which are no longer needed to determine the current state. This was the first presentation directly involving CRDTs.

My Presentation on Sal and Prof. KC's Keynote

After this, I presented our work on Sal. The presentations were timed for 20 minutes, and I had prepared a few times earlier so that I could fit it in comfortably, and allow for questions. My presentation is available on Github. The primary story which I attempted to convince the audience was that automated verification of replicated datatypes had become considerably easier with the advent of Lean. Lean offered a multi-modal proof approach, which included the careful and systematic use of both interactive and automated theorem proving techniques. This sought to offer a better methodology than the earlier push-button automated verification. Our approach included counterexample generation and verification whenever a verification condition (VC) failed. One such example for the enable-wins flag is given below. More details are available in the paper, as well as in Prof. KC's excellent blog on his Keynote speech at PaPoC which followed my own talk. I would, therefore, not describe his keynote talk in this blog.

Other Interesting Presentations at PaPoC

Several other groups had come up with a lot of other interesting work, most notably Florian Pfeil et al.'s work on CRDT design for collaborative spreadsheets, called AegisSheet. They described several flaws in existing spreadsheet softwares, and proposed a formalization for a spreadsheet CRDT. A common concern with such attempts is that an obscure test case could completely break the guarantees they attempt to offer. This is exactly where Sal's pitch comes in - with the help of AI agents, if the specification is formalized and proved using Sal's framework in Lean, then the desirable properties for any CRDT (primarily convergence) is automatically guaranteed!

Prof. Lindsey Kuper, one of the chairs of PaPoC, also gave an interesting talk on her group's work Can you keep a secret? A new protocol for sender-side enforcement of causal message delivery.. The work described a new protocol for message passing, highlighting the shortcomings of both the client-centric and server-centric approaches (Figure below). The presentation style was refreshing, and it was also a learning for me on how to present a work of research while at the same time taking the audience along in teaching something new. I had also discussed with her about her blog which is also one of the inspirations for me developing interest to write my own.

Emilie Ma (from Prof. Marc Shapiro's group) presented a nice work on formalizing the semantics of RocksDB. Their work, titled CobbleDB, relied on composition to offer reasonable performance, as well as correctness guarantees. For the uninitiated, Prof. Marc Shapiro was one of the researchers who introduced CRDTs to the world. Meeting him, and interacting with him, therefore, was hugely inspiring.

Other Days - EuroSys 2026 and Exploring Scotland

The PaPoC conference lasted the entirety of the first day, and I learnt a lot interacting with the various speakers and the problems they were working at. I enjoyed listening to most of the talks, and the speakers did a great job at taking the audience with them and helping them understand research.

For the next two days, I attended parts of the EuroSys 2026 conference, primarily the Cloud & Serverless Resource Management and Fault Tolerance, Reliability & Debugging tracks. Each of these gave me new insights and information about areas within computer science which I was relatively unfamiliar with. I also attended the AI and Security components of the conference. I particularly found Ryan Deckett's presentation on Learning Network Configuration Contracts interesting. It described an approach to reduce the security threats caused by erroneous network configurations using a meta-language which looked a lot like First Order Logic.

I also walked around the historical city of Edinburgh, and went on a trip to Arrochar and Tarbet via train. The views were some of the most breathtaking you could see (photos attached). The trip was rounded off by a visit to the Edinburgh Castle.

Final Note

I would like to thank Prof. KC as well as the entire CyStar for helping me and sponsoring the trip. I would also like to thank the organizers of the conference for the wonderful experience.