This Friday, the New Jersey Prog Lang & Systems seminar hosted at @princeton.edu will feature our own @bloomberglp.bsky.social researcher Matthew Z. Weaver presenting new research done with @joomy.bsky.social on extracting certified C++ code from @CoqLang. Full program: njpls.org/dec2025.html

I am hiring a full time researcher for our team in Bloomberg. Candidates must be university professors or experienced industry researchers in the following fields: Network design & verification, AI for infrastructure & security, Compute & Storage, Systems & PL. Reach out!

excited that my team at Bloomberg is supporting PhD students in certified programming (and other infra/sec topics too!) through a fellowship. 💻🛡️ includes stipend, tuition, and internship. timely for Rocq and proof assistant folks as science funding tightens. please apply by July 18th! 📬

I am happy to share that our paper “Non-Termination Proving: 100 million LoC and beyond” was accepted at CAV’25. Joint work with Jules Villard, Peter O’Hearn and Azalea Raad. We’ve analyzed dozens of very large open source and proprietary programs and uncovered a number of execution divergences.

Hello! I am now on bsky.