В теории категорий Мили-машина это бесконечный коиндуктивный объект: дай вход - получи выход и снова Mealy-машину. Он идеально ложится на раннера IO-эффектов в функциональщине: каждый вызов возвращает результат и обновлённого исполнителя, готового к следующему вызову. То есть Мили-машина -- это математическая форма вечноживущего stateful-сервера, который помнит контекст!
 
И когда мы к Мили добавим инвариант состояния, который машина обязуется поддерживать, получаем runner, который носит с собой доказательство своей корректности, которое сохраняется при любой композиции. Соответственно, любой агент, использующий эффект через такой runner, автоматически наследует гарантию без дополнительных проверок в коде агента и без e2e тестов на состояние.