fhevm-static-analysis

name

fhevm-static-analysis

description

Used when running Slither, Aderyn, or Semgrep on an FHEVM project, or when setting up static analysis in CI. Covers the canonical slither . invocation (never npx slither), the ZamaConfig source-map crash workaround, known FHEVM false-positive detectors, FHE-specific Semgrep rules, and when to prefer Aderyn or Halmos. Triggers on Slither crash on ZamaConfig, source code appears to be out of sync, slither-analyzer install, npx slither, aderyn ., semgrep FHE rules, Halmos on rate limiters, or adding static analysis to a Hardhat CI workflow for confidential contracts.

fhevm-static-analysis

Static analysis patterns for FHEVM projects. Slither is the default gate; the tooling diverges from generic Solidity in two places — the ZamaConfig.sol source-map crash and a handful of FHE-specific false positives. This file is the routing core; the full Slither / Aderyn / Semgrep / CI snippets live in references/static-analysis.md.

Essential Principles

1. slither . — not npx slither

Slither is a Python tool distributed as slither-analyzer on PyPI. There is no npm package, no npx slither. The literal invocation from a project root is:

pip install slither-analyzer         # one-time
slither .                             # at repo root
# or one-shot without installing:
uvx --from slither-analyzer slither .

Agents that emit npx slither are wrong every time.

2. A bare slither . crashes on FHEVM projects

@fhevm/hardhat-plugin patches ZamaConfig.sol at compile time. The on-disk file differs from the source map Slither rebuilds, and Slither aborts with SlitherException: source code appears to be out of sync. Apply the ZamaConfig patch workaround (see references/static-analysis.md), then use the canonical invocation:

uvx --from slither-analyzer slither . \
    --hardhat-ignore-compile \
    --filter-paths "node_modules" \
    --exclude-dependencies

3. Three detectors always false-positive on FHEVM

• reentrancy-no-eth — every FHE.* op is a precompile call that Slither models as an external call. Disable.
• unused-return — FHE.allow / FHE.allowThis return the handle for chaining; ignoring the return is the canonical usage. Disable.
• calls-loop — encrypted batch operations are intentional. Disable unless the loop has a plaintext external call.

4. Aderyn is faster on large codebases

Aderyn (Rust-based) typically does not hit the ZamaConfig crash and runs faster than Slither on codebases > ~20 contracts. Use as an alternative or alongside Slither:

cargo install aderyn && aderyn .
# or, if nix is available:
nix-shell -p aderyn --run "aderyn ."

5. Semgrep catches FHE-specific patterns that generic tools miss

Custom Semgrep rules catch missing FHE.allow after FHE.fromExternal, arithmetic on euint256 (unsupported), and view functions returning encrypted types — bugs that Slither and Aderyn do not model. See references/static-analysis.md for starter rules.

6. Halmos for small, high-stakes functions

Halmos (symbolic execution) is well-suited for sub-200-line functions with clean state shapes — rate limiters, access-control gates, token-math libraries. Not a whole-program tool; scope it to what you suspect.

CI integration

Add static analysis to the three-gate deployment checklist (see fhevm-testing Essential Principle 6). A minimal CI step wraps the ZamaConfig workaround around the canonical invocation:

#!/bin/bash
set -e
npx hardhat compile    # applies the plugin patch
# … extract patched source from build-info, copy over node_modules file …
uvx --from slither-analyzer slither . \
    --hardhat-ignore-compile \
    --filter-paths "node_modules" --exclude-dependencies \
    --json slither-report.json
# … restore original …

Full scripted workaround in references/static-analysis.md.

When to Use

• Setting up Slither / Aderyn for the first time on an FHEVM project.
• Debugging SlitherException: source code appears to be out of sync.
• Wiring static analysis into a Hardhat CI workflow (GitHub Actions, etc.).
• Choosing between Slither, Aderyn, Semgrep, and Halmos for a given review scope.
• Triaging Slither findings and filtering FHEVM-specific false positives.

When NOT to Use

• Writing contract code → fhevm-contracts.
• Fixing a specific detector finding that's not a known false positive → general Solidity audit skills.
• Runtime debugging (ACLNotAllowed(), EmptyDecryptionProof()) → fhevm-antipatterns.
• Mocha / Hardhat test authoring → fhevm-testing.

Cross-references

• fhevm-antipatterns/references/debug-checklist.md § 11 (Slither "source code out of sync") — the ZamaConfig source-map crash is catalogued there as a debug-checklist entry. (fhevm-antipatterns/SKILL.md pitfall 11 is .env secrets, unrelated.)
• fhevm-testing Essential Principle 6 — the three-gate deployment checklist puts slither . in gate 3 (pre-mainnet review).
• fhevm-setup — static analysis assumes a working Hardhat workspace exists.

Routing

Which task does the user's prompt match?

1. "How do I run Slither on an FHEVM project?" → references/static-analysis.md § Slither Setup.
2. "Slither crashes with source code appears to be out of sync." → references/static-analysis.md § ZamaConfig Workaround.
3. "Which Slither detectors are useless on FHE code?" → Essential Principle 3 + references/static-analysis.md § Known False Positives.
4. "Semgrep rules for FHE patterns?" → references/static-analysis.md § Semgrep Custom Rules.
5. "Is Aderyn / Halmos a better fit?" → Essential Principles 4 and 6.
6. "Add Slither to CI." → CI integration section above + references/static-analysis.md § CI Integration.

External references

• Slither — https://github.com/crytic/slither
• slither-analyzer on PyPI — https://pypi.org/project/slither-analyzer/
• Aderyn — https://github.com/Cyfrin/aderyn
• Semgrep — https://semgrep.dev
• Halmos — https://github.com/a16z/halmos
• @fhevm/hardhat-plugin (source of the ZamaConfig patch) — https://github.com/zama-ai/hardhat-plugin