[dist1ll]

There is a huge body of work around proof-based programming.

If you're looking for a full blown SMT solver and general purpose dependently-typed PL have a look at F*

https://fstar-lang.org