I roughly check it. The array looks like tree in type defintion, where indexing is O(log n), but the real implementation seem to be real array with O(1) The Ty

I roughly check it. The array looks like tree in type defintion, where indexing is O(log n), but the real implementation seem to be real array with O(1) The Type thing is affine type similar to Rust ownership. The array in-place mutation relies on affinity to avoid deep copying. The Data thing is reference-counted if shared, like Rust Arc. The parallel invocation is similar to Rust's rayon::join . About the proof system, I am not familar with formal verification, but it's obvious that the translation from business requirement to proof target still requires coding and can contain bugs. Even if proof is fully correct, if proof target deviates to business requirement then it still have a bug