See anishathalye/knox for a framework for formally verifying full functional correctness and security of circuits.
Tools for reasoning about circuits in Rosette/Racket.
Moved to knox/rosutil.
Interpret Yosys SMT2 STDT output in Rosette. Moved to knox/yosys.
For proving deterministic start.
Run raco pkg install in the top-level directory to install the package.
Run raco test . to run the tests. When possible, tests should go in the
test collection. When writing tests for functionality that is not exported,
they should go in a test submodule.