You can look into theorem proover (Coq, lean ...) and code extracted from them. A middle ground is FramaC+WP plugin for hoare logic for C.

Some languages like F* are also proof oriented.