Symbolic Software is a bigger team than usual this summer, and we’d like you to meet everyone. Five people joined us: two research interns, Lorenzo and Hossein, who came on board through our Summer 2026 research internship, and three teaching assistants, Faysal, Abd El Kader and Rabab, who are helping run the Applied Cryptography online course for the Summer 2026 cohort.
The interns have been working on soundcalc-lean, a project proposed and backed by the Ethereum Foundation: a Lean 4 restatement of soundcalc, the calculator that evaluates the concrete bit security of hash-based zkVMs under different parameter choices. In soundcalc-lean, every cell of a soundness report is re-derived as a machine-checked theorem over exact rationals rather than computed with floats. The teaching assistants, meanwhile, have been grading, proctoring, answering questions and handling logistics for the fifty Lebanese students taking the course this summer.
Rather than describe everyone ourselves, we asked each of them to introduce themselves and their work. Here they are, in their own words.
The research interns
Hossein Hafezi
I’m Hossein Hafezi, a PhD student at the University of Cambridge (previously at NYU), where I work on applied cryptography and systems security. You can find out more about me at hosseinhafezi.com.
At Symbolic Software I worked on rewriting soundcalc in Lean, with added semantics. The project was proposed and backed by the Ethereum Foundation, and it computes the bit security of different hash-based zkVMs under different parameter choices — an important effort given how widely these zkVMs are used, especially in zk-rollups, and the role they are likely to play in post-quantum blockchains. I started this project with zero knowledge of Lean and formal methods, and came away having learned a great deal. We hope the Ethereum and ArkLib communities will keep building on top of our library. One small note: working with Nadim is fun, because he’s very hands-on.
Lorenzo Magliocco
I am Lorenzo Magliocco, a PhD graduate in Cybersecurity from Sapienza University of Rome and LUISS. My research efforts focused on foundational theoretical cryptography, particularly in the design of multi-party protocols and theoretical models where truly honest parties do not exist.
Coming from a background in engineering and cybersecurity, I always had an inkling for exploring more applied avenues, and that’s what brought me to Symbolic Software! From no prior experience in formal verification and open-source development, I was able to contribute towards writing a Lean port of soundcalc: a Python tool that enables zkVM developers to evaluate the overall soundness and proof size of different zkVM configurations. Early on, I gave an introductory bullet talk on our efforts to the broader Ethereum formal verification community (Ethproofs #9). Ever since, I have been working mostly on the engineering side of the project, while diving into Lean subtleties and proofs as needed. I am already happy with the results we achieved so far, and I hope the broader zkVM ecosystem will be able to benefit from our efforts!
The teaching assistants
Faysal El Estwani
Hi, my name is Faysal El Estwani! I’m currently pursuing a Master’s degree in Computer Science at the American University of Beirut, where my thesis focuses on cybersecurity, specifically malware analysis. I’m passionate about software engineering and enjoy tackling programming problems. Outside of cybersecurity, I have a strong interest in game development and love exploring how software can be used to create interactive experiences. In my free time, I’m also an avid music enthusiast and enjoy learning about and playing musical instruments.
This summer, I’ve been working as a Teaching Assistant for the Applied Cryptography course. I spend most of my time grading assignments and exams, answering students’ questions, and helping explain concepts that they find challenging. It’s been a great opportunity to strengthen my own understanding while helping others learn. It’s so rewarding explaining something to a student and then seeing them apply it correctly on an exam or exercise!
Abd El Kader Kahil
Hello, my name is Abd El Kader Kahil. I am a graduate student, finishing up my Master’s thesis in Lebanon at the American University of Beirut. My technical interests include programming language design and implementation, cryptography, graphics/game programming and algorithm optimizations. Here’s my website with links to my socials.
At Symbolic Software I worked as a Teaching Assistant with Professor Nadim Kobeissi at his independent summer course. During this period I corrected assignments, answered questions, held exams and handled logistics. My goal is to minimize the friction between Lebanese students and learning cryptography and make this subject more widely studied and researched in the country. This opportunity also allowed me to connect with promising students in Lebanon and help shape their knowledge base and future.
Rabab Salim
Hello, I’m Rabab Salim, a Master’s student at the American University of Beirut where I’m currently finishing up my thesis on topics related to cybersecurity and machine learning. I have also TA’ed many courses as part of my Graduate Assistantship here, which has ignited my passion towards teaching.
Working with Professor Nadim under Symbolic Software as part of the Applied Cryptography course has been a wonderful experience. Being a teaching assistant here isn’t constricted to grading assignments and proctoring exams, but is part of a bigger goal of making cryptography easy and accessible to Lebanese students, and this is what I hope to accomplish by the end of the course. Meeting and engaging with students has been insightful and inspiring in many different ways. I aspire to make the most out of it while pushing towards many more meaningful goals like this one!
Our thanks to all five — the summer’s research output and the course both rest on their work. We’ll have more to say about soundcalc-lean as the project matures, and the Summer 2026 cohort runs through October 10.