Recently I was playing around in this space and came across Dafny, rather I should confess that Claude code pointed be to it.

For software projects it seemed very approachable, even for a complete newbie like me. Probably not for Math though.