"GhostTrace is a self-verifying multi-agent intelligence engine built on FalkorDB—where an Investigator, Red-Team, and CEGAR Formal Verifier collaborate over a live temporal knowledge graph to eliminate hallucinated reasoning paths before execution."
Find the hidden path. Prove what holds. State what could be wrong. Remember why.
GHOSTTRACE is a graph-native incident-investigation and company-knowledge platform built on FalkorDB. It reconstructs time-aware attack paths over a bitemporal graph of identities, credentials, workloads and dependencies. It also challenges its own hypotheses and synthesises minimum-disruption containment plans. Each plan ships with a machine-checkable certificate that states its assumptions, and an independent stdlib-only verifier checks it. Specialised agents coordinate through durable shared memory in the same graph.
No action is ever executed. Every containment action is a simulation; a human approver can record an authorisation, but this build has no executor. The bundled scenarios are synthetic. The local profile uses a demo-only header token; the production profile requires OIDC (see Production deployment).
GHOSTTRACE is entered into all three tracks:
- Agents That Act on Connected Data: Time-valid multi-hop attack path enumeration over bitemporal graphs, CEGAR containment optimizer computing the Price-of-Certainty curve, and out-of-process certified verification.
- Agent Memory and Coordination: 5-agent swarm (Investigator, Verifier, Planner, Red Team, Curator) coordinating directly via FalkorDB atomic CAS leases, durable tasks, handoffs, and provenance-tracked memory that survives restarts.
-
Company Brain: Bitemporal organizational knowledge graph tracking ownership, dependencies, and runbooks across world time
$T$ and knowledge time$\tau$ , resolving conflicting and stale CMDB records.
| Track | What you can see in the product |
|---|---|
| 1 · Agents that act on connected data | Time-valid multi-hop paths enumerated in FalkorDB under world time T and knowledge time τ. Paths are classed CONFIRMED / CONDITIONAL(k) / TEMPORALLY_UNCERTAIN. A CEGAR planner produces the Price-of-Certainty curve, the cost of each additional level of assurance. Certificates are verified out-of-process. |
| 2 · Agent memory & coordination | Investigator → evidence verifier → containment planner → red team → memory curator. Tasks, leases, handoffs, outputs and memory are persisted as graph nodes. Memory carries provenance, taint, a promotion rule, quarantine and supersession. Investigations resume after restarts. |
| 3 · Company Brain | "Who owned this at incident time, as known then vs as known now?", plus dependencies, runbooks and decision provenance. Every answer is source-linked and time-scoped, with stale and conflicting records surfaced. |
The headline scenario, The Ghost Credential, works like this:
- Disabling the alerted developer account leaves a confirmed path through a CI-runner token cached on the developer's workstation.
- The cheapest certified plan (cost 3) is only 0-robust: a single unverified edge can reopen access.
- A 1-robust plan costs 10 and a 2-robust plan costs 14.
- An attacker-written "token rotated" log does not remove the edge (R2).
- A planted alert's suggested action is flagged
requires_human_scrutiny, and the trust-filtered plan differs (R3/R4). - The AI proposes, the graph disposes. A model advisor (Claude, or a deterministic mock offline) proposes plans. Each is simulated and certified: "disable the account" and "isolate whatever the alerts name" are rejected with the surviving path or broken hard flow; "rotate the exposed credential" is accepted at the certified optimum.
Here is a visual tour of GhostTrace across each stage of an investigation:
| 1. Story Mode & Incident Overview | 2. 5-Agent Swarm Live Timeline |
|---|---|
 Guided narrative through The Ghost Credential scenario with live evidence inspector |
 5 specialized agents coordinate via FalkorDB CAS leases and durable task handoffs |
| 3. Hypotheses & Bitemporal Reasoning | 4. CEGAR Containment & Price of Certainty |
|---|---|
 Multi-hop attack path reconstruction under world time $T$ and knowledge time $\tau$ |
 CEGAR optimizer computes the Price-of-Certainty curve ($k=0, 1, 2$ robustness) |
| 5. Machine-Checkable Proof Certificate | 6. Company Brain (CMDB Reconciliation) |
|---|---|
 Independent stdlib-only verifier checks containment proof out-of-process |
 Reconciles conflicting ownership and stale CMDB records across time |
| 7. Durable Agent Memory & Provenance Audit |
|---|
 Quarantined tainted inputs, provenance tracking, and state that survives backend restarts |
export ANTHROPIC_API_KEY=... # or `ant auth login`
GT_LLM_PROVIDER=anthropic GT_LLM_MODEL=claude-opus-5-5 make apiThe model only summarises, explains, nominates latent edges and proposes plans; its output is schema-constrained, re-validated, and every proposal goes through the same simulation and certificate check. Tests and the default demo use the deterministic mock and need no key.
Prerequisites: Docker, uv ≥ 0.12, Node 22.
cp .env.example .env # set GT_DEMO_TOKEN to any random string
docker compose up -d --build # FalkorDB (persistent volume) + API + UI
open http://localhost:8080 # click "Reset scenario & investigate"
docker compose down # stop (data volume kept); add -v to delete datamake install # uv sync --frozen + npm ci
docker compose up -d falkordb # or: make falkordb (FalkorDB on localhost:6379)
make check-env # toolchain + FalkorDB client smoke test
make seed # seed workspace "demo" with Ghost Credential A
GT_DEMO_TOKEN=dev-demo-token make api # API on :8000 (OpenAPI at /docs)
make web # UI on :5173 (proxies /api)make test # unit + property + integration tests (needs FalkorDB)
make lint typecheck # ruff, ruff format --check, mypy --strict, tsc
make e2e # Playwright end-to-end demo flow + axe accessibility (needs API on :8000)
GT_RUN_DOCKER_TESTS=1 make test # also runs the FalkorDB container-restart recovery test
make evals # regenerates evals/report.md; exits non-zero on any soundness violation
make audit secrets # pip-audit, npm audit, secret scan
make reset # re-seed the demo workspace
cd backend && uv run python -m app.worker # queue-mode worker (GT_RUN_MODE=queue)
scripts/recover_falkordb_aof.sh # recover a FalkorDB volume whose AOF cannot be replayed
scripts/smoke_api.sh # end-to-end API smoke test (GT_DEMO_TOKEN must match the API)
python -m verifier check cert.json edges.jsonl # independent verifier CLI (from repo root)
cd backend && GT_MCP_WORKSPACE=demo uv run python -m app.mcp_server # read-only MCP server (stdio)cp .env.example .env.prod # fill GT_DOMAIN, GT_TLS, GT_FALKORDB_PASSWORD, GT_OIDC_* (see docs/operations.md)
docker compose --env-file .env.prod -f docker-compose.yml -f docker-compose.prod.yml up -d --build- HTTPS via Caddy (
GT_TLS=internalfor a private CA, or an e-mail address for public ACME certificates). - OIDC bearer tokens (authorization code + PKCE in the UI); roles
viewer/analyst/approver/adminand permitted workspaces come from token claims.GT_ENV=productionrefuses to start with any other auth mode. - FalkorDB password-protected and not published on the host; AOF + RDB persistence; schema migrations run at start.
- Investigations run on
workerreplicas (python -m app.worker); rate limits are shared across replicas. - Approvals: four-eyes, the independent verifier re-checks the certificate, scrutiny-flagged actions need explicit acknowledgement. Nothing is executed.
Verified on 2026-10-11 by bringing this profile up locally with a test signing key (see the claims ledger).
backend/app/ FastAPI app: graph/ (FalkorDB client, migrations, constant Cypher, repository),
temporal/, ingestion/ (bitemporal ledger, scenarios, seeding), reasoning/ (evidence
calculus R1–R3, snapshot, paths, κ rules, latent templates), planner/ (CEGAR, engine,
brute-force oracle), agents/, orchestration/, memory/, security/, api/
verifier/ stdlib-only independent certificate checker (+ mutation tests); imports nothing from app/
frontend/ React + TypeScript + Vite + Cytoscape.js; Playwright e2e with axe checks
data/scenarios/ ghost_credential_a.json, ghost_credential_b.json (synthetic, timestamped ingestion logs)
evals/ generator/ (seeded benchmark families with planted ground truth), run_evals.py, report.md
docs/ architecture, schema, hard problem, why FalkorDB, API, threat model, evaluation, ops, demo
scripts/ seed, smoke test, env check, profiling, backup/restore, secret scan
The product runs entirely on FalkorDB (one graph per workspace: ws:<workspace_id>). All facts carry bitemporal intervals [valid_from, valid_to) (world time [tx_from, tx_to) (knowledge time
(:Entity {id, name, segment, cost_*})
-[:HAS_CREDENTIAL {tx_from, tx_to, valid_from, valid_to, kind, source_ids}]-> (:Credential)
-[:AUTHENTICATES_AS]-> (:Identity)
-[:CAN_ASSUME]-> (:Identity)
-[:CAN_ACCESS]-> (:Service | :Asset)
-[:CONNECTS_TO]-> (:Host | :Service)
-[:DEPLOYS_TO]-> (:Service)
-[:OWNS {tx_from, tx_to, valid_from, valid_to, stale}]-> (:Service)
-[:DEPENDS_ON]-> (:Service | :Asset)
- Entity Labels:
Person,Team,Identity,Credential,Asset,Service,Repository,Deployment,BuildRunner,Host,Group,Policy,Runbook,Document,Decision,SecurityEvent,Incident. - Durable Coordination Nodes:
:AgentTask,:AgentOutput,:Hypothesis,:Plan,:Certificate,:Memory,:SourceRecord,:AuditEvent. - Full schema documentation: docs/graph-schema.md.
"Without FalkorDB's low-latency graph traversal, our CEGAR verification loop and multi-agent state synchronization cannot resolve multi-hop evidence chains in real time."
FalkorDB is not a cache or an optional sink—it is the central nervous system that powers every autonomous decision, formal proof, and agent coordination lease in GhostTrace. Three of our most complex multi-hop queries from app/graph/queries.py demonstrate sub-millisecond execution over dense connected data:
During Counterexample-Guided Abstraction Refinement (CEGAR), the formal verifier checks if an active attack path still reaches crown-jewel targets through a candidate cut set
MATCH p=(s:Entity)-[*1..$depth]->(t:Entity)
WHERE s.id IN $sources AND t.id IN $targets
AND all(r IN relationships(p) WHERE r.workspace_id = $ws AND r.edge_id IN $allowed AND (
r.tx_from <= $tau AND (r.tx_to IS NULL OR $tau < r.tx_to)
AND (r.valid_to IS NULL OR $T < r.valid_to)
AND (r.valid_from IS NULL OR r.valid_from <= $T)
))
RETURN [r IN relationships(p) | r.edge_id] AS edge_ids, [n IN nodes(p) | n.id] AS node_ids LIMIT $limitWhy FalkorDB matters: Rerunning this verification loop on ordinary SQL or document stores would require recursive CTE joins taking hundreds of milliseconds per iteration, rendering real-time containment synthesis impossible.
The Red-Team agent challenges proposed containment certificates by proposing latent (unmodeled) attack edges. FalkorDB validates whether multi-hop preconditions hold—such as undeclared group trust inheritance across peer identities:
MATCH (s {id:$src})-[m1:MEMBER_OF]->(g:Group)<-[m2:MEMBER_OF]-(peer)-[r:CAN_ASSUME]->(d {id:$dst})
WHERE peer.id <> s.id
AND (m1.tx_from <= $tau AND (m1.tx_to IS NULL OR $tau < m1.tx_to) AND (m1.valid_to IS NULL OR $T < m1.valid_to) AND (m1.valid_from IS NULL OR m1.valid_from <= $T))
AND (m2.tx_from <= $tau AND (m2.tx_to IS NULL OR $tau < m2.tx_to) AND (m2.valid_to IS NULL OR $T < m2.valid_to) AND (m2.valid_from IS NULL OR m2.valid_from <= $T))
AND (r.tx_from <= $tau AND (r.tx_to IS NULL OR $tau < r.tx_to) AND (r.valid_to IS NULL OR $T < r.valid_to) AND (r.valid_from IS NULL OR r.valid_from <= $T))
RETURN count(*) > 0 AS okWhy FalkorDB matters: Bidirectional group traversals are evaluated instantly using FalkorDB's sparse matrix GraphBLAS linear algebra engine, instantly validating or falsifying adversarial hypotheses.
To coordinate the 5-agent swarm without split-brain anomalies or lost updates, FalkorDB executes atomic compare-and-set leases and retrieves graph-relevance memory through multi-hop provenance:
// Atomic Compare-And-Set Task Leasing (Track 2: Agent Memory & Coordination)
MATCH (t:AgentTask {task_id: $tid}) WHERE t.workspace_id = $ws AND
(t.status = 'queued' OR (t.status = 'running' AND t.lease_expires_at < $now))
SET t.status = 'running', t.lease_owner = $owner, t.lease_expires_at = $exp,
t.attempt_count = coalesce(t.attempt_count, 0) + 1, t.started_at = $now
RETURN properties(t);
// Provenance Lineage & Memory Overlap Search (Evidence Verifier & Curator)
MATCH (m:Memory) WHERE m.workspace_id = $ws AND m.status <> 'quarantined'
OPTIONAL MATCH (m)-[:DERIVED_FROM]->(s:SourceRecord)
WITH m, collect(s.source_id) AS srcs
WITH m, srcs, size([x IN coalesce(m.entity_ids, []) WHERE x IN $entity_ids]) AS ent_overlap,
size([x IN srcs WHERE x IN $source_ids]) AS src_overlap
WHERE ent_overlap + src_overlap > 0 OR m.category = 'procedural'
RETURN properties(m), ent_overlap, src_overlap ORDER BY ent_overlap + src_overlap DESC LIMIT $limit;Detailed query catalog and benchmarks: docs/why-falkordb.md.
In compliance with Hackathon Rule 11:
- AI coding assistants (Gemini, Claude, Cursor) were utilized during the hackathon for code autocompletion, boilerplate scaffolding, and voiceover script timing.
- All core architectures, mathematical proofs, Evidence Calculus rules (R1–R4), CEGAR min-cut algorithms, bitemporal schemas, and FalkorDB Cypher queries were designed, implemented, and verified by the authors.
Architecture · Graph schema · The hard problem · Why FalkorDB · API · Threat model · Evaluation and report · Performance · Operations · Demo script · Judge FAQ · FalkorDB bug report · Claims ledger · Decisions · Progress · Security
GHOSTTRACE does not solve open-world containment and does not "guarantee security". Every certificate claim is scoped: within the modeled graph, at snapshot H, at (T, τ), under the stated trust policy and assumptions. All evaluation is on synthetic graphs with synthetic priors; there is no real-world validation. See docs/hard-problem.md and the claims ledger.