Sure man thanks for the critique, genuinely....
To be precise..the core concurrency shapes, disjoint-chunk commit ordering and DAG-level wavefront scheduling, are model-checked (SequentialEquivalence; DependencySafety + Termination), continuously re-verified in CI via a second independent executable encoding. The TLA+ file itself is bounded to a small instance and a 2-chunk model... the paired Python checker checks all contiguous chunk counts and all commit-order permutations for n up to 6.
Conflict detection isn't in the TLA+ file, it's verified separately .. unit and integration tests exercise the real dispatch code against an independent golden sequential run, covering duplicate-key writes, unresolved-index writes under an explicit "depend=none" assertion, and all three error modes (report/quiet/hard), plus a real module-import-level integration test and a concurrency stress test hammering the same conflict path across 10 threads x 6 repeats to catch anything nondeterministic.
Also a note: this is v1.1. The rigor was front-loaded by me, and not something that evolved over years ...so there can be a chance of more rigor or checks...currently working on that.
If you find a bug or a security issue, please open one, genuinely want the feedback.
To be precise..the core concurrency shapes, disjoint-chunk commit ordering and DAG-level wavefront scheduling, are model-checked (SequentialEquivalence; DependencySafety + Termination), continuously re-verified in CI via a second independent executable encoding. The TLA+ file itself is bounded to a small instance and a 2-chunk model... the paired Python checker checks all contiguous chunk counts and all commit-order permutations for n up to 6.
Conflict detection isn't in the TLA+ file, it's verified separately .. unit and integration tests exercise the real dispatch code against an independent golden sequential run, covering duplicate-key writes, unresolved-index writes under an explicit "depend=none" assertion, and all three error modes (report/quiet/hard), plus a real module-import-level integration test and a concurrency stress test hammering the same conflict path across 10 threads x 6 repeats to catch anything nondeterministic.
Also a note: this is v1.1. The rigor was front-loaded by me, and not something that evolved over years ...so there can be a chance of more rigor or checks...currently working on that.
If you find a bug or a security issue, please open one, genuinely want the feedback.