Yes. In fact, musl 1.2.0's pthread_mutex_t was verified in 2021 without changes. The same work found a bug in seL4 (obviously in unverified part, but still). T

Yes. In fact, musl 1.2.0's pthread_mutex_t was verified in 2021 without changes. The same work found a bug in seL4 (obviously in unverified part, but still). The author remarks that this is in part because musl is conservative, and identifies barriers in musl that can be removed. But I think musl should get credits for being conservative here. Also in benchmarks, redundant barriers showed no performance impact. https://people.mpi-sws.org/~viktor/papers/asplos2021-vsync.pdf https://people.mpi-sws.org/~viktor/papers/asplos2021-vsync.p...