Hi HN, I built PON-BEAM, a heavily modified version of the Erlang/OTP 30 virtual machine. I wanted to eliminate the O(N) selective receive bottleneck and the C

Hi HN, I built PON-BEAM, a heavily modified version of the Erlang/OTP 30 virtual machine. I wanted to eliminate the O(N) selective receive bottleneck and the CPU-heavy scheduler spinlocks by introducing a reactive, event-driven notification mesh at the C level (using epoll/eventfd). However, changing how the Erlang scheduler and garbage collector handle state transitions is notoriously dangerous and prone to lost wakeups or deadlocks. To make this viable, I had to formally prove the new architecture. I used a 4-pillar verification pipeline: TLA+ / TLC to model the non-blocking invariants of the new scheduler and mailbox. Coq for mechanized proofs of the Tri-Color garbage collection propagation. Frama-C / ACSL for C source-level memory safety and loop termination. PropEr for stateful equivalence testing against the baseline OTP 30. The result is a VM that maintains exact Erlang semantics but achieves O(1) mailbox reads and 0.0% idle CPU. It is a completely different way to think about VM design (based on the Notification-Oriented Paradigm). You can read the architectural breakdown and the formal proofs in the repo. Would love to discuss formal methods and VM design with this community. Repo: https://github.com/matheuscamarques/pon_beam https://github.com/matheuscamarques/pon_beam