Hi, released a overhauled version of Recife, now using TLC :) Recife 0.3.0 - Use Clojure and the REPL; - Visualize the trace; - Hillel's examples from his book; - Also an example using the incredible @jepsen_io's Elle lib. Model checking your implementation is easier than ever, the lib is like re-frame in the sense that you just pass functions which receive a state and return another state. One point that I would like to test later is to use pfeodrippe/arrudeia to have control over the scheduling of your application, with it you could. Another possibility is to test re-frame applications themselves given that it's async by default. Both need some form of instrumentation. https://github.com/pfeodrippe/recife Small release video at https://youtu.be/C9WwF4RXq74.