https://gist.github.com/hiredman/60e5e6f0025cb38c8a7739d21f5a8ce6 is a toy for specifying and checking stateful protocols (describing a state machine in spec)

For finite state machines you often don't actually need to do proofs, because you can do exhaustive checking for a finite set of states

https://www.hillelwayne.com/post/alloy6/ alloy might be interesting to check out too

Thank you @U0NCTKEV8, you always seem to have infinitely deep sleeves to pull something from!

@U0NCTKEV8 https://gist.github.com/hiredman/60e5e6f0025cb38c8a7739d21f5a8ce6 Are you using core async to mock a internet network? Is the goal here to have some communication protocol between 2 actors/servers/whatever and then see what happens with arbitrary message failures? I'm trying to read the code top down as by the time i hit the details i lose the thread...

core.async is just how the code communicates

The idea is to define, via spec, how a stateful protocol operates over time (start in state x, in which messages q w and e can happen, and those messages cause it to change to another state)

Inspired by https://ubf.github.io/ubf/ubf-user-guide.en.html#contracts_amp_plugins

Thanks, haven't looked at the link but the explanation makes sense.

What if a state machine has multiple possible states in multiple places? For instance 10 variables which can be populated depending on some rules and each can have n states. Is it 10^n of combinations to describe in the state machine "checker" language?

you could also check out http://docs.imandra.ai/imandra-docs , it's a computable logic as a subset of ocaml (much in the spirit of ACL2) with seamless integration between (semi)-automated inductive proofs and bounded model checking (disclaimer: I work on this).