Literally none of the things you mention help with verifying distributed systems. I think you just fundamentally aren't understanding what it is and this isn't the right forum for me to bridge that gap for you. You highlight this lack of understanding by dismissing a custom hypervisor as a collection of bash scripts and focusing on things Rust has or does well that are completely irrelevant for the classes of bugs that Antithesis is trying to uncover.

> To get Raft, will do sans-io with full typed rust covered by proofs for state(machine) and macro generator for glue(from state machine). I need only prop/fuzz test to test small integration sans-io part. I do not need antithesis.

Again, I think you're missing the point entirely. With hand written property test/fuzz test, you have to manually and correctly implement all the failure conditions that can happen "sans-io". A notable one would be packet reordering (if you're I/O doesn't guarantee ordering) or network partitions. The point of Antithesis is that it will transparently do all of that state checking for you. It's not that you'd not get there eventually, but Antithesis will be an easier system and you'll move faster. Whether or not that's valuable is a decision everyone makes for themselves.