Locate test-suite blind spots in one Python, TypeScript, JavaScript, Java, Rust, or Go module and its test file. Umbra deterministically finds unexercised branches, untested input regions, unasserted return contracts, and unasserted exception paths, then reports coverage beside a transparent Silence index. It can return isolated proof requests or generate and execute failing-test proofs; the execution gate keeps only runnable tests that genuinely fail or make the audited function error. The result identifies two local report artifacts: a plain portable Markdown report and a rich, shareable, self-contained HTML visual. After it returns, write and verify a failing-test proof for each returned request, then generate both reports with module_path and tests_path only: the server includes only proofs its gate retained. Umbra proves gaps and never edits the test file. The optional OpenAI backend reads only a locally configured key after explicit confirmation; never pass a key as tool input.

Run one user-approved Codex proposal through Umbra's execution gate. Use proof_index from umbra_audit's structured proof_requests. Umbra retains only a runnable test that genuinely fails or makes the audited function error. It rejects malformed concrete_input or expected_property fields with a correction reason so Codex can resubmit. A passing proposal is discarded. Re-run umbra_audit after an approved test write to measure the updated suite.

After the proof loop, write both Umbra report artifacts locally with module_path and tests_path only. The persistent server automatically includes only proofs retained by umbra_verify_proposal for that same pair. retained_proofs remains an optional explicit override for compatible callers. This deterministic action re-audits locally, sends no data to any API, and does not run proof generation.

Return Umbra's authoritative fixed definition for one precise, non-standard Umbra term, or list all defined terms with short glosses. Use this whenever a user asks what an Umbra term means. Unknown terms are identified plainly and never guessed. This deterministic local tool makes no model call and sends no data anywhere.