Formal Verification Tool

Use Z3py binding to take in function parameters, analyze AST for symbolic execution and produce the function return value range for preventing math overflow or underflow. Still work in progress.