I haven't actually used it but I do have experience of refinement types / liquid types (don't ask me about the nomenclature) and IMO they occupy a very nice space just before you get to "proper" formal verification and having to deal with loop invariants and all of that complexity.
https://github.com/flux-rs/flux
I haven't actually used it but I do have experience of refinement types / liquid types (don't ask me about the nomenclature) and IMO they occupy a very nice space just before you get to "proper" formal verification and having to deal with loop invariants and all of that complexity.