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.