v1.1.0: Rigorous Testing & Formal Verification
Bugs Found and Fixed
| Severity | Bug | Impact |
|---|---|---|
| CRITICAL | Delta encoding corrupted data for large targets | Silent data loss in push/pull |
| MEDIUM | Create/Modify violated documented preconditions | Overwrites and silent creates |
| LOW | Git merge driver couldn't detect file types | E2E merge driver tests failed |
All fixed. Zero known open bugs.
Testing: 808 tests, 0 failures
- Protocol: +25 tests — delta roundtrip, compress/decompress, V2 types
- Semantic drivers: +136 tests — merge correctness (determinism, commutativity, idempotency, Unicode, nulls, nesting, large files, output validity)
- Determinism: +7 tests — commit, patch ID, merge, BLAKE3, diff symmetry
- Git merge driver: +2 e2e tests — clean merge and conflict detection
- E2E: All 27 tests passing (was 26 pass / 1 fail)
Formal Verification (Lean4)
23 theorems proved across 6 domains:
- TouchSet algebra (conflict ↔ intersection)
- Commutativity (symmetry, disjoint ⇒ commute, identity units)
- DAG acyclicity (node/edge addition preserves)
- Ancestor transitivity
- LCA properties (reflexivity, maximal generation)
- Merge properties (base-equals, both-same, symmetry, clean merge)
Performance Benchmarks
28 benchmark functions: cargo bench -p suture-bench
Full Changelog: v1.0.1...v1.1.0