Elazar Gershuni

Applied PL

elazar.g@gmail.com
linkedin/elazar-gershuni

I am Elazar Gershuni.

I am a PhD candidate working at the intersection of programming languages, formal methods, and systems. I work across research and implementation: I turn formal ideas into open-source systems and refine them in practice.

I am the chief maintainer of PREVAIL and its Rust port.

My current program is Vegas:

Foundations for reasoning about strategic protocols.
The vegas compiler, which turns specifications into analyzable and executable artifacts.
thrones, a workbench for interactive game-theoretic analysis.

This program lives at the boundary of game theory, blockchain protocols, formal verification, and practical cryptography.

Selected work:

pythia: static-analysis tool that synthesizes per-loop checkpoint state, persisting only live dirty roots rather than all locals.
mypy: contributor, working with the maintainer team led by Jukka Lehtosalo and Guido van Rossum.
np-guard: contributor.
anyway: civic-tech work for road-safety transparency.
Lean ecosystem: contribution to the Lean standard library, and kraft, where I formalized the Kraft-McMillan inequality, a constructive converse via prefix-free code existence, and source-coding results (entropy lower bound and an entropy-plus-one existence bound), with parts being upstreamed to Mathlib.
nakdimon: a Hebrew diacritizer for restoring niqqud (vowel marks) in unpointed Hebrew text.

Publications:

Dan Greenstein, Elazar Gershuni, Ilan Ben-Bassat, Yaroslav Fyodorov, Ran Moshe, Fiana Raiber, Alex Shtoff, Oren Somekh, Nadav Hallak. A Stochastic Approach to the Subset Selection Problem via Mirror Descent. ICLR 2025. OpenReview
Elazar Gershuni, Yuval Pinter. Restoring Hebrew Diacritics Without a Dictionary. Findings of NAACL 2022. ACL Anthology
Elazar Gershuni, Nadav Amit, Arie Gurfinkel, Nina Narodytska, Jorge A. Navas, Noam Rinetzky, Leonid Ryzhyk, Mooly Sagiv. Simple and Precise Static Analysis of Untrusted Linux Kernel Extensions. PLDI 2019. DOI · Local PDF

Contact: