I recall that @Ptival was looking into reviving this at some point, but I don't know what became of that.

There are two crucible-mcs:

• The one merged into the master branch, that is very barebones and was created by Iavor 4 years ago. I doubt it's ever going to be useful in the present state, and so likely could be removed (with @yav 's confirmation).

• The one stuck in the longstanding crucible-mc branch. This one I wrote under Aaron Tomb's supervision about 2-3 years ago, and is more fleshed out. As I recall, we were able to export some Crucible ASTs (under some restrictions) into transition systems that we could export into Sally syntax to run the model checker on. I'm not aware of any interest in reviving this one, it's also likely bitrotting. Not sure how I feel about it, merging it would add a bit of maintenance overhead that may be useful to no one, but throwing it away sounds wasteful. Open to discussion.