Abstract: Critical software components often display effects such as randomization, 
nondeterminism, concurrency, and exceptions. Complex combinations of effects show up 
in distributed systems, security, and privacy applications where correctness is crucial, but 
mixtures of effects also make testing and informal reasoning difficult or impossible. While 
powerful formal methods exist for reasoning about individual effects, those semantic 
foundations do not provide a unified account of how such effects interact. As a result, 
verification techniques are highly specialized and difficult to compose.
In this talk, I present Outcome Logic, a logical foundation that captures diverse program 
behaviors via a common notion of outcomes. Outcome Logic enables reusable reasoning 
principles across deterministic, nondeterministic, and probabilistic settings, and allows 
multiple effects to be composed on top of the base logic. I will show how the extensible 
approach allows Outcome Logic to support new types of reasoning in domains such as 
verification of randomized distributed systems and principled bug-finding techniques.

Bio: Noam is a final year PhD Candidate at Cornell University in the area of Programming 
Languages and Formal Methods, advised by Alexandra Silva. Before coming to Cornell, he 
was a staff software engineer in the Facebook Programming Languages and Runtimes 
team, where he worked on unique projects including using dependently typed Haskell in 
production and formally verifying concurrent algorithms for an OS microkernel.
Noam's current research focuses on logical foundations for reasoning about programs that 
branch into different outcomes, which provide a unifying perspective for reasoning about a 
wide variety of effects including nondeterminism, nontermination, randomization, 
concurrency, and exceptions. The resulting Outcome Logic, has applications including 
unifying the theories of correctness and incorrectness and verification of concurrent 
randomized algorithms. Noam's research is supported in part by the NSF and he was 
recently recognized with the 2024 ACM SIGPLAN John Vlissides Award for applied software 
research and a distinguished paper award at POPL 2026