Installation#

StrataSolidity can currently only be used by building from source.

Prerequisites#

1. Lean 4 (via elan; the version is pinned in lean-toolchain) — needed to build StrataSolidity and the Strata back-end.
2. Strata vendored as a git submodule at ./Strata.
3. Python 3.12+ — only for development and CI tooling (the SARIF schema check and the benchmark CSV check). You don’t need it to verify contracts.
4. solc — the Solidity compiler (used for AST extraction only).
5. z3 SMT solver on your PATH.

Building#

1. Check out the StrataSolidity repository with submodules:

   git clone --recurse-submodules https://github.com/strata-org/Strata-Solidity.git
   # or, after a plain clone:
   git submodule update --init --recursive
   

2. Verify the submodule layout:

   bash scripts/check-strata.sh
   

3. Build:

   lake build
   

This compiles the Lean translation pipeline and the strataSolidity CLI executable at .lake/build/bin/strataSolidity.

Verifying the installation#

Run the included test suites:

lake test               # Lean unit and characterization tests
bash test/run_tests.sh  # golden suite (test/examples/*.sol vs test/expected/) and exit-code checks

The golden suite runs each example contract through the full pipeline and diffs the result against the expected output. If both pass, your installation is working correctly.