See anishathalye/knox for a framework for formally verifying full functional correctness and security of circuits.

---

rtlv

Tools for reasoning about circuits in Rosette/Racket.

Collections

rosutil

Moved to knox/rosutil.

yosys

Interpret Yosys SMT2 STDT output in Rosette. Moved to knox/yosys.

shiva

For proving deterministic start.

Setup

Run raco pkg install in the top-level directory to install the package.

Testing

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.