AIRAS

Draft the analysis of a study from its record and run outputs. Reads `.research/record.json` and `.research/results/` in the clone at `local_path`: every live hypothesis and claim with its frozen criterion and predicted interval, the observed difference, and the verdict the criterion derives. `model` (required; see `get_available_llms`) reads them and returns `analysis` — per claim, then the hypothesis, then limitations and open questions — plus each claim's verdict and observed difference. Nothing is written: the analysis is a draft for the Discussion, to be checked against the numbers like any other prose. Without an LLM key, `get_prompts(step="experiment_analysis", local_path=...)` renders the same prompt for you to answer.

Add declarations to the record; nothing already in it ever changes. The record only grows: every committed revision must contain the one before it whole, so this tool appends and never edits. `hypotheses` appends whole new hypotheses; `claims`, `tables`, `charts` and `notes` append under the hypothesis named by `hypothesis_id`. Entry shapes are the ones `preregister_record` documents. Revising a frozen entry means appending a new one with the *same id* — the later entry is the live one and the earlier stays readable in place. That is also how a design or a run is added to an existing claim: append the claim again, with the extra design. Use this for exploratory extensions (declare the claim and its runs first, then execute — results for an undeclared run fail verification). The append is committed in the same step (`commit` in the result); anything a run should count as evidence for must be in that commit's history before the run executes, so a claim declared after its run stays unverified forever. A seyval claim appended here needs its criterion and prediction like one preregistered; `claims.tex` is re-rendered and committed alongside. `literature` appends sources the paper came to rest on after the freeze (same entry shape as `preregister_record`); `passages` append under the source named by `source_id` (`{"node_type", "quote", "anchor"?}`). A quote must be copied from that source's `fulltext.txt`, or the append is refused.

Start an experiment run (asynchronous). The code must already be pushed. `run_stage` selects the stage, in increasing scale: "sanity" for a quick correctness run, "pilot" for a small preliminary one, "full" for the real experiment. `run_id` identifies the experiment run defined by the experiment code (one config/run/{run_id}.yaml). Pass the same stage to `import_run_outputs` to collect the run's results afterwards. `backend` selects where the run executes; either way the run's outputs stay on the backend's side until `import_run_outputs` copies them into the repository with their provenance, and the returned `execution_id` is what that call and `get_experiment_run_status` take. - "github_actions" (default): dispatches run_experiment.yml in the experiment repository; `runner_label` picks the runner. Requires GH_PERSONAL_ACCESS_TOKEN. - "seyval": executes on the Seyval compute platform. `compute_id` picks the machine — normally a cluster you registered, "byo:<uuid>" from the Seyval MCP server's `list_computes`; it defaults to SEYVAL_COMPUTE_ID, and without either the run goes to Seyval-managed compute. `compute_type` sets the resource request in both cases (e.g. "cpu-general", "gpu-a10"). `workspace_id` (default SEYVAL_WORKSPACE_ID) is required when your key sees several workspaces: a repository is registered into one for good. `user_dockerfile_path` (default "Dockerfile") makes Seyval build the committed Dockerfile as-is instead of generating an environment; pass None to let it generate one. Its CMD then runs verbatim, so the run's command is `command_args` (argv), which defaults to `make run RUN_ID=<run_id> MODE=<run_stage>` — the repository's one entry point, the same one run_experiment.yml calls. The Makefile reads the run's kind from `config/run/<run_id>.yaml`: an experiment runs `src.main`, airas-eval and `src.evaluate` (a run that stops after `src.main` writes no metrics.json and fails verification); a `lean` run builds the module and writes `lean.json`. Lean has sanity and full stages only. `inputs_from_runs`, `time_limit` and `resource_count` apply to "seyval" only. `inputs_from_runs` takes `execution_id`s of earlier completed runs and restores their outputs into this run's working directory at the paths they were written to, so a run can consume what a previous one produced. `time_limit` (e.g. "24:00:00") and `resource_count` request per-run resources from a registered cluster; accepted values are in its `run_profile` from `list_computes`.

Start paper-reproduction code generation on GitHub Actions (asynchronous). Dispatches a workflow that reads `paper_url`, picks a figure or table to reproduce (guided by `instruction`), and generates the code. Returns immediately with `dispatched`; track progress with `get_workflow_runs` and run the experiment with `dispatch_paper_reproduction_run` once the run succeeds. `model` (required) is forwarded to the workflow as the coding- agent model (`model_name`) — call `get_available_llms` to list valid models. Requires GH_PERSONAL_ACCESS_TOKEN. Returns repro_id, which identifies this reproduction's directory (.reproduction/<repro_id>/) and must be passed to every subsequent reproduction tool.

Start a paper-reproduction run on GitHub Actions (asynchronous). Use after a `dispatch_paper_reproduction_generate` run has succeeded. `repro_id` is the ID returned by `dispatch_paper_reproduction_generate`. Returns immediately with `dispatched`; track progress with `get_workflow_runs` and collect outputs with `fetch_paper_reproduction_results`. Requires GH_PERSONAL_ACCESS_TOKEN.

Start a hyperparameter tuning run for a paper reproduction (asynchronous). Requires a completed paper reproduction on the branch. `repro_id` is the ID returned by `dispatch_paper_reproduction_generate`. Returns immediately with `dispatched`; track progress with `get_workflow_runs` and fetch results with `fetch_parameter_tuning_results`. Requires GH_PERSONAL_ACCESS_TOKEN.

Download the artifacts produced by a GitHub Actions workflow run. `workflow_run_id` comes from `get_workflow_runs`. Useful for inspecting logs and outputs of a specific run. Requires GH_PERSONAL_ACCESS_TOKEN.

Read what the runs left under `.research/results/` in the clone. Use after `import_run_outputs` has committed a run's outputs and the clone has pulled them. Returns, per results directory, the `metrics` (metrics.json), the airas-eval `evaluation` report (metrics, curves, skipped metrics with reasons), the `figures` under it, and the entry the provenance manifest holds for it (None when the directory arrived some other way, which `verify_record` will fail). Nothing is interpreted here: the record's verdicts come from `update_record`.

Download a paper's full text into a local file you then read yourself. Identifiers are tried in the order arXiv ID, then PDF URL, then DOI, and passing several is useful rather than wasteful: arXiv IDs are fetched straight from arXiv, DOIs are resolved to an open-access PDF through Semantic Scholar, and a DOI that resolves to nothing falls back to the `pdf_url` you supplied. Pass both whenever `search_papers` gave you both — a DOI alone returns only the abstract for any paper Semantic Scholar's open-access index does not cover, bioRxiv among them. On `status="fulltext"` the text is written to `fulltext_path` under `~/.airas/cache/fulltext/` (pages separated by form feeds) and nothing is returned inline: a paper runs to 80k+ characters, so read the file with your own tools, in parts or by searching it. `total_chars` says how long it is. `abstract_only` returns the abstract inline and writes no file; `not_found` means nothing at all was reachable. The cache keeps files for seven days; nothing is written to the research repository or the record — that happens at `preregister_record`, which takes the papers the hypothesis rests on together with their `fulltext_path`. No API keys required.

Fetch and validate the results of a paper reproduction run. Use after a `dispatch_paper_reproduction_run` has succeeded. `repro_id` is the ID returned by `dispatch_paper_reproduction_generate`. Returns the self-reported result, a validation verdict, and the reproduced figure/table. `model` (required) is the LLM used to judge the reproduction — call `get_available_llms` to list valid models. Requires GH_PERSONAL_ACCESS_TOKEN and an LLM provider API key.

Fetch the results of a parameter tuning run. Use after a `dispatch_parameter_tuning_run` has succeeded. `repro_id` is the ID returned by `dispatch_paper_reproduction_generate`. Returns the tuning summary and optimization figure. Requires GH_PERSONAL_ACCESS_TOKEN.

Report which LLMs are usable with the currently configured API keys. Reads credentials fresh (so keys added or rotated since the server started are picked up) and, for each known LLM provider, reports whether its required API key(s) are present. Call this before the LLM-backed tools (`analyze_experiment`, `verify_paper_values` with a model) to know which will run and which model names you may pass — a tool whose model belongs to an unconfigured provider fails fast with the missing key named. This tool itself needs no API key. Set `include_models` to true to also list, per configured provider, the model names in litellm's catalog. It defaults to false because some providers return hundreds of models, which bloats the response; request it only when you need to choose a specific model. Scope: this reports the **LiteLLM** view — provider credentials (`LITELLM_PROVIDER_REQUIRED_ENV_VARS`) and litellm's model catalog. Every generation tool executes via litellm and accepts any model name litellm can route to the configured providers, so a listed provider/model is usable by all of them. Returns: - `any_provider_configured`: whether at least one provider is usable - `configured_providers`: sorted provider names that are ready - `providers`: per-provider `configured` flag, `required_env_vars`, `missing_env_vars`, and (when configured and requested) `models` / `model_count` - `setup_instructions`: how to add keys, present only when none are set

Check one experiment run and fetch its execution logs (non-blocking). `execution_id` identifies the run on the selected `backend`: the `execution_id` returned by `dispatch_experiment(backend="seyval")`, or a `workflow_run_id` from `get_workflow_runs` for "github_actions" (pass `github_owner` and `repository_name` in that case). Returns the run status and, once the run has finished, the last `log_tail_lines` lines of stdout and stderr where the backend provides them — use stderr to diagnose execution errors and fix the experiment code locally.

Look up canonical documentation endpoints for AI research libraries. Covers ~165 libraries organized as domain > category (the same shared taxonomy as retrieve_models / retrieve_datasets). Domains: foundations, language, vision, audio, multimodal, reinforcement_learning, time_series, graph, systems, statistics, machine_learning, decision_science, interpretability, science. For each library returns the official docs URL, the source repository, and — where the project publishes one — its `llms.txt` / `llms-full.txt` endpoint, which serves the current documentation in a machine-readable form. Fetch those endpoints to get up-to-date library guidance while writing experiment code. Pass `library` for one entry; `domain` or `category` to filter the listing; no arguments to list everything. No API keys required.

The prompt for an authoring step, so you write the result yourself — no LLM API key required. The skills route each authoring step here. The prompt says what the step's output must contain and where it goes; the material (the record, the run outputs, the papers) is in the clone, which you read yourself. A step that also has a backend-LLM tool (`analyze_experiment`) renders the very prompt the tool sends, from the clone at `local_path`, so what you read is what the tool would have read. Steps: "hypothesis_and_design", "experiment_code", "paper_writing" (plain text; `local_path` is not needed) and "experiment_analysis" (needs `local_path`). Returns `prompt`, the `output_json_schema` to produce, and a `flow` note on where the output goes.

Check the status of recent GitHub Actions runs in the experiment repository (non-blocking). Returns the most recent workflow runs with their status, conclusion and the commit they ran on, newest first. Runs from every trigger are included, so this is also how the record gate (`Verify Record`, which runs on push) and `Publish Paper` are read: pass `branch_name="verify"` to follow the staging ref, and match `head_sha` against the sha you pushed. Pass `event="workflow_dispatch"` to see only runs started by `dispatch_experiment`. Poll it between other work instead of waiting. Requires GH_PERSONAL_ACCESS_TOKEN.

Copy a finished run's result files from the backend's store into the repository. Neither backend pushes results back: Seyval keeps them in its storage and a GitHub Actions run uploads them as a workflow artifact. This downloads everything the run wrote under `.research/results/` and commits it to `branch_name` at the same paths, together with `.research/results/.provenance.json` declaring, per results directory, the backend, `execution_id`, commit, dispatch parameters and each file's sha256. `verify_record` pins its cross-check to that declaration, so results that arrive any other way, or are edited afterwards, fail. `execution_id` is what `dispatch_experiment` returned and `backend` the one it ran on. Call it once `get_experiment_run_status` reports a terminal status. A repository path holds one run's results regardless of stage, so importing a provisional stage ("sanity" or "pilot") replaces the full run's results at the paths they share, and requires `confirm_overwrite=True`. "visualization" needs no confirmation because such a run adds figures derived from an earlier run. File contents never leave airas. Requires GH_PERSONAL_ACCESS_TOKEN, and SEYVAL_API_KEY for `backend="seyval"`.

Create a link that opens the paper in Overleaf for editing. Returns `overleaf_url`, which must be shown to the user as a clickable link. Opening it in a browser packages the LaTeX project (main.tex, bibliography, template assets, plus every figure PDF under `.research/results/` and `.research/diagrams/` mapped into `images/`) and submits it to Overleaf, creating a new project in the user's Overleaf account (login required; each click creates a new project). By default the project is read from the experiment repository on GitHub (main.tex must have been pushed; requires GH_PERSONAL_ACCESS_TOKEN, private repositories work). Pass `local_path` — the absolute path of your local clone — to read the working tree on disk instead: no push needed, and locally rendered figures are included as-is. Starts the local dashboard API in the background if needed.

Create a GitHub repository for running experiments, ready to enforce. Creates the repository from the AIRAS experiment template and the working branch, and returns `html_url` and `clone_url` so the next step, cloning it locally, needs nothing reconstructed by hand. Run it once before writing experiment code, then `set_github_actions_secrets`. It also protects `protected_branch` (the working branch unless another is named) and points GitHub Pages at the artifact the `Publish HTML` workflow deploys. Both are setup whose absence is invisible: without branch protection a red CI run can simply be pushed past, so they happen here rather than being left to a later call. Branch protection is what makes the record's guarantees enforceable instead of advisory: the record and paper gates become required status checks, admins included, with force pushes and deletions refused because the record's evidence is its git history. Squash and rebase merging are disabled repository-wide, since verification asks whether each run's recorded commit is an ancestor of HEAD and a rewrite breaks that. So work on a branch and, once the gate is green on a commit, fast-forward that same sha onto the protected branch. On GitHub's free plan branch protection is only available on public repositories, which is why `is_private` defaults to false. A step that fails does not abort the creation; it is reported in `warnings` and in its own flag. **A repository whose `branch_protected` is false is not enforcing anything**; say so rather than proceeding as though it were. The call is safe to repeat on a repository it created, and re-running it is how a failed CI setup gets repaired, e.g. once the token has admin rights. Requires GH_PERSONAL_ACCESS_TOKEN with admin rights on the repository.

Create the research record before any experiment has run. Writes `.research/record.json` — the canonical record the whole verification system keys on — and commits it in the same step (`freeze_commit` in the result). That commit is the freeze point: every later revision must *contain* this one whole, so a claim cannot be reworded, its criterion cannot be moved, a run's conditions cannot be changed and a result cannot be dropped once written. The record is a tree, read as "to support this hypothesis, these claims; to verify this claim, these designs; a design is these runs": hypotheses: [{ "id": "h1", "statement": "the hypothesis, in prose", "assumptions": ["what must be granted for the claims together to " "imply h1, naming the claims concerned", ...], "claims": [{ "id": "c1", "statement": "one assertive sentence", "rationale": "why c1 holding is evidence for h1, and for which part", "verifier": {"kind": "seyval"}, "criterion": {"metric": "accuracy", "subject": "proposed-...", "reference": "comparative-1-...", "op": ">=", "margin": 0.02}, "prediction": {"low": 0.02, "high": 0.04, "basis": "pilot run"}, "designs": [{ "id": "d1", "summary": "...", "runs": [{"run_id": "proposed-...", "description": "...", "params": {"mode": "full"}}] }] }], "tables": [...], "charts": [...], "notes": [...] }] `literature` is what the hypothesis rests on, pinned in the same commit. Each entry is a paper (`doi` / `arxiv_id` from `search_papers`, with `title`, `authors`, `year`, `venue`, `pdf_url`, and the `fulltext_path` `fetch_paper_fulltext` returned), a repository (`url`, a full 40-hex `commit`, `files`) or a study AIRAS produced (`airas_record`), each with `passages`: `[{"node_type": "gap|claim|result|method|setup|definition", "quote": "<copied verbatim from the full text>", "anchor"?}]`. A registry (doi.org, arXiv, git) must confirm each source exists, its text is snapshotted under `.research/sources/<id>/`, and every quote is checked against that snapshot. Sources get ids in the order given (`s1`, `s2`, …) and passages `p1`, `p2`, … within each, so a hypothesis's `grounded_on`, a claim's, design's or run's `cites_passages` and a criterion's `reference_passage` name them as `"s1.p2"`: what the declaration rests on, in the prior work's own words. The gate refuses a passage no source declares. `run_id` names the results directory the run will produce and must be unique across the whole record — a run belongs to exactly one claim. (Not a bare number: `criterion.reference` reads a number as a constant.) The claims are meant to imply the hypothesis together (c1 ∧ … ∧ cn ⇒ h1). `rationale` says why each claim is a member of that set; the hypothesis's `assumptions` say what has to be granted for the conjunction to reach h1 — a proxy metric standing for the property, generalisation beyond the datasets run, and the like. Every claim supported leaves exactly the assumptions unverified, so they are what the paper states as such; claims.tex lists them under the claims. `verifier` says what verifies the claim and sets its `verified` and `verdict`; one per claim (a claim needing both a proof and an experiment is two claims), and required. The kind decides what `params` declares and what the gate re-derives: seyval (experiment) params = dispatch conditions, e.g. {"mode": "full"}, checked against what the platform recorded. `criterion` is the falsification line, required: (subject.metric - reference) op margin, where reference is a run under this claim (its same metric) or a constant; exactly at the margin counts as met. `prediction` is the interval the difference is expected to land in, required, a range never a point, with where it comes from. Verdict: supported/refuted by the criterion on the runs' metrics; inconclusive when the metric cannot be resolved. lean (theory) {"kind": "lean", "toolchain": "leanprover/lean4: v4.33.1", "mathlib_rev": "<sha>", "allowed_axioms": [...]}; params = {"module": "Airas.Thm1", "decl": "thm1", "statement": "<the type `#check @thm1` prints>"}. The toolchain and mathlib_rev are the repository's `lean/lean-toolchain` and `lean/lake-manifest.json`. The run is dispatched like an experiment (`dispatch_experiment` with a `config/run/<run_id>.yaml` holding kind: lean, module, decl) and writes `lean.json` into its results directory. Verdict: supported iff the result has no errors (build failed, sorry, statement drift, module/decl/toolchain/ mathlib_rev other than declared, an axiom outside allowed_axioms); else inconclusive — Lean cannot refute. llm_judge (qualitative) {"kind": "llm_judge", "model": "<dated id>", "rubric": "<repo path>", "temperature": 0, "samples": 5}; params = {"evidence": ["<repo paths>"]}. The judgment writes `judgment.json` into the run's results directory. It verifies that the evidence presented supports the claim, not that the evidence is true. The tool that executes llm_judge, and the gate's re-execution of lean and llm_judge, are not implemented yet. Also renders `claims.tex` — the numbered claim list with each criterion, prediction and (pending) verdict — into `.research/latex/{template}/` and commits it with the record; `\input{claims.tex}` where the paper lists its claims. The gate regenerates and diffs it at every stage. Fails if record.json already holds declarations (use `append_to_record`; the empty record a repository ships is initialised in place), if a claim declares no run, if a seyval claim lacks its criterion or prediction, or if the clone cannot commit. After this: write every future experimental number in main.tex as `\airasval{<run_id>.<metric>}` or `\airasval{<run_id>.params.<key>}`, compile, commit main.tex and push to the staging ref — tell the user the freeze sha once it lands.

Render a result chart whose data points come from measured metrics. Use this for publication-quality result figures. The Vega-Lite spec must not contain literal numbers in its data: write every numeric datum as `"metric:<run_id>.<path>"` (e.g. `"metric:run_1.accuracy"`), and the tool resolves it against `.research/results/` in `local_path` itself — so a plotted point cannot be a number no run measured. Categorical fields (method names, dataset labels) stay plain strings; `calculate`/`expr` transforms are rejected. `\unverified` has no chart equivalent: a number that no run produced does not belong in a result figure. Save charts as **PNG** under `.research/results/chart/` in the clone (`output_path` must lie under that directory and end with .png or .svg), then commit and push — the LaTeX build collects figure PDFs and PNGs under `.research/results/`. PDF chart output is refused: vl-convert's PDF bytes are not deterministic across processes, so a PDF chart could never be verified against a re-render. The unresolved spec is appended to `.research/record.json`, under the hypothesis named by `hypothesis_id`, as the chart's declaration, and the chart and record.json are committed together in the same step (`commit` in the result); `verify_paper_values` re-resolves, re-renders and byte-compares. A path that already has a different declared spec is refused — render to a new path, or supersede the old declaration via `append_to_record`. Rendering runs in-process (vl-convert); no data leaves the machine and no API keys are required.

Render a text diagram (diagram-as-code) to a file via Kroki. Use this for method/architecture diagrams: write the diagram source in a text notation (`diagram_type`: "mermaid", "graphviz", "d2", "plantuml", and 20+ more Kroki types). When rendering into a local clone of the experiment repository, save the result as a PDF under `.research/results/diagram/`, then commit and push — the LaTeX build collects every `*.pdf` under `.research/results/`. `output_path` must end with .pdf, .svg, or .png; PDF conversion happens locally from the SVG (vector). Types whose SVG embeds HTML labels (e.g. mermaid) fall back to a raster PDF automatically — prefer "graphviz" / "plantuml" when you want vector text. Rendering uses the public https://kroki.io by default — set KROKI_BASE_URL to a self-hosted instance to keep unpublished diagrams private. No API keys required.

List AIRAS's hand-curated candidate datasets for a subfield. Check here first. Subfields follow the shared domain>category taxonomy: language ("instruction_tuning", "reasoning_evaluation", "nlp_tasks", "prompt_engineering", "code_evaluation"), "image_recognition", "speech", "vision_language". Returns a dict keyed by dataset name; each value has description, task_type, huggingface_url, dependent_packages, a runnable code snippet, citation, and more. If none fit the experimental design, fall back to `search_huggingface_hub` (kind="datasets"), which returns the same shape from the live Hub. No API keys required.

List AIRAS's hand-curated candidate models for a subfield. Check here first. Subfields follow the shared domain>category taxonomy: language ("text_generation", "text_understanding", "sequence_to_sequence", "code_generation", "text_embedding", "reranking", "hosted_api"), vision ("image_recognition", "image_generation"), "vision_language", "speech", "forecasting", "protein". Returns a dict keyed by model name; each value has model_architecture, task_type, huggingface_url, dependent_packages, a runnable code snippet, citation, and more. If none of these fit the experimental design, fall back to `search_huggingface_hub` (kind="models"), which returns the same shape from the live Hub. No API keys required.

Live Hugging Face Hub fallback for `retrieve_models`/`retrieve_datasets`. Use this only when the curated tools (`retrieve_models` / `retrieve_datasets`) have no suitable candidate for the experimental design — check them first, then come here to go wider or find newer releases. Returns the same shape as the curated tools: a dict keyed by resource id, each value carrying the curated-compatible fields (description, task_type, huggingface_url, dependent_packages; code and citation are empty for Hub results — read the card at huggingface_url), plus discovery metadata (downloads, likes, tags, last_modified). `kind` is "models" or "datasets"; `query` is free-text search; `task` filters by pipeline tag for models (e.g. "text-generation", "image-classification", "automatic-speech-recognition") or by tag for datasets; `sort` ranks results ("downloads", "likes", "trendingScore", "lastModified"). HF_TOKEN is optional (only for gated resources).

Search academic papers across multiple sources in parallel. Sources: openalex, semantic_scholar, arxiv, airas_db (curated conference database: the major ML and NLP venues, plus the formal-methods and theorem-proving venues — ITP, CPP, CADE, IJCAR, CAV, TACAS, LICS, POPL — for theory claims), airas_records (the research AIRAS itself produced whose gate passed). Pass a comma-separated subset or "all". `year` filters by publication year ("2024" or "2020-2024"); it does not apply to airas_records. `airas_records` matches the query against what each study hypothesized and claimed — and the titles of the papers it built on, so a paper's title finds the studies that rest on it — not against paper prose. Each row's `abstract` lists the hypotheses and claims with their verdicts, and `external_ids.airas_record` is the id `preregister_record` takes. `verdict` keeps studies with a claim of that verdict (`refuted` finds what has already failed), `stage` keeps preregistered-only or realized studies; both apply to airas_records alone, so select only that source with them. `search_mode="keyword"` (default) does lexical/relevance search on every source. `search_mode="semantic"` does AI-embedding search that matches by meaning; it is only supported by `openalex` and requires OPENALEX_API_KEY (so pass sources="openalex"). Selecting any other source in semantic mode is an error. Results are normalized (title, authors, abstract, doi, arxiv_id, pdf_url, citations, source) and de-duplicated across sources; failures of individual sources are reported in `search_errors` without failing the search. Keyword search needs no API keys (SEMANTIC_SCHOLAR_API_KEY / OPENALEX_API_KEY optionally raise rate limits). Pass a promising row's arxiv_id / doi / pdf_url to `fetch_paper_fulltext`.

Copy locally configured API keys into the repository's Actions secrets. Run once right after `prepare_repository`, and again when a key is added or rotated. The record gate needs `SEYVAL_API_KEY` in the repository to re-fetch each run's stored outputs and compare them against what the repository holds; without it that check is skipped rather than failed, so CI looks green without having run it. Reads the values from this machine's environment and writes them encrypted; no value appears in the result. `secret_names` defaults to every key airas knows about, and a name with no local value is skipped rather than failing. Requires GH_PERSONAL_ACCESS_TOKEN with admin rights on the repository.

Realize the record from the run outputs and commit it. This is the only sanctioned way experimental numbers enter the paper. The declarations live in `.research/record.json`; this tool reads the actual run outputs in the local clone (`.research/results/<run_id>/` — metrics.json, eval_inputs/, evaluation/) and the provenance manifest `.provenance.json`, and appends to each run a `results[]` entry: the platform's execution id and commit, the hash of the evaluation inputs, the evaluator's report, and the metrics file verbatim. Numbers cannot be passed in, so a value that was never measured cannot enter the record. A lean run is read from `lean.json` and an llm_judge run from `judgment.json` in the same results directory. A claim's `verified` is set to true when every run under it has results — the data the claim rests on is in — and its `verdict` once the verifier concludes: for seyval, the declared criterion applied to the runs' metrics. Both are written once and never back; a re-run that would flip the verdict is reported by the gate as drift, and re-judging means appending the claim again under the same id. Whether the claim was declared before its runs executed is not modelled yet. It then renders `values.tex`, `tables/<key>.tex` and `claims.tex` into `.research/latex/{template}/`; when the clone has an `origin` remote, every value macro is a hyperlink to record.json at the commit that wrote it. This tool does not judge the result, and deliberately so. Whatever it reported locally, the agent could push regardless, so a local verdict was advice rather than a gate — and running the identical checks twice made the advisory pass look like a second, independent opinion. The verdict comes from CI, on the pushed commit, where the agent cannot intervene: push to the staging ref, read the run, and fast-forward the protected branch only when it is green. Then `\input{values.tex}` in main.tex's preamble, `\input{tables/<key>.tex}` where each table belongs, and every experimental number as `\airasval{key}` — never a literal. A legitimate number no declaration can produce (e.g. a value quoted from a cited paper) must be wrapped as `\unverified{...}` so it is surfaced for review.

Compile the paper locally and report whether it is actually sound. Use this before `open_in_overleaf` or a push — those produce a link and a dispatch receipt, neither of which tells you the document built. This one builds it and answers the questions that decide whether the paper is publishable: did a PDF come out (`compiled`, `page_count`), do any citations render as `?` (`undefined_citations` — the usual cause is writing main.tex without also writing the generated bibliography to `.research/latex/{template}/references.bib`, whose shipped version is a single placeholder entry), do any `\ref`s render as `??` (`undefined_references`), and is any figure referenced but absent (`missing_figures`). `ok` is true only when all of those are clean and `errors` — the `!` lines from the log, which is where a missing package or a broken environment shows up — is empty too. It compiles exactly the file set `open_in_overleaf` would export, so what is checked is what would be shipped. The toolchain is still the local one — Overleaf builds its own TeX Live image through latexmk — so read the two verdicts differently: `ok=False` is a property of the document and will follow it anywhere, while `ok=True` says this machine built it, not that Overleaf will. A package installed there but not here is the likely way the two disagree. Pass `local_path` — the absolute path of your local clone — to check the working tree with no push and no API keys. Otherwise pass `github_owner`/`repository_name`/`branch_name` to check what was pushed (requires GH_PERSONAL_ACCESS_TOKEN). Pass `output_path` to keep the PDF this build produced — the build directory is temporary otherwise, and `pdf_path` in the result says where it landed. A Japanese paper's PDF comes from here or from the Publish Paper workflow (lualatex on both). Requires a local TeX distribution. A Japanese document is built with lualatex (`texlive-luatex`, `texlive-lang-japanese`); everything else with pdflatex. When checking a local clone of a paper that uses the canonical-record system (a `.research/record.json` created by `preregister_record` exists), the record is verified too — the same checks as `verify_paper_values`: declarations, append-only history, value/ table/chart recomputation, claim flags, and (unless `check_provenance=False`) the Seyval provenance cross-check. The record's verification lands under `record` (every failure is a line in its `problems`) and the build under `build`. On failure `ok` is false and no PDF is written to `output_path` — so a PDF this tool hands out states verified, provenance-backed numbers.

Check that everything the paper states is what was declared and measured. Verifies the canonical record `.research/record.json` end to end. At the prereg stage (no run outputs yet) it checks the declarations' internal consistency, that nothing realized exists prematurely, and the append-only history. Once results exist, the deterministic checks that decide `ok`: every declared value is recomputed from the run outputs under `.research/results/` and compared to the record's stored results (a tampered record surfaces as a mismatch), `values.tex` and `claims.tex` are regenerated and diffed byte-for-byte (`claims.tex` at the prereg stage too), every `\airasval` key main.tex references must be declared, every table under `tables/` and every chart under `.research/results/chart/` must match a regeneration of its declaration (undeclared files fail), every results directory must belong to a declared run, the record's git history must be pure appends to the declaration section, and each claim's stored verified flag must be borne out by the recomputation: verified means every run under the claim has results. A claim that is merely not yet verified does not fail the check — only a stored flag the recomputation contradicts does. Unless `check_provenance=False`, the local metrics files are also cross-checked against the execution platform's stored run outputs (currently Seyval): each referenced results directory must be byte-identical to what the run *declared* for it in `.research/results/.provenance.json` (written by `import_run_outputs`) actually produced, that run must be completed, and its commit must be an ancestor of the local HEAD. Each check lists the other completed runs of the same commit (`sibling_run_ids`); review them — repeated executions mean the reported run was a choice. `provenance.status` "unavailable" is surfaced without failing the local checks. `unverified` lists every `\unverified{...}` the author marked — review input, not a failure. Run this after any step that may edit main.tex (including compile agents), and treat the list as mandatory review items before publishing. `unsupported_citations` is the same kind of item: what the judge did not find borne out by the passage. `unjudged_citations` — citations no judgment covers as the text now stands — fail the check. Pass `model` to have that model read each unjudged citation against its passage first; the judgments are written into the record and committed, so the same call then reports only what the model found unsupported. Re-run with `model` after rewriting a sentence that cites a passage. Requires an LLM provider key when `model` is given.