This is very cool, thank you for working on it! I noticed on your personal website that you’ve also worked on using TLA+ PLA+ to verify the completeness of Bitcoin contract protocols (hat tip to @dgpv who has also done similar work). I’m wondering if there’s any planned overlap, for example an automated way to extract information from a comprehensive DSL to use with TLA+ PLA+?
[Edited to correct name based on @dgpv reply.]