Narya proofs, one hole at a time

narya-mcp is an MCP server for the Narya proof assistant. It gives an agent the loop that a person gets in Emacs ProofGeneral: the open holes of a file with their contexts and types, a suggested split, checks of candidate terms, solutions, and a recheck of only the changed part of the file. The server drives Narya's own ProofGeneral mode, so every answer comes from Narya.

Source code on GitHub (Apache-2.0) · Install · Narya bug report

narya_start(file = "plus.ny")

?0   n : ℕ
     ⊢ refl ℕ (plus 0 n) n

narya_split(hole = 0, term = "n")

match n [ zero. ↦ ? | suc. n′ ↦ ? ]   not committed

narya_solve(hole = 0, term = "match n [ zero. ↦ ? | suc. n ↦ ? ]")

?1   n ≔ 0 : ℕ
     ⊢ refl ℕ 0 0
?2   n : ℕ
     ⊢ refl ℕ (suc. (plus 0 n)) (suc. n)

narya_try(hole = 2, terms = [ … ])

type_mismatch  refl (suc. n)
               n does not equal plus
ok             refl ((x ↦ suc. x) : ℕ → ℕ) (zero_plus n)

edit plus.ny, then narya_sync and narya_check_file

sync: 1 command retracted, 1 replayed, no holes
check: ok, clean

A real session on a small file: the proof that 0 + n = n, by induction on n. Narya prints the type Id ℕ a b as refl ℕ a b. Responses are shortened.

17MCP tools

1Narya process per session

22failure reasons in a fixed set

2benchmarks that decide changes

1Narya bug found and reported

How it works

Sessions: narya_start loads a file into a live Narya process, one command at a time, as ProofGeneral does. Each hole comes with its position in the file, its context and its type.
Recheck after an edit: Narya counts its undoable commands. narya_sync compares the file with the loaded commands, undoes the commands from the first change, and replays the rest. Imports stay loaded, so a recheck takes seconds where a fresh check loads every import again.
Final check: narya_check_file runs a fresh Narya process and gives the verdict: errors with line and column, assumed axioms and open holes.
Long computations: A command under work that runs longer than 120 seconds is interrupted. Thus a term whose normalization grows without limit does not use all the memory, and the session usually stays alive.
Larger machines: A launcher can run Narya on another machine over SSH, in a copy of the project with precompiled files.

Tools

tool	purpose
`narya_start`, `narya_sync`	Load a file into a session; recheck it after an edit.
`narya_holes`	Open holes with position, context and type.
`narya_split`	Narya's proposed shape for a hole: abstraction, tuple, comatch, constructor or match.
`narya_try`	Check up to 20 candidate terms against a hole without solving it.
`narya_synth`	Type or normal form of a term, also in the context of a hole.
`narya_solve`	Solve a hole; return the edit for the file.
`narya_exec`, `narya_check`	Run commands in a session; check a snippet in the context of a file.
`narya_check_file`, `narya_audit`	Fresh check of a file; axioms and holes in its import closure.
`narya_search`, `narya_lookup`, `narya_toc`	Find declarations; read one by name; outline a file.
`narya_close`, `narya_sessions`, `narya_health`	Sessions, configuration and Narya version.

Search

Narya has no search command. narya-mcp indexes every definition of the project with its statement and the comment above it, and ranks with BM25. Identifiers are split at _ and ., and abbreviations are learned from the project: a comment that says "associativity" above a name with assoc. Results can be limited to what a file imports. For a hole, the constants of its goal are added to the query. Narya prints goals in normal form, so the statement of the definition that holds the hole is used too.

Measurement

Every call is logged with its tool, time and result. A failure has a reason from a fixed set, so the log shows which tools fail and why. Two benchmarks decide which changes stay:

Retrieval: For a definition, the query is its comment and statement, and the answer is the set of lemmas that its proof uses. Modules are split in two halves, and each change is compared with the current settings by a paired bootstrap. On symmetry-narya, with about 17,000 declarations, only the statements gave a significant gain over names alone: recall at 10 went from 0.33 to 0.38.
End to end: Definitions of a project become holes. Agents with a budget work in an isolated copy, and a separate check accepts a result only if the file is clean and the statements did not change. Two groups of agents differ only in the tools that they get.

Results so far:

When only one definition is hidden, agents solve almost every task with or without the interactive tools. Tasks that hide all proofs of a module show differences, but ten modules are not enough for a significant result.
The log showed that agents did not use narya_sync, and that terms with runaway normalization took 28% of the tool time. The server now points agents to the session loop and interrupts such terms.

Found in Narya

During a benchmark run, a check stopped with an internal error of Narya: anomaly: failure: Meta.Map.find_opt. Narya loads a compiled file but keeps the old file number in the keys of its metavariable table, so a lookup fails when the number changes. The report has a two-file example, a one-line fix and a regression test. Until a fix is released, narya-mcp checks from source when this error occurs.