Из готовых не знаю, но по идее любой функциональный, где есть нормальная форма у термов. Тогда вычисление это переписывание графа и можно каждый шаг дампить.
В общем-то и lua тоже, но luajit умеет в продолжения и можно засаспендить программу в любом месте и продолжить из точки управления внутри программы на lua
Вот тут уже не знаю, мне казалось каждый запуск функции там принципиально однопоточный, но можно написать свой раннер. Но лучше тут поговорить с теми у кого опыта больше. Мне казалось, что у @astynax есть соотвествующий