matheusosan

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

Using Elixir’s metaprogramming (Code.compile_quoted) and the BEAM’s Hot Code Swapping, we can transform a configuration flag into a reactive recompilation. Instead of asking if a flag is active, the system is structurally altered to execute only the necessary code.