pon_beam

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 res

PON-BEAM is a complete re-architecture of the Erlang/OTP Virtual Machine (ERTS — Erlang Run-Time System) using the Notification-Oriented Paradigm (PON)