Verification¶

Verification runs validation on demand from the term-store server.

The term store remains an orchestrator. It starts a configured proof-assistant or preprocessor process and reports the result; it still does not parse or type-check record bodies itself.

Configure A Database¶

A database needs a language and proof-assistant source path:

curl -s \
  -X PUT \
  -H 'Content-Type: application/json' \
  -d '{"language":"agda","proofAssistantPath":"examples/agda/DemoStep1Numbers.agda"}' \
  'http://127.0.0.1:8080/admin-api/v1/databases/demo'

create-from-source also stores the source path as part of database metadata.

Run Verification¶

curl -s \
  -X POST \
  'http://127.0.0.1:8080/admin-api/v1/databases/demo/verify'

The response is a normal JSON result even when validation fails:

{
  "database": "demo",
  "language": "agda",
  "backend": "agda-native",
  "proofAssistantPath": "examples/agda/DemoStep1Numbers.agda",
  "ok": false,
  "exitCode": 42,
  "signal": null,
  "durationSeconds": 0.25,
  "stdout": "",
  "stderr": "validation output"
}

Protocol problems, such as an unknown database or missing proof-assistant path, are returned as API errors instead.

Backend Selection¶

The SQLite store accepts:

--verification-backend auto
--verification-backend agda-native
--verification-backend lean-preprocessor
--verification-backend rocq-preprocessor
--verification-backend preprocessor

auto selects:

Language	Backend
`agda`	`agda-native`
`lean`	`lean-preprocessor`
`rocq`	`rocq-preprocessor`

preprocessor is currently valid for Lean and Rocq verification. Agda verification uses native Agda in the implemented minimal profile.

Generated Files¶

Lean and Rocq verification writes generated preprocessor output under:

artifacts/generated/verification/

The result may include generatedPath. Native Agda verification does not generate a preprocessed file.

Native Agda Requirement¶

Agda verification executes AGDA_BIN when that environment variable is set, or agda from PATH otherwise. Repository test helpers additionally require that the executable has MLTTDB --tdb-mode support and was installed from the current Agda subrepository build inputs.