crack ⚡

verify distributed and lock-free algorithms through symbolic execution

appendix: philosophy of reliable engineering

for large stateful systems, extra specification up-front saves tremendous effort overall

1. TLA+ is useful, but it's costly to learn. we use this to bridge the gap
2. cleanroom methodology: specify the intended behavior of ALL nontrivial blocks
3. simulate asynchronous network conditions by delivering messages {on time, late, never} in a test harness that explores different paths (either generative or full-state enumeration) depending on testing compute time budget

in action:

1. model core communication algos in TLA+ before coding
2. make all messaging pluggable
3. make all sources of time pluggable
4. rely on typed notions of time to reduce the state space explosion of message delivery latencies
5. HEAVILY use debug_assert! for all nontrivial blocks