I think you’re looking at a program verification problem.

With this tool: http://viper.ethz.ch/ You essentially sprinkle your functions with pre- and post conditions (& loops), press „verify“ and it will verify the correctness of your program code.

There are multiple frontends you can use for different languages. Behind the scenes your code + annotations are converted from e.g. Python/Rust/Go to an intermediate language (Viper), which is then verified.