Meet Our Team: 10 questions for Shankara Pailoor

Veridise
Veridise
Published in
8 min readOct 29, 2024

“Meet Our Team” is a blog series where we introduce you to the people behind Veridise. Today, we sit down with our Head of ZK Research, Shankara Pailoor.

Shankara joined Veridise in 2022. He earned his PhD in Computer Science, and has extensively published in program verification (zero-knowledge security), program analysis, and related fields.

At Veridise, Shankara works at the intersection of research, in-house tool development, and security auditing, with a particular focus on zero-knowledge audits. He is one of the core developers of Picus, Veridise’s tool to check the determinism of ZK circuits. Shankara has audited several ZK projects such as Succinct SP-1 ZK-VM, Risc Zero ZK-VM, and Semaphore.

1. Who is Shankara Pailoor? Can you tell me a bit about your background?

I did my undergrad at the University of Chicago, where I studied mathematics and computer science. Initially, I thought I’d pursue a PhD in math, but I quickly realized that math research wasn’t the path for me. After graduation, I worked as a software engineer at Expedia for just over a year. It was a great experience, and I learned a lot, but I found myself wanting to go back to school to explore the research side of computer science.

That led me to Columbia University, where I earned my Master’s degree under the guidance of Professor Suman Jana. I really enjoyed the research process in computer science and even published a paper on OS fuzzing. At that point, I wasn’t sure if I wanted to pursue a PhD, but Suman encouraged me to apply.

When I started looking into PhD programs, I came across Isil’s website at UT Austin. Funny enough, when I applied, I thought, “We probably don’t have a perfect match in terms of research interests, but her work is fascinating, so it can’t hurt to apply.” In hindsight, that was a great decision, and that’s how my PhD journey began. Then, in 2022, during my fourth year, Isil founded Veridise and soon recruited me to join.

2. Tell me about your PhD journey and areas of research

My PhD journey was really about discovering a variety of interesting research problems and diving into them. Early on, I realized I’d get bored if I focused on just one topic for too long, so I branched out into several different areas. I ended up working on things like program synthesis, fuzzing, program verification (especially zero-knowledge circuit security), and even SMT solvers. Each area kept things fresh and exciting, and I enjoyed exploring the diverse challenges that came with each one.

3. Any tips for new PhD students embarking on a similar journey?

One of the most important things is to spend a lot of time reading papers and staying up to date with the existing research in your field. It’s not always easy, but being aware of what’s being published and reading the key papers is crucial. It’s a lot of work, but it pays off — ideas flow more naturally when you’ve absorbed a lot of material.

Another tip is to build strong connections throughout your PhD. It’s helpful to have people you can talk to and bounce ideas off of, whether they’re colleagues, mentors, or friends. Some of the best ideas come from discussions, and having a solid support network can be invaluable.

A PhD can be a lonely and daunting experience at times because you’re often venturing into uncharted territory. You might not know if you’ll even find a solution to the problem you’re working on, which can lead to pressure or feelings of frustration when progress is slow. That’s why it’s so important to have a good group of friends or a support system to help keep you grounded and boost your morale when things get tough.

Lastly, take your time choosing the right advisor. Don’t feel pressured to join someone just because they offered you a position. Make sure their research aligns with your interests, and that you feel comfortable working with them. You’ll be spending a lot of time with them over the years, so it’s important to find someone who’s a good fit both professionally and personally.

4. Before Veridise, you mentioned you worked with Isil Dillig in the UT Austin research lab. How were those times?

It was a really great experience! Isil did an amazing job fostering a supportive lab culture. The lab had a good balance of senior and junior students, and the senior students were always willing to help and mentor the newer ones. I found that super helpful when I first joined. Later on, as a senior PhD student myself, I really enjoyed being able to mentor the new students who came into the lab.

There was also a big social aspect to the lab. Isil organized a lot of activities, like hikes and get-togethers at her house, and she made a point of celebrating everyone’s birthday. Those small touches made a big impact — you got to know her and your lab mates better in a more casual, social setting. I have a lot of fond memories from my time in her lab.

5. You’re one of the most experienced ZK auditors at Veridise. What challenges do developers face when it comes to Zero Knowledge development?

Developing zero-knowledge (ZK) circuits is a very different process compared to traditional software development. Normally, when you write software, you’re expressing some kind of computation that follows a clear data flow — where you set a variable and use it later in the program.

In ZK development, however, you’re working with constraints, which are polynomial equations over finite fields. You need to ensure that these constraints accurately reflect the computation you have in mind, but it’s easy for a mismatch to occur. The constraints often look quite different from the actual computation, so it’s not as simple as translating from one to the other.

Another major challenge is that ZK circuits are difficult to test. In traditional smart contract development, you can build confidence in your code by writing extensive tests. But with ZK circuits, many issues — like determinism bugs — are hard to catch through regular testing. This requires more sophisticated tools, and the limited amount of advanced tooling in the ZK space makes writing circuits even more challenging.

6. What advice would you give ZK devs?

I would say that many issues come from early optimization.

It’s much better to start by writing a circuit that you know is secure, even if it has some redundant constraints. Once you have a correct circuit, you can then focus on optimizing it, one part at a time, while carefully reviewing it to make sure it’s still correct. Trying to write an optimized circuit from the start can lead to mistakes — it’s easy to overlook something in the process.

I often see bugs when someone tries to get clever and minimize the number of constraints too early, but ends up introducing errors.

7. As one of the core developers of Veridise’s Picus tool for checking ZK circuits, how has Picus evolved over the years?

Initially, Picus was being developed by Yanju and Clara from our team. They had the insight that checking a circuit’s determinism could be framed as an SMT query. The advantage of using an SMT solver is that, in theory, it gives you a sound and complete way of verifying determinism. However, the downside is that SMT solvers struggle to scale up when you’re dealing with large circuits.

I realized that in many cases, you don’t actually need the full precision of an SMT solver to prove determinism. To show that a signal is deterministic, you just need to demonstrate that it’s a function of the inputs, and you can often use lightweight static analysis rules to do this. There was some previous work from the PSE team, called Ecne, that took a similar approach, and I wanted to combine the strengths of this lightweight method with the more rigorous SMT solving.

That’s how Picus came about — it combines lightweight static reasoning with the more powerful SMT solver in a synergistic way. Picus starts by applying the lightweight rules to identify deterministic signals. When the static analysis hits a wall, it falls back on the SMT solver. But instead of using the SMT solver blindly, Picus uses the results from the lightweight analysis to simplify the queries it sends to the solver, making it easier to prove whether certain signals are deterministic.

If the SMT solver proves determinism for certain signals, it feeds those back into the static analyzer, and the process starts again. This creates a nice iterative loop between lightweight reasoning and more intensive SMT solving.

That said, the bottleneck in determinism checking is often still the SMT solver itself, which has led us to explore ways to improve SMT solvers for finite field domains. For example, our latest paper with Alex Ozdemir focused on enhancing the CVC5 solver for handling bit constraints, and that’s a direction we’re continuing to explore.

8. What has been your favorite auditing experience?

Probably the most fun auditing experience was Succinct’s Telepathy protocol. It was such a big audit, but what I really liked about it was a lot of the issues we found in the audit were used to build our static analysis tool ZK Vanguard . It’s always great when the issues you find can help improve your tooling so the same issues can be found quickly.

9. We’ve heard through the grapevine that besides auditing, you enjoy philosophy. Tell us more!

Philosophy has always been a hobby of mine for a while. It all started back in high school when I picked up Bertrand Russell’s Problems of Philosophy, and that book really sparked my interest in the subject.

Later, while I was studying at UT Austin, I got more involved in academic philosophy. The department was welcoming and open, so I had the chance to attend a lot of seminars and events. It was fascinating to hear the kinds of questions philosophers wrestle with — things you might not think about in everyday life. For instance, they might explore whether abstract objects actually exist or debate concepts in Mereology, like whether tables are real entities or just collections of more basic elements. Engaging with these debates is really stimulating, and it opens your mind to ideas that might never cross your path otherwise.

There are a number of philosophers I enjoy reading. For example, Philosophy of Science by Alexander Bird is a fantastic book, and I also love Contemporary Debates in Metaphysics, edited by Theodore Sider. It’s a collection of papers where philosophers argue opposing viewpoints using different frameworks and theories, which makes for a great survey of the field while showing both sides of key issues.

Overall, philosophy is a fun intellectual pursuit for me. It challenges my mind and lets me think in ways I don’t always get to in my everyday life.

10. Besides philosophy, when you’re not working, what are some of your hobbies and personal interests? Any books you never stop recommending?

I’m a huge sports fan and absolutely love watching games (both in person and on tv), especially American football. I also really enjoy baseball, but it’s tough as a Mariner’s fan. A few friends and I often get together to watch the games, which is always a good time. Outside of sports, I’m really into hiking and spend weekends discovering new places to explore.

As for books, I’m a big fan of classic American novels. Two that really stood out to me are Blood Meridian and The Road by Cormac McCarthy. Both are beautifully written. Recently, my brother recommended that I read the original Dracula, and I’m glad I did. Even though it’s an older book, it’s surprisingly easy to read, and I found it really fun.

Interview by: Mikko Ikola

Want to learn more about Veridise?

Twitter | Lens | LinkedIn | Github | Request Audit

--

--

Veridise
Veridise

Published in Veridise

Our mission in to harden blockchain security with formal methods. We write about blockchain security, zero-knowledge proofs, and our bug discoveries.

Veridise
Veridise

Written by Veridise

Hardening blockchain security with formal methods. We write about blockchain & zero-knowledge proof security. Contact us for industry-leading security audits.

No responses yet