CIS Seminar Series 2026 - Ruzica Piskac, PhD- Yale University

About

Privacy-Preserving Automated Reasoning: From Program Verification to Private AI Guardrails

ABSTRACT As AI systems become increasingly capable and autonomous, ensuring that they behave correctly, respect policies, and protect sensitive information is a fundamental challenge. Formal methods and automated reasoning provide powerful tools for verifying correctness, while cryptographic techniques enable verification without revealing sensitive information. In this talk, I will present our on-going research on privacy-preserving automated reasoning. I will first outline the framework for privacy-preserving program verification. Program verification provides stronger guarantees of correctness than standard testing. The verification process takes a program as input and derives a mathematical formula. Proving that the program is correct then reduces to establishing that this derived formula is unsatisfiable. Traditionally, automated reasoning tools can determine unsatisfiability automatically, and modern solvers can also produce proofs of unsatisfiability. However, these techniques typically rely on the proof and the underlying code being publicly available, which may not be desirable in certain applications. I will show how to address this challenge. We initially developed a protocol for validating the unsatisfiability of Boolean formulas in privacy-preserving settings. Building on these results, we developed ZKSMT, a virtual machine for validating unsatisfiability results produced by SMT solvers in zero-knowledge settings. I will describe the theoretical foundations of this work and show how they are scalable. Finally, I will connect these results to a broader vision of trustworthy AI, in which formal reasoning and cryptography provide principled guarantees of correctness, policy compliance, and confidentiality.

BIOGRAPHYRuzica Piskac is the Zhan Tianyou Professor of Computer Science and Chair of the Department of Computer Science at Yale University, where she leads the Rigorous Software Engineering (ROSE) group. Her research spans formal methods, programming languages, software verification, automated reasoning, program synthesis, security, and applied cryptography, with a common goal of improving the reliability and trustworthiness of software and AI systems. Her recognitions include an NSF CAREER Award, a CACM Research Highlight, multiple Distinguished Paper Awards, the Facebook Communications and Networking Award, the Microsoft Research Software Engineering Innovation Foundation Award, several Amazon Research Awards, and Yale University's Ackerman Award for Teaching and Mentoring. Her professional service has included serving as Program Chair of the 37th International Conference on Computer Aided Verification (CAV), serving on more than 70 program committees, and serving as a member of the Steering Committee of the Formal Methods in Computer-Aided Design (FMCAD) conference.