SymbiYosys is an open source formal proof engine. Limitations of the free version are verilog only support, assertions and assumptions can only be boolean (no SVA).
Use docker to run these example on any platform
docker run -it -v $PWD:/root tocisz/verilog-toolbox:latest
counter : simple demo
arbiter : round-robin arbiter
fib : fibonacci generator
integer-divider : More complex example demonstrating rtl visualization
memory : demonstrate abstract memory modeling engine
mult : explore capacity