I think I'm asking for something in between a mathematically verifiable proof and fuzzing. A lightweight way to translate runnable code into a symbolic executio

I think I'm asking for something in between a mathematically verifiable proof and fuzzing. A lightweight way to translate runnable code into a symbolic execution environment that can be exercised (not necessarily verified) exhaustively or stochastically. There are relatively few functions that I want to do this for, and I'm okay with doing some manual work to define the possible inputs and how the functions talk to each other (i.e. mock out network / filesystem / database).