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:

• Maude System
• AutoIoT Paper
• Hex

https://github.com/futhr/ex_maude