# LLVM/Java Verification with SAW

This tutorial introduces SAW's LLVM/Java verification capabilities.
After completing this tutorial, you will be able to:

- Show that alternative implementations of a function, even across languages,
  are equivalent
- Use external SMT/SAT solvers to augment SAW's internal proof system
- Write proofs in SAW _compositionally_
- Use the SAW REPL to interactively run proofs

You can download {download-dir}`the tutorial files <code>`.

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

introduction
example-find-first-set
using-smt-lib-solvers
external-sat-solvers
compositional-proofs
interactive-interpreter
other-examples
```