Semantic search underpins retrieval-augmented generation, recommender systems, and web search. The provider controls the index and executes the query, leaving the client to trust that results come from the correct algorithm over the intended index. A provider might truncate search to cut costs, bias results toward preferred outcomes, or deviate from the specified algorithm entirely. In RAG pipelines where retrieved content is consumed directly by downstream language models with no human oversight, these risks compound. Zero-knowledge proofs can in principle remove this trust assumption, proving that results follow the agreed algorithm over a committed index without revealing the index itself. But HNSW, the graph-based algorithm that powers nearly all production-scale retrieval, maps poorly onto the fixed constraint systems of zero-knowledge proofs. Atlas is the first system to prove HNSW search at scale, achieving sub-second proving on a million vectors and 2.0 seconds on 100 million.
Why HNSW Breaks Zero-Knowledge Proofs
HNSW organizes vectors into a multi-layer proximity graph. Search starts at a fixed entry point in the top layer, greedily visits neighboring nodes, and descends when no neighbor at the current layer is closer to the query. In the bottom layer, it performs a beam search maintaining a candidate set of ef nodes. The traversal is greedy and data-dependent: how long the search runs and how much state it accumulates both vary with the query and the index. Zero-knowledge proofs from polynomial interactive oracle proofs require circuits to be fixed in advance and provisioned for worst-case behavior at every step. The data-dependent termination of HNSW, where each layer's traversal length depends on local graph structure, maps badly onto this fixed structure. Prior verifiable search systems sidestep this by targeting cluster-based indices like IVF, which partition data into clusters offline and answer queries by scanning the nearest clusters. This fixed, data-independent pattern encodes compactly but sacrifices recall, since a closer neighbor outside the selected clusters is unreachable for the remainder of the search.
Three Techniques That Make It Work
Atlas bridges the gap between HNSW's adaptive traversal and zkSNARKs' fixed constraints through three techniques.
First, preprocessing shifts all database-dependent cost offline. The system uses cq lookup arguments, which prove that claimed values appear in a committed table with per-query prover cost independent of table size after a one-time preprocessing. The preprocessing runs in O(N log N) time, matching the cost of constructing the HNSW graph itself. After this one-time setup, the per-query proving cost scales with the length of the traversal, not the size of the database. This preserves HNSW's sublinear per-query property in the proof system.
Second, HNSW is restructured into a fixed-size-state procedure. The multi-layer graph is collapsed into a unified upper graph where layer transitions become edges, turning L separate per-layer greedy traversals into a single walk. A fixed step budget T_g replaces the data-dependent termination condition. For the beam search phase, the two interdependent priority queues (result set W and candidate set C) are replaced with a single bounded set of size ef. Two lemmas prove this restructuring preserves the exact HNSW result. The first shows that the final state of the result set is order-independent: inserting neighbors in any order always yields the same top-ef elements. The second shows that the candidate queue's contents, while order-dependent, never influence the search result, because disputed nodes are selected only after every closer candidate and trigger termination rather than expansion. With these properties, each beam search iteration becomes one batched merge operation instead of a chain of sequential insertions, reducing constraint cost from O(M times ef) to O(M plus ef).
Third, timestep-tagged batching merges the per-step arguments of the entire traversal into a single invocation. Each step uses identical constraints, with branching handled through witness flags that select values rather than control flow. This eliminates the need for separate permutation and lookup arguments at each step, which would cause proving overhead to grow with the step budget.
Proving Times and Recall
On SIFT1M (1 million vectors, 128 dimensions), Atlas proves a query in 0.8 seconds with a 16.5 kB proof that the client verifies in 40 milliseconds. On BIGANN-100M (100 million vectors, 96 dimensions), proving takes 2.0 seconds, only 2.5 times more than SIFT1M despite a 100 times larger database. The proving cost scales with beam width and step budget, not database size. On a complete RAG pipeline with learned text embeddings, Atlas preserves end-to-end answer quality and reaches higher quality at lower proving cost than all prior verifiable retrieval systems.
The step budget introduces a tunable tradeoff between proving cost and recall. At 95th-percentile budgets, the proven search stays within 0.8 recall@1 points of plaintext HNSW on integer datasets. Every evaluated dataset exceeds 0.9 recall@1 at a deployable configuration. The budget can be set from the observed distribution of step counts for a given dataset, making the tradeoff predictable.
The system is evaluated on six standard ANN benchmarks spanning one million to one hundred million vectors with embedding dimensions from 96 to 960, plus end-to-end RAG pipelines with learned text embeddings. The cost of truncation is small: at 95th-percentile budgets the proven search stays within 0.8 recall@1 of plaintext HNSW on integer datasets, and every dataset exceeds 0.9 recall@1 at a deployable configuration.
Comparison to Prior Verifiable Search
Prior systems like VeriRAG and V3DB target IVF indices, which encode compactly as polynomial constraints but sacrifice recall due to their cluster-based structure. Atlas preserves graph-based traversal and achieves substantially better recall. A concurrent system, zkRAG, directly encodes HNSW but preserves the layered graph structure and relies on revealing the number of steps at every layer. Atlas' merged traversal runs under a single fixed bound and reveals no query-dependent information beyond the search result. zkRAG also uses a specialized PIOP for queue updates; Atlas replaces both queues with a single bounded set and constrains updates through one batched merge per iteration.
Private ANN search systems address a different setting: hiding the query while assuming the server executes faithfully. Atlas assumes the query is public but the index is private, and proves that the server executed the correct algorithm over the committed index. The two settings are orthogonal and complementary.
Threat Model and What Gets Hidden
The provider may deviate from the protocol arbitrarily: answer from a stale or altered index, truncate the traversal, bias the ranking, or forge a proof. The client may try to learn as much as possible about the index graph's structure, edges, or embeddings. Atlas achieves privacy (the client learns nothing beyond the query result), soundness (the result is correct with respect to the committed index), and efficiency (sublinear per-query cost). The query is sent in the clear, and the provider publishes a binding commitment to its index before serving queries. Claims about the well-formedness of the index, such as whether edges connect genuinely nearby vectors, are orthogonal and can be addressed with existing techniques.
What It Does Not Do
Atlas proves correct execution of HNSW search against a committed index, but it does not prove anything about the index's quality or construction. A provider could commit to a well-formed index and then serve results from a different one, but the proof would catch that. What it cannot catch is an index that is technically consistent with its commitment but constructed to produce poor results. The step budget tradeoff means that at lower budgets, recall degrades, and the system must be configured appropriately for the deployment's quality requirements. The evaluation is on standard benchmarks; transfer to other embedding spaces or distance metrics is not evaluated. The end-to-end RAG evaluation demonstrates that proven retrieval preserves answer quality, but the interaction between retrieval quality and generation quality in RAG is itself a complex system-level question.
What This Means for practitioners
If you operate a retrieval service and your clients need assurance that results are computed correctly, Atlas provides that assurance without sacrificing the graph-based search that makes modern retrieval work. The preprocessing cost is one-time and scales with index construction. The per-query proving cost is sublinear in the database size, and the client verification is fast enough for interactive use. The step budget gives you a knob to trade recall for proving cost, and the evaluation shows that the tradeoff is favorable at practical configurations. For RAG pipelines, the end-to-end evaluation confirms that proven retrieval preserves answer quality, which is the result that matters in practice.