Prover MCP Server
Click on "Deploy Server".
Wait a few minutes for the server to deploy. Once ready, it will show a "Started" state.
In the chat, type
@followed by the MCP server name and your instructions, e.g., "@Prover MCP Serverrequest a zero-knowledge proof for the KS test on my dataset"
That's it! The server will respond to your query, and you can continue using it as needed.
Here is a step-by-step guide with screenshots.
Natural-Language Zero-Knowledge Verification via Skeptical MCP Tools
Code and data for the paper A Natural-Language Interface to Zero-Knowledge Verifiable Computation: Enforcing Correctness at the Tool Boundary (see Paper and artifact map).
The system, the MCP Prover Chatbot, is a dockerized chat assistant that lets authenticated users interact with the CoSMeTIC zero-knowledge proof service through natural language. Queries flow through a LangGraph ReAct agent (default model Qwen3-32B through an OpenAI-compatible API, swappable via LLM_MODEL and LLM_BASE_URL; cross-model runs have also used Llama 3 8B and Mistral-Small 24B) which calls MCP tools exposed by a dedicated prover server. Session state lives in Redis; user accounts in Postgres.
The repository also hosts an ablation study — four main configurations (A/B/C/D) plus a supplementary A_STAR variant — comparing architectural design choices (identity protection, server-side state, smart Redis fallbacks, LLM summarization). See ARCHITECTURE.md for the complete design.
Contents
Just want to run it? → Quick start · Example queries. That's all you need — stop after step 4.
Reproducing the research / ablation study? → Ablation configs · Test suite · Grading · Sweeps
Here for the paper's artifacts? → Paper and artifact map · Reproduce the numbers offline · Models and providers · Deviations and known issues
Reference: Endpoints · Schema · Security · Config vars · Repo layout · Architecture deep-dive (
ARCHITECTURE.md)
Paper and artifact map
This repository is the artifact for A Natural-Language Interface to Zero-Knowledge Verifiable
Computation: Enforcing Correctness at the Tool Boundary (Shanto and Ramanan, Oklahoma State
University, 2026). Citation metadata is in CITATION.cff. The manuscript itself is not in this
repository. Code is MIT-licensed (LICENSE); the evaluation data is CC BY 4.0 (LICENSE-DATA).
The paper promises | Where it is |
Test suite: 75 main queries plus 7 verification queries |
|
Original faithfulness grader, as run |
|
Corrected faithfulness grader |
|
Experiment results: 24 files, 6,371 records |
|
Hand-read inspection dumps (Sections V-B, V-E) |
|
Every number in the paper, recomputed offline |
|
How to cite. GitHub's Cite this repository button reads CITATION.cff. Until the paper has a public identifier:
@misc{shanto2026nlzk,
title = {A Natural-Language Interface to Zero-Knowledge Verifiable Computation:
Enforcing Correctness at the Tool Boundary},
author = {Shanto, Md Nazrul Huda and Ramanan, Paritosh},
year = {2026},
note = {Oklahoma State University. Artifact: https://github.com/nazrulhuda/Natural-Language-Zero-Knowledge-Verification-via-Skeptical-MCP-Tools}
}Architecture at a glance
Service | Container | Port | Role |
Backend |
| 5001 | Flask UI + auth + LangGraph agent + MCP client |
Prover MCP |
| 8003 | FastMCP server exposing proof tools; owns all job/session state |
Redis |
| 6379 | Session state, job records, optional chat history (7-day TTL) |
Postgres |
| 5432 | Dataset-driven user accounts with bcrypt passwords |
Design rule: Flask stays thin (HTTP, auth, one security-critical Redis write for session ownership). The MCP prover owns all proof-lifecycle state and all COSMeTIC API calls.
External dependency: this chatbot is the front end to the separate COSMeTIC prover stack — it cannot run without it. COSMeTIC provides the prover APIs on ports 5012 (logistic_accuracy), 5013 (KS), 5014 (LRT) and the input-files service on 5015, and its Docker Compose project creates the regulatory_hypothesis_tests_default network that this stack joins. Start COSMeTIC before this stack — see the Prerequisites below.
Quick start
Prerequisites
Docker and Docker Compose
An API key for an OpenAI-compatible LLM endpoint. The paper's runs used DeepInfra (https://deepinfra.com); any compatible provider works through
LLM_BASE_URL.The COSMeTIC prover stack running (see Step 0) — without it this chatbot has no provers to talk to and no users to sign in as.
0. Start COSMeTIC (required first)
This chatbot is only the front end — it depends on the separate COSMeTIC prover stack, which must be set up and running before this one:
https://github.com/disys-lab/regulatory_hypothesis_tests (branch
forMCP); project page https://disys-lab.github.io/cosmetic/
Follow COSMeTIC's own README to set it up and run it — that is the authoritative source. Its setup is a real pipeline (SMT setup + EZKL zkSNARK generation via driver.py, plus a one-time per-API "Setup" step); do not expect a single up command to be enough. We deliberately don't reproduce those steps here because they live in (and will change with) that repo.
What this stack additionally needs from COSMeTIC once it's running:
Run it with the project name
regulatory_hypothesis_testsso its default network is namedregulatory_hypothesis_tests_default— the network this stack joins asexternal:git clone -b forMCP https://github.com/disys-lab/regulatory_hypothesis_tests cd regulatory_hypothesis_tests # ... set up / generate proof data per COSMeTIC's README, then: docker compose -p regulatory_hypothesis_tests up -d(If you start it under a different project name, update the
networks:block in this repo'sdocker-compose.ymlto match the actual network name fromdocker network ls.)The provers must expose ports
5012(ACC),5013(KS),5014(LRT), and input-files on5015.There must be proof data. COSMeTIC's
proofs/is gitignored, so a fresh clone has none until you run its proving pipeline. Without data,/admin/sync-dataset(Step 3) returns zero users and you can't sign in.Verify it's ready before continuing:
curl -s http://localhost:5015/input-files/listshould return a non-empty JSON list of input files.
1. Create .env
cp .env.example .env # then put your API key in DEEPINFRA_API_KEYThe template sets:
DEEPINFRA_API_KEY=your_key_here
LLM_BASE_URL=https://api.deepinfra.com/v1/openai
LLM_MODEL=Qwen/Qwen3-32B
CONFIG=C
EVAL_MODE=true
SECRET_KEY=change-me-in-productionCONFIG selects the ablation configuration (A / B / C / D, plus the supplementary A_STAR). C is the current/default full system. EVAL_MODE=true adds a tool_calls log to every /get response — useful for the test runner and for debugging. LLM_MODEL selects the model and LLM_BASE_URL the endpoint (default Qwen/Qwen3-32B on DeepInfra); it has also been run with meta-llama/Meta-Llama-3-8B-Instruct and mistralai/Mistral-Small-3.2-24B-Instruct-2506.
2. Build and start
docker-compose build
docker-compose up -dVerify both services came up with the right config:
docker-compose logs backend 2>&1 | grep "System configuration" | tail -1
docker-compose logs proverserver 2>&1 | grep "Prover server configuration" | tail -1The backend prints System configuration: C and the prover prints Prover server configuration: C (or whichever CONFIG you set) — both must match.
3. Wait for readiness and sync the dataset
Wait for the agent to initialize (probe /get directly — log line is unreliable under Flask debug mode's buffering):
until curl -s -X POST http://localhost:5001/get \
-H "Content-Type: application/json" \
-d '{"msg":"ping","session_id":"probe"}' 2>/dev/null | grep -q '"response"'; do
sleep 3
doneThen sync dataset users into Postgres:
curl -X POST http://localhost:5001/admin/sync-datasetThis fetches the input-files zip from COSMeTIC and upserts dataset_users rows named User1, User2, ..., each with one raw_hash and one input_data JSON blob. The shared password is password123 (or whatever DATASET_DEFAULT_PASSWORD is set to).
4. Open the UI
http://localhost:5001 — sign in as User1 / password123 and chat.
Running on a remote server?
localhost:5001/127.0.0.1:5001only work when the stack runs on the same machine as your browser — from a remote machine they showERR_CONNECTION_REFUSED. Instead, either browse the server's IP directly (http://<server-ip>:5001, if your network/firewall allows it), or forward the port to your machine — the VS Code Ports panel (forward5001), orssh -L 5001:localhost:5001 <user>@<server>. Note: the app binds0.0.0.0with Flaskdebug=True, so don't expose port5001to the public internet.
Example queries
Prove my data in KS
Check my status
Check where my data has been used
Download the proof
Verify my proof # confirm the proof is cryptographically valid
Prove hash abc123 in LRT # explicit hash (not "my hash")That's it for running the chatbot. Everything below is for the ablation study and evaluation — skip it unless you're reproducing the research.
Ablation study — configurations
Config | Philosophy | Identity protection | Conversation history | Redis fallbacks (B4/B5/B6) | LLM summarizes response |
A | "Trust the LLM" | off | on (replay history) | off | on |
B | "Distrust LLM memory" | on | off | partial (B4 only; B5/B6 off) | on |
C | Full system (default) | on | off | all on | on |
D | No LLM summary layer | on | off | all on | off (deterministic formatter) |
A_STAR | "Identity in the prompt" (supplementary) | off ( | on (replay history) | B4 on; B5/B6 off | on |
To switch configs, edit .env and restart:
sed -i 's/^CONFIG=.*/CONFIG=D/' .env
docker-compose down && docker-compose up -dSee ARCHITECTURE.md §12 for the full gate-by-gate code references.
Running the ablation test suite
The test runner (test_runner.py) executes test_suite.json (75 executable queries across 7 source types; the file also holds 5 standalone Source-3a entries that are skipped at runtime) against the running backend for a given CONFIG and writes results to results/results_{CONFIG}.json (the results/ directory is created automatically; override with --results-dir). Runs are resumable. The runner refuses to start unless LLM_MODEL is set, and stops if the reference proof job does not reach done within about 17 minutes (see Deviations and known issues). Pass --test-suite eval/test_suite_verify.json to run the 7-query verify_proof evaluation suite instead (results still land in results/results_{CONFIG}.json).
# Pilot: one run through the 75 queries (run from the repo root)
PYTHONUNBUFFERED=1 python -u eval/test_runner.py --config C --runs 1 --fresh
# Full: five runs (starts fresh; takes several hours)
python eval/test_runner.py --config C --runs 5 --fresh
# Continue an interrupted run (omit --fresh)
python eval/test_runner.py --config C --runs 5
# Re-execute any records that previously errored
python eval/test_runner.py --config C --runs 1 --retry-failedInstall the runner's requirements with pip install -r requirements.txt. In Docker-only setups, run it from the host with the ports exposed. The runner logs into User1, auto-creates a reference completed job at startup (skipped for Config A, where the identity gate is disabled), and injects test fixtures directly into Redis / Postgres as needed per query.
Grading results
To reproduce the paper's tables, use eval/reproduce_paper_numbers.py instead; it reads the released files as they are named.
grading_script.py is the original grader. It reads results_{A,B,C,D}.json from --results-dir (default results/), which is the name the test runner writes, + test_suite.json, and prints the metric tables (tool selection, parameter correctness pre/post, task completion, response faithfulness, tool-use rate) as mean ± std across runs, with per-source and Config-A auth/non-auth breakdowns:
python eval/grading_script.py --configs A,B,C,D # defaults: results/ dir, eval/test_suite.jsonWhat each metric means
Metric | Question it answers | How it's scored |
Tool Selection | Did the agent call the right tool? | First tool call vs |
Param Correctness (pre) | Were the tool arguments correct as the LLM emitted them, before any backend correction? | Each |
Param Correctness (post) | Were the arguments correct after the interceptor fixed them? | Same check against |
Task Completion | Did the user get the correct end-to-end outcome? | Response text must contain all |
Response Faithfulness | Does the user-facing reply match what the tool actually returned? | Original grader; the paper reports the corrected grader in |
Tool-Use Rate (S7) | On bait queries, did the agent call a tool instead of guessing? | Source-7 only ( |
Results are reported as mean ± std across runs. Source-6 multi-step scenarios use cascade scoring: if an early step fails, dependent later steps are marked unreachable rather than counted as separate failures (see ARCHITECTURE.md §13.4).
Multi-model / multi-config sweeps
Shell orchestrators drive full sweeps end-to-end — they edit .env, recreate the backend + proverserver, run the suite, and archive results as results/results_{model}_{config}.json:
./eval/run_llama_all.sh # Llama 3 8B × A,B,C,D,A_STAR -> results/results_llama_{config}.json
./eval/run_mistral_all.sh # Mistral 24B × A,B,C,D,A_STAR -> results/results_mistral_{config}.json
./eval/run_verify_all.sh # verify_proof suite: Qwen A-D, Mistral C-D (its Llama C-D runs were not completed)Key endpoints
Endpoint | Auth | Purpose |
| — | Chat UI |
| — | Sign in as a dataset user |
| — | Clear session |
| — | Current auth status |
| login required | Masked preview of the user's stored |
| — | Chat endpoint (session-scoped if logged in) |
| login required | Proxy a proof-file download |
| login + owner | Inspect Redis session state |
| optional secret | Re-run the dataset sync |
Schema
Single init script at sql/002_dataset_and_zips.sql, applied automatically by the Postgres container:
dataset_users—id(uuid PK),username(unique),password_hash(bcrypt),raw_hash,input_data(JSONB),source_file,zip_archive_id(FK),created_at,updated_atinput_zip_archives—id(uuid PK),source_url,stored_path,file_size_bytes,fetched_at
Manual signup is not supported — accounts are created only by /admin/sync-dataset.
The authoritative dataset is the COSMeTIC input-files zip ingested into Postgres by
/admin/sync-dataset.
Reproducing the paper's numbers offline
Every figure in the paper's tables and prose that derives from the logs can be recomputed from
results/ alone, with no CoSMeTIC stack, no LLM and no network:
python eval/reproduce_paper_numbers.py # prints every derived figure with its definition
python eval/reproduce_paper_numbers.py > out.txt && diff out.txt eval/expected_output.txt
python eval/test_grading_faithfulness_v2.py # four synthetic controls; hand-label agreement 150 of 151eval/expected_output.txt is the output as saved at release. Figures marked [H] in the
output were established by hand-reading the dumps in reports/ and are reported, not recomputed.
Only the standard library and the two graders in eval/ are needed.
Models and providers
Model | Identifier | Configurations | Provider |
Qwen 3 32B (primary) |
| A, B, C, D, A*, verification A to D | Groq during development, DeepInfra for later runs; the provider of the main A to D study was not recorded per run |
Mistral Small 3.2 24B |
| A, B, C, D, A*, verification C and D | DeepInfra |
Llama 3 8B |
| A, B, C, D, A* | DeepInfra |
Qwen 2.5 72B | not recorded | B only | not recorded |
Qwen 3 235B-A22B | not recorded | B only, one run plus 11 queries | not recorded |
Result records written before September 2026 carry no model or provider field; the model per file comes from the file name and the sweep scripts. See the provenance caveat under Repository layout.
Deviations and known issues
Stated plainly, because a reader of the code would otherwise infer the opposite.
Trust label tiers. The evaluation ran a two-tier label (
[Backed by COSMeTIC prover],[Not backed by COSMeTIC prover]). The releasedcompute_trust_labelhas four tiers; the two cryptographic tiers never appear in any logged turn and are unevaluated.Post-run changes to the runner. The
llm_modelandllm_provider_base_urlrecord fields, the refusal to start withoutLLM_MODEL, and the hard failure when the reference job does not reachdonewere all added after the reported runs. The sweep scripts now pinLLM_MODEL; at run time they inherited whatever.envheld.Reference-job fixture. In the Mistral, Qwen 2.5 72B and Qwen 3 235B sweeps the reference job stayed
queuedthroughout (the poll timed out and the runner continued on a warning). Status- and download-dependent cells for those sweeps are not comparable with Qwen 3 32B or Llama; within-model comparisons are unaffected. Per-file state is inresults/RESULTS_MANIFEST.csv.Five authored queries were never executed.
S3a_01toS3a_05ineval/test_suite.json; seeeval/MANIFEST.md.Grader label.
grading_script.pynow prints "Tool-Use Rate (S7)" where it printed "Tool Bypass Rate (S7)"; the value is unchanged and higher is better.Endpoint variable.
LLM_BASE_URLwas added toapp.pyat release with the DeepInfra endpoint as its default, so the value the runner records is the value the app uses.Known gaps in the design, as evaluated. A supplied
job_idis not checked against the session, so an invented one defeats both the fallback and the override. The nonce is fixed at[[0.0, 0.0, 0.0]], so proofs are not tied to individual verification requests. Hashes are scrubbed only at display time; tool outputs, including dataset hashes, job identifiers and the account UUID, reach the model provider in every configuration.Data. All accounts are synthetic (
User1toUser54, seeded at run time from CoSMeTIC's synthetic input files); one generated test-account UUID appears in the logs. No real participant or patient data exists anywhere in this repository.
Security notes
Local defaults, not production values.
docker-compose.ymlshipsPOSTGRES_PASSWORD=mcp_passwordandSECRET_KEY=dev-secret-change-me, and the synthetic dataset users sharepassword123. Set real values before any network-reachable deployment. The evaluation runner reads the same defaults fromPG_PASSWORD,EVAL_USERNAMEandEVAL_PASSWORD.Passwords are bcrypt-hashed.
raw_hashis never returned in full; the/api/me/hashendpoint returns a masked preview.User identity is enforced by HTTP header injection in the backend's MCP interceptor (
x-user-id) and is never trusted from a tool argument (except in Config A, which disables this protection deliberately for the ablation).Sessions are claimed on first request — Redis stores
owner_user_idand rejects cross-user session access afterward.Qwen3-32B emits
<think>...</think>reasoning blocks; these are stripped frombot_responsebefore persistence, trust labeling, or user display so they don't pollute Config A history or skew grading.
Configuration reference
Variable | Used by | Description |
| backend | DeepInfra API key (required) |
| backend | Model identifier (default |
| backend | OpenAI-compatible endpoint (default |
| backend | Flask session signing key |
| backend | MCP URL (default |
| proverserver | COSMeTIC hostname (default |
| both | Redis connection |
| both | Postgres DSN |
| both | Shared volume for proof artifacts |
| backend | Dataset sync source |
| backend | Local storage for dataset zips |
| backend | Default password for dataset users (default |
| backend | Optional; protects |
| both | Ablation selector ( |
| backend | Enables |
Operations
docker-compose ps
docker-compose logs -f backend
docker-compose logs -f proverserver
docker-compose down
docker-compose build backend # rebuild after requirements changeRepository layout
Runtime code at the root:
app.py,proverserver.py,context_manager.py,account_store.py,dataset_sync.py, plustemplates/,static/,sql/, the Dockerfiles, anddocker-compose.yml(these must stay at the root — they're referenced by the Docker build context and compose mounts).eval/— all evaluation tooling:test_runner.py,grading_script.py,grading_faithfulness_v2.py,reproduce_paper_numbers.py, therun_*.shsweep orchestrators, andtest_suite*.json. Run these from the repo root (e.g.python eval/test_runner.py …); paths are anchored to the script location, so they also work if invoked from elsewhere.results/— allresults_*.jsonproduced by the test runner and sweeps (created automatically; readers/writers default here).Provenance caveat. The
llm_modelandllm_provider_base_urlfields were added to the result schema in September 2026, after the runs reported in the paper were executed. Result files produced before that date therefore contain no record of which model or which API endpoint produced them; the model was selected through theLLM_MODELenvironment variable and was not captured per run. The two sweep orchestrators (run_llama_all.sh,run_mistral_all.sh) also did not setLLM_MODELat that time, so they inherited whatever value.envalready held. Onlyrun_verify_all.shpinned model identifiers explicitly. The runner now refuses to start unlessLLM_MODELis set, and records both fields in every record, so this gap cannot recur. Determining retrospectively which provider and model served a given 2026 sweep requires the provider's usage history, not this repository. Development before the cross-model runs used Groq's API; DeepInfra was adopted for the other models, and the released build targets the OpenAI-compatible DeepInfra endpoint by default.reports/— the hand-read inspection dumps (inspection_*.txt), and the 252 classified wrong-port replies.eval/reproduce_paper_numbers.pyandeval/expected_output.txt— offline recomputation of every figure in the paper.eval/MANIFEST.mdandresults/RESULTS_MANIFEST.csv— what the suite contains and what each results file is.data/input_zips/(not in the repository) — created at run time when/admin/sync-datasetfetches CoSMeTIC's synthetic input archive and seeds theUser<N>accounts.LICENSE(MIT, code),LICENSE-DATA(CC BY 4.0, data),CITATION.cff,.env.example,SHA256SUMS.txt(checksums of the results, suites, graders and reproduction output as released).downloads/(proof artifacts) — runtime data, not in the repository.
Further reading
ARCHITECTURE.md— complete code-verified architecture (14 sections, ~1371 lines)§12 — CONFIG mechanism and the feature matrix
§13 — Test suite structure
§14 — Test runner design
This server cannot be deployed
Maintenance
Related MCP Connectors
Discover, invoke, and trustlessly verify ForceDream AI agents with cryptographic proofs. 17 tools.
Authenticated async GPT-5.6-sol Agent agent with status polling and artifact results.
Authenticated LLM Traced Agent