Meet Our Team: 10 questions for Ben Sepanski

“Meet Our Team” is a blog series where we introduce you to the people behind Veridise. Today, we sit down with our Chief Security Officer, Ben Sepanski.

Ben graduated with an M.S. in Computer Science from the University of Texas at Austin and earlier with a B.S. in Mathematics from Baylor University. To date, Ben has published papers in program synthesis, verification, and analysis, high-performance computing, and scientific computation.

1. Who is Ben Sepanski? Tell me a bit about your background.

I started out working towards a career in mathematics. My father is a math professor, and my long-term plan was to follow in his footsteps. I spent most of my time in high school and college doing extra coursework. By my sophomore year at Baylor, I was primarily attending graduate courses. This came with fun opportunities to pass my summers working on mathematics research in San Diego, Maryland, and with professors at Baylor.

While I was enjoying myself, I eventually began to feel a bit detached from reality. My studies came with fun problems and puzzles to think about, but not much to tie them down to earth.

I remember one afternoon distinctly sitting in an abstract algebra course. We were learning about elliptic curves. I remember staring and sitting in the class and thinking, “This is one thing I will never again use for the rest of my life.” Looking back, things turned out to be quite the opposite.

2. How did you find yourself in the security auditing space?

I initially worked in scientific programming, e.g., studying wave equations for modeling fluids. Looking for a change of pace, I set off to the University of Texas at Austin to study Computer Science instead of pursuing graduate studies in mathematics as planned.

At UT, I joined Isil Dillig’s Utopia research group. Their research studies a fascinating intersection between theory and engineering. Domains of study without clear correctness conditions or theoretical guarantees (like some like AI or engineering applications) have never called to me. I find a clear notion of correctness extremely satisfying, and the research problems in program synthesis and formal verification are a perfect area from which to attack practical problems with a combination of logical analysis and engineering effort.

I enjoyed doing research work at the Utopia research group. During my two years there, I primarily worked with Isil and Kostas Ferles. At the end of my stay, Isil invited me to join the early team at Veridise. Working here has been a nice intersection of theoretical studies and real-world problems and needs.

3. How does the math background help with security auditing work?

There are many layers of mathematics working in the background of the crypto space. In this field, many standard cryptographic methods results are being applied in new and exciting ways. People are interested in perfecting the engineering, but within the context of several stringent and formal correctness requirements. The trustless nature of blockchain systems pits scalability (engineering & design) against mathematical correctness (security & cryptographic argument), creating an exciting dynamic to work in.

Having someone’s money directly tied to how well you can guarantee the correctness of a large system is a very concrete tie to reality. You are not just thinking about puzzles, there are very real consequences to making mistakes in theory or implementation. When I am auditing, I can put into practice the theoretical knowledge that I’ve built during my studies.

This is especially noticeable when investigating the details of zero-knowledge proofs. So much of the literature is still in research papers, and the structures at hand are mathematical in nature. Having a heavier math background makes a huge difference when reading about these systems and staying up to date with new results.

4. Can you explain how you approach security audits in general?

I approach auditing in a very formal way, which is our standard at Veridise.

Ideally, protocols implement the core idea in a simple and clear structure. Take Uniswap, for instance. They have a core codebase which is small and focused on the essential invariants that make the system work. Separately, the periphery contract adds the extra engineering needed to make the project user-friendly and feel smooth. Unfortunately, this clear separation is often not present.

In auditing, a large part of the work involves understanding, and sometimes reverse engineering, the core idea. After reviewing, the auditor should understand not just what a protocol does or how, but why. For example, what invariants ensure that a lending protocol remains solvent? How do you know that a token launcher distributes rewards to the correct users? What relationships are expected to hold between an underlying asset and a share in a vault? Once you understand the underlying motivation and reasoning, you need to compare the idea behind the code with the code itself

I typically like to engage in reviews in two phases: an initial pass where I check for common vulnerabilities and gather an understanding of the protocol, then a second high-level overview focusing on attacking the central invariants.

There is some similarity here with mathematical studies. You can only accept simple and obvious facts as true. Everything else must be built up from these basics. Even in large protocols, if you can’t break things down to smaller, understandable ideas and properties, the system becomes too complex to fit in your head.

5. As the CSO at Veridise, can you tell us on your role and your day-to-day work?

A large part of my work is security auditing. I greatly enjoy this technical side of my work.

I also spend a lot of time working directly with clients. I handle timeline estimates, provide quotes, and coordinate our security analysts for upcoming audits. This means I need to stay updated on each auditor’s expertise, what they’re comfortable with, and where they fit best in our audit projects.

This is an important part of my job as we aim to provide clients with the fastest timelines available without sacrificing our top-notch security guarantees.

6. Before Veridise, you worked with Veridise co-founder Isil Dillig in the UT Austin research lab. What was that experience like?

Isil has a talent for bringing together a team that’s not only fun to work with but also genuinely interested in helping each other. I was very fortunate to be a part of her lab, and it was an incredibly positive experience for me.

7. Software testing before an audit — what are your recommendations?

Most of the errors we encounter are logical ones. It’s rarely reentrancy or front-running. Often, it’s something simple like a typo, mishandling an else-case, or forgetting to update code where needed.

To catch these issues, you need unit tests to check individual components and integration tests to ensure everything works together. It’s also crucial to test in the environment where the software will run. Thankfully, there are excellent tools for simulating blockchains locally in almost every ecosystem.

If you haven’t rigorously tested your system before deployment, that is very risky. Your protocol could be handling a lot of value, so taking an extra week or two to test thoroughly is well worth it. The effort will pay off immensely.

8. We’ve heard through grapevine that you’ve come to really appreciate ‘types’ in programming languages. Can you tell us more about that?

People don’t use types enough.

When I first learned to program, I started with Python in high school. Python doesn’t require you to specify data types, so you just tell the program what to do without worrying as much about how the data is represented. If everything is what you think it is, it works fine, and you can program quickly.

Next I learned C++, which requires you to define data types. This slows you down, makes the code longer and more verbose, and initially seems uglier.

But since my wild days of youth, I’ve come to appreciate why types exist and why they’re important. From a security auditor’s perspective, having clear data types makes code much more readable, especially when you’re dealing with code you haven’t seen before. If you know what the data is supposed to be, it’s easier to understand the code and spot errors. Without types, you have to figure out what the data is, which adds complexity and increases the potential for mistakes.

Types are especially useful in our security audits involving zero-knowledge proofs. In performance-constrained environments like ZK proofs, even small computations require significant prover effort. People care a lot about minimizing constraints, and using types helps maintain these invariants.

For ZK circuits, developers should rely on types as much as possible to communicate how different variables are constrained. The programming language should do the work for you, and handle as much as possible, reducing the high burden on auditors and developers tracing through the call stack to check for inter-procedural constraints.

Fortunately, more people are heading in this direction.

9. What area of blockchain excites you the most recently?

Lately, I’ve spent a lot of time with zero-knowledge and the ZK infrastructure. We’ve been working with frameworks and protocols such as O1JS and Succinct, focusing on projects that not only use ZK but also aim to make the technology more accessible. This is super exciting to me because it helps those who might find ZK tech intimidating.

Take O1JS, for example. They’re enabling developers to write ZK circuits in TypeScript, including recursive circuits. Typically, when you create a ZK circuit, you need to know how long the program will run. But with the power of recursive circuits, you can run programs for much longer periods. This means you can do a lot more with your programs, moving from single, fixed tasks to endless possibilities. It’s a game-changer for developers, making the technology much more impactful and opening up new horizons for what we can achieve.

10. When you’re not working, do your pursue any hobbies or personal interest?

Probably the most stereotypical thing about me is that I’m a big Dungeons and Dragons fan. I’ve played since I was small, and I don’t remember a time without it. Whenever I can, I run a campaign with friends. When I can’t, I follow online campaigns on YouTube series.

I also enjoy playing tennis and during college got pretty good at juggling.

Lastly, I love reading fantasy books like The Name of the Wind by Patrick Rothfuss and The Lies of Locke Lamora by Scott Lynch.

Want to learn more about Veridise?

Twitter | Lens | LinkedIn | Github | Request Audit