I think the closest thing in usage is Liquid Haskell. Although not a standard proof, the ‘refinement’ types serve as a linearly solvable language of predicates on types. The syntax is relatively standard (in the way of set comprehensions), but it is limited to a subset of what can be captured with ‘full spectrum’ dependent types.