A Neo4j code-property graph of a Solidity codebase, exposed to coding agents through a read-only MCP server, so an agent auditing smart contracts can answer cross-contract and state-dependency questions with graph queries instead of grep.
The pipeline ingests one target repo at a time: Slither compiles the codebase, a walker turns Slither's IR into nodes and edges, and an MCP server serves the graph to Claude Code as 15 curated tools. It is a single-user personal audit tool, not a hosted service.
flowchart LR
A[Solidity repo] -->|Slither 0.11.5| B[SlithIR walk +<br/>IR-failure capture]
B -->|batched MERGE| C[(Neo4j 5.26<br/>code-property graph)]
C --> D[MCP server<br/>15 read-only tools]
D -->|stdio| E[Coding agent<br/>Claude Code]
E --> F[Human review<br/>against source]
D -.->|JSONL session logs| G[scripts/analyze_sessions.py]
The graph models six node labels — Repo, Contract, Function (functions
and modifiers), StateVariable, Event, UnresolvedCall — connected by
eleven relationship types: INHERITS_FROM, DEFINES, USES_MODIFIER,
CALLS_INTERNAL, CALLS_LIBRARY, CALLS_EXTERNAL (with a kind property:
call, staticcall, delegatecall, transfer, send, low_level),
CALLS_UNRESOLVED, READS, WRITES, EMITS, and OVERRIDES. Every node
carries a stable canonical_id; functions whose IR Slither failed to generate
are tagged ir_extraction_status: failed so queries can warn when a traversal
under-reports. Ingest is idempotent (MERGE on canonical_id), and the Repo
node records provenance: git commit, dirty flag, and toolchain versions.
The MCP tools split into three groups (registered in
src/solidity_audit_graph/mcp_server/):
- 11 catalog tools wrapping the
.cypherfiles insrc/solidity_audit_graph/queries/: contract overview, forward/reverse reachability, state readers/writers, reentrancy candidates, delegatecall and external surfaces, IR-failed functions, unresolved calls, and state-dependency intersection. - 3 primitives composing common audit shapes:
transitive_state_writers,reach_with_chain,function_callers_partitioned. - 1 escape hatch,
cypher_query, for arbitrary read-only Cypher.
Every tool returns the same envelope: {rows, warnings, truncated, row_count}.
During an audit of Panoptic (a Code4rena contest, December 2025), the
invariant under investigation was
totalAssets() == s_depositedAssets + s_assetsInAMM + unrealizedGlobalInterest(),
where unrealized interest is computed from one state variable,
s_marketState. The load-bearing question — can any external entry point
write s_depositedAssets without first accruing interest? — is a
reachability question grep cannot answer, because "accrue" happens 1–4 call
hops away, sometimes through a library in another file.
Two graph queries settled it: a WRITES match enumerated the direct writers
of s_depositedAssets — seven of them external boundary entry points — and a
variable-length CALLS_INTERNAL|CALLS_LIBRARY|CALLS_EXTERNAL traversal showed
six of those seven transitively reach _accrueInterest, and proved
settleLiquidation does not. Source reading then confirmed the bug the asymmetry pointed at: a
liquidation with zero open positions skips the burn path that freshens
s_marketState, so payouts are computed against stale interest. The finding
matches Code4rena M-14. The full investigation, including the exact Cypher, is
in docs/audits/collateral-tracker-totalAssets.md.
The graph proved reach and non-reach; call ordering still required source
reading — see limitations below.
Prerequisites: Python ≥ 3.12, uv, Docker, and a
solc your target compiles with (uv run solc-select install <version>).
git clone <this-repo> && cd solidity-audit-graph
uv sync --extra mcp # the MCP server needs the [mcp] extra
docker compose up -d neo4j # Neo4j 5.26 Enterprise (eval license)Provision the read-only role the server connects as (guide §2):
docker exec -it audit-graph-neo4j cypher-shell -u neo4j -p auditpass123
# CREATE USER sag_reader SET PASSWORD 'changeme' CHANGE NOT REQUIRED;
# GRANT ROLE reader TO sag_reader;The compose file ships dev-only credentials (neo4j/auditpass123,
sag_reader/changeme); change both for anything beyond a local sandbox.
Ingest a target repo (ingest connects as the admin user, since it writes):
cp .env.example .env # set NEO4J_URI/USER/PASSWORD and TARGET_REPO
uv run ingest --install-schema --wipeSmoke-test the server wiring without Neo4j (expected output: the 15 tool names):
uv run python -c "
from solidity_audit_graph.mcp_server.config import Config
from solidity_audit_graph.mcp_server.server import build_server
mcp = build_server(Config.from_env({'SAG_SESSION_LOG_DIR': '/tmp/sag-smoke'}))
print(sorted(mcp._tool_manager._tools.keys()))
"Register with Claude Code — either open Claude Code inside this repo (the
committed .mcp.json runs uv run sag-mcp-server), or register
per-user:
claude mcp add-json solidity-audit-graph '{
"command": "sag-mcp-server",
"args": [],
"env": {
"SAG_NEO4J_URI": "bolt://localhost:7687",
"SAG_NEO4J_USER": "sag_reader",
"SAG_NEO4J_PASSWORD": "changeme"
}
}'/mcp should list solidity-audit-graph as connected with 15 tools.
From the recorded acceptance walkthrough in the operator guide §9, run against a Panoptic ingest:
transitive_state_writers(state_var_name="balanceOf")
returned 21 rows partitioned by write_kind: 12 direct writers (e.g.
ERC1155::_mint, ERC1155::_burn, CollateralTracker::delegate), each with
chain = [<writer>], and 9 transitive writers, each with its call chain,
such as:
["PanopticPool::_forceExercise(...)", "CollateralTracker::delegate(address)"]
When a result touches a function whose IR extraction failed, the envelope carries a warning (verbatim from the same walkthrough):
{
"type": "ir_extraction_incomplete_in_result",
"functions_failed": [
{"canonical_id": "contracts/SemiFungiblePositionManager.sol::SemiFungiblePositionManager::initializeAMMPool(address,address,uint24,uint8)"}
],
"message": "Edges from these functions may be missing or incomplete..."
}- Database-enforced read-only. The server defaults to the
sag_readeruser (Neo4jreaderrole). Thecypher_queryescape hatch does no client-side parsing or filtering — aCREATEattempt fails at the driver with aForbiddenerror from the database. If the reader user is not provisioned, auth fails closed. Role enforcement requires Neo4j Enterprise; on Community Edition escape-hatch writes would succeed (see the operator guide §8 before accepting that risk). - Bounded results. Rows are truncated at
SAG_MAX_RESULT_ROWS(default 200); truncated envelopes settruncated: truewithrow_countas a lower bound. - Query timeouts. Every query runs with a server-side timeout of
SAG_QUERY_TIMEOUT_S(default 30 s). - Predicate validation.
reach_with_chaininterpolates a caller-supplied predicate into Cypher, so it lexically rejects write and control keywords (CREATE,MERGE,DELETE,DETACH,SET,REMOVE,DROP,FOREACH,CALL) and chaining/comment tokens before the database sees them.
Every tool invocation appends one JSONL record to
<SAG_SESSION_LOG_DIR>/<utc-ts>-<session-id>.jsonl (default
~/.solidity-audit-graph/sessions/), flushed and fsync'd immediately. Fields:
tool_name, params, cypher_string (the generated Cypher, populated for
cypher_query and reach_with_chain), result_row_count, latency_ms,
error ({type, message} or null), timestamp, session_id; failed calls
are recorded with error set. uv run python scripts/analyze_sessions.py
aggregates the logs into a per-audit report: tool frequency, error and latency
breakdowns, the escape-hatch Cypher corpus, and fallback-to-source annotations.
- Solidity only, via Slither (pinned to 0.11.5); the analysis is static.
- The graph is relation-level, not execution-level: it models who calls, reads, and writes, but not statement ordering, conditional guards, loop semantics, or argument values at call sites. "Reaches" means "could call", not "calls before X" — ordering questions still require source reading.
- Where Slither fails to generate IR for a function, that function's outgoing
edges are missing; the graph tags these, and results that surface an
affected function carry an
ir_extraction_incomplete_in_resultwarning, but the blind spot remains. - External calls hidden in inline assembly are invisible to Slither's IR; the
walker synthesizes edges for the common Solmate/Solady
SafeTransferLibshapes only. Other assembly-wrapped transfer libraries are not covered. - Writes through storage-pointer parameters are attributed to the caller passing the pointer, not the function performing the write.
state_writers/state_readersmatch direct edges by declaring contract and do not walk inheritance;contract_overviewwalks inheritance for state variables but not for events, modifiers, or functions.reentrancy_candidatesis a structural heuristic (write + reachable external call within 2 hops) — a hit is a candidate, not a vulnerability.- Tests, NatSpec, and comments are not ingested. One codebase at a time;
re-ingest is a manual
--wipe.
- Unit tests cover extraction (canonical IDs, IR-error capture, toolchain probing) and the MCP server (config, session log, result envelope, truncation, IR warnings, predicate validation, 15-tool registration).
- Integration tests ingest the bundled fixture
tests/fixtures/sample/Sample.solinto an isolated Neo4j testcontainer and exercise all 11 catalog queries plus the primitives against it. CI runs lint and the full suite on every PR and on pushes to master (.github/workflows/ci.yml). - Manual checks documented in the operator guide: a no-database smoke test (§4), a live connectivity check (§5), and a five-bullet acceptance walkthrough (§9) with recorded output covering expected writers, partition semantics, database-side write rejection, session-log capture of the failed write, and IR-warning enrichment. Write rejection is verified manually in the walkthrough — the automated variant is intentionally skipped because the testcontainer user has write permissions.
- Real-world validation consists of the totalAssets investigation described above and an 8-prompt with/without-MCP comparison pass on the same codebase (docs/audit-improvements.md). There is no evaluation benchmark.
- Operator guide — install, role provisioning, env reference, smoke tests, registration, log recipes, acceptance walkthrough.
- totalAssets investigation — the worked audit that validates the approach, with the Cypher used.
- Audit improvements — an 8-prompt with/without MCP validation pass and the fixes it produced.
- Effect/order probe — tractability study for an execution-order layer (probe only; not part of the graph schema).
- Roadmap and catalog gaps.