I’d like to announce the release of eta 0.1.0 (as in η) - a deterministic simulation testing framework for Erlang.
Deterministic simulation testing is an approach to system testing in which you remove all non-determinism from the system under test and the test harness. Once you’re able to achieve this, bugs become perfectly reproducible and replayable, even when the system includes interleavings of message processing and wall-clock timers.
DST is an investment, and not all systems will give you a positive return. It’s well suited for distributed systems problems (e.g. Two-Phase Commit, Leadership Election and Replication, etc), and in my experience, when applied there it’s possible to reap huge rewards.
eta was created out of a project in which we found ourselves implementing a bespoke distributed data replication scheme after a database-driven leadership election. Specifically, I was making heavy use of AI coding to build a distributed process registry, and correctness was a serious concern. In a world where we all have more ideas than time, I went looking for ways to accelerate the verification of an AI agent’s output, and stumbled into formal methods. After a successful use of TLA+/TLC, I decided that the actual Erlang implementation needed some protection via DST, and created eta.
eta’s main hook into your system is via a test-time parse_transform. It rewrites your actual Erlang code, only in test, so that it can be fully and deterministically controlled by the eta execution engine. You implement the eta_harness which sets up your system and generates a workload against it, hopefully achieving interesting behavior. Finally, define rules about invariants and properties of your system that can be checked along the way.
When you execute the DST harness, eta suspends all processes under test and activates one at a time, thus behaving as a process scheduler. When your system invokes a clock, it’s replaced by a virtual clock, allowing us to skip forward in time in the event that no process is runnable. As your system runs under the workload, your defined invariants are checked throughout.
When an invariant is violated, the PRNG seed that generated the workload is guaranteed* to recreate the precise sequence of events that led to the pathology. From here, you or your favorite AI agent can add additional tracing to debug and troubleshoot the issue at hand.
*: assuming you’ve achieved real determinism
There’s lots more to say, but perhaps it’s better left to the documentation:
The pages linked above and this post were written by hand the old fashioned way. You’ll find many annoying LLM-isms in the rest of the eta documentation. I do strive to rewrite them so they are fit for human consumption. However, we all have more ideas than time, and what is an LLM if not a fuzzy idea resolver?
eta has helped me wrestle LLM output into correctness for a subset of the vast software problem space, and I hope it can help others, too.