Hi! I've done extensive work in both TLA+ and Alloy. My advice is to pick something small and just run with it. It takes some time to learn either, and the bett

Hi! I've done extensive work in both TLA+ and Alloy. My advice is to pick something small and just run with it. It takes some time to learn either, and the better you get, the more easily you'll be able to apply it to even small systems. I recommend starting with speccing a system you already know inside and out, so you can tell if surfaced errors are actual problems or modeling mistakes. You'll learn faster that way. Alloy is a lot more niche because it hasn't had the same popularization push and it's mostly a team of small academics doing everything with no outside funding whatsoever.