Expand description
Vector Clock implementation for causality tracking
This implementation follows the TLA+ verified specification in protocol/tla/vector_clock.tla
Properties verified:
- CausalityPreserved: Happens-before relationship is correct
- Transitivity: If A→B and B→C, then A→C
- Monotonicity: Clock values only increase
- ConcurrentDetection: Concurrent operations detected correctly
- MergeCorrectness: Clock merging preserves causality
Structs§
- Vector
Clock - Vector clock for tracking causality between operations