[4ad]

Unless you use a language designed for formal verification (Lean/Idris/Agda/F*/ATS/etc), no, it is not possible.

You can get pretty far in Haskell (with various extensions) and Scala. But for Go/TypeScript/etc, forget about it.