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

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.