Problem is, usually describing the problem you want to solve *correctly* using formal tool is a task as hard (and often, equivalent to) the implementation. That said, having a formal description is useful
Coming up with simple specs is not necessarily easy. You could say that is kind of what math is about. That’s how we actually make progress: find those cases where simple specs are possible and build upon them. That’s the kind of library made for eternity.
Very often, the spec is indeed just a very simple implementation. Often you can make the spec especially simple if there are no constraints on the resources it can use, at times even infinite ones.