Great to see this here, as a contributor to this project. We even went the model checking direction with Bastet: https://github.com/se2p/Bastet