# SAW User Manual

:::{warning}
The SAW User Manual is currently being restructured/rewritten in large chunks.

It is likely that you will encounter typos, omissions, and otherwise incorrect
or incomplete information about SAW and SAWScript's features and operation.

Your help identifying these [documentation
issues](https://github.com/GaloisInc/saw-script/issues?q=is%3Aissue%20state%3Aopen%20label%3Adocumentation)
is deeply appreciated, as it helps us prioritize and resolve them more quickly.
Thanks for helping to make SAW better for everyone!
:::

```{toctree}
:maxdepth: 2
:caption: Contents

overview
structure-of-sawscript
invoking-saw
cryptol-and-its-role-in-saw
loading-code
analyzing-hardware-circuits-using-yosys
creating-symbolic-variables
symbolic-execution
symbolic-termination
the-term-type
specification-based-verification
bisimulation-prover
transforming-term-values
proofs-about-terms
extraction-to-the-coq-theorem-prover
formal-deprecation-process
appendices/index
```