Tla Plus, Resilience, Software Development, DevOps.
Tail(VMs); end if; end process; There are a few unfamiliar things here. First await tells TLA+ not to run the process until the statement that follows it is true. VM_dies and scale_down will not run if the current pool has less than two VMs in it. This keeps all our servers from being turned off at