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

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 https://fstar-lang.org