ExMaude is an Elixir library providing high-level bindings for Maude, a formal specification language based on rewriting logic developed at the University of Illinois at Urbana-Champaign. Maude has been in active development since 1999 and is used in academia for protocol verification, security analysis, and programming language semantics.
The library manages Maude processes through a Poolboy worker pool and offers a pluggable backend architecture (Port, C-Node, NIF) for different performance and isolation requirements.
Features:
- Term reduction, rewriting, and state space search through a high-level Elixir API
- Pluggable backends: Port (~500us/op), C-Node (~100us/op), NIF (planned)
- Bundled Maude 3.5.1 binaries for macOS and Linux (ARM64 + x86_64)
- Telemetry integration for observability
- Structured error types with 16 error categories
- Livebook notebooks included for interactive exploration
IoT rule conflict detection:
The library includes a specialized module for detecting conflicts in automation rules, based on the AutoIoT research paper. It identifies four conflict types – state conflicts, environment conflicts, state cascades, and state-environment cascades – through Maude’s equational reduction, providing mathematical proof of conflict-freedom rather than probabilistic coverage.
I wrote this primarily to support formal verification of IoT automation rules, but the core API is general-purpose and applicable to any domain where rewriting logic or model checking is useful – protocol verification, state machine analysis, configuration validation, and similar problems.
Feedback and contributions are welcome. Full documentation, code examples, and Livebook notebooks are available in the repository.
Happy coding … or AI introspecting or whatever we call this fusion today 
References:
