formalspec

> No language will prevent you from misimplementing the specs

If the spec is written in the language itself, then some languages certainly will.

See Lean, Rocq, Isabelle, etc