Codex, Plugin
Rigorous Open Math Research
Codex skills for rigorous open mathematics research, research-program management, and Lean 4 formal verification (rigorous-open-math-research + manage-math-research-program + lean-verify plugin + math-research-workflow pipeline).
Compatibility: Not stated.
Grade C
One Medium finding. Read the findings before installing.
Not a guarantee. A hygiene check of the source at the commit shown, not a security audit.
Rescanned at commit af360f8f1fdf, unchanged since the check below.
PERMISSION_SHELL_UNDECLARED
Why this grade
- PERMISSION_SHELL_UNDECLARED Medium
Runs shell commands that the manifest or description does not mention.
plugins/lean-verify/scripts/lean_develop.py, line 165
Process = subprocess.Popen(Command, cwd=Root, stdout=subprocess.PIPE, stderr=subprocess.PIPE, **background_options())
Any High, or two or more Medium findings, give D. One Medium gives C. Low findings or a security Note give B. Each code names a finding behind the letter.
Grades are a hygiene check of the source at the commit shown, on the date checked, not a security audit or a guarantee. The free directory grades are automated. Before release, a PlugVet engineer reviews every paid report and any grade we hold back, including all F grades, against the source code and the evidence we quote.
What was checked
Plain notes from the hygiene checks.
Permissions
Concern
requests shell access. No manifest field names shell or command execution.
PERMISSION_SHELL_UNDECLARED
plugins/lean-verify/scripts/lean_develop.py, line 165
Process = subprocess.Popen(Command, cwd=Root, stdout=subprocess.PIPE, stderr=subprocess.PIPE, **background_options())
plugins/lean-verify/scripts/lean_feedback.py, line 46
self.Process = subprocess.Popen(Runtime.Command + ["--server"], cwd=Runtime.Root, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=self.ErrorLog, env=Runtime.command_env(), **
plugins/lean-verify/scripts/lean_runtime.py, line 110
Result = subprocess.run(["wslpath", "-w", str(PathName)], capture_output=True, text=True, timeout=10)
Show more
plugins/lean-verify/scripts/lean_runtime.py, line 272
Process = subprocess.Popen(Command, cwd=str(Cwd), stdout=Output, stderr=Error, stdin=subprocess.PIPE if InputText is not None else subprocess.DEVNULL, env=Env, start_new_session=os
plugins/lean-verify/scripts/lean_runtime.py, line 286
subprocess.run(["taskkill", "/PID", str(Process.pid), "/T", "/F"], capture_output=True, timeout=10, **background_options())
plugins/manage-math-research-program/runtime/blueprintctl.py, line 471
completed = subprocess.run(command, cwd=cwd, capture_output=True, text=True, encoding="utf-8",
plugins/manage-math-research-program/skills/manage-math-research-program/assets/blueprint-accepted-knowledge/tools/receive_blueprint.py, line 902
completed = subprocess.run(
plugins/manage-math-research-program/skills/manage-math-research-program/scripts/research_context.py, line 185
Process = subprocess.run(Command, capture_output=True, text=True, encoding="utf-8", timeout=240, creationflags=subprocess.CREATE_NO_WINDOW if os.name == "nt" else 0)
Install and update
Pass
No install-time script found, and dependencies are pinned or absent.
Network
Concern
can reach a host that is not written as a fixed address.
NETWORK_NO_FIXED_HOST
plugins/manage-math-research-program/skills/manage-math-research-program/assets/blueprint-accepted-knowledge/viewer/blueprint-viewer.js, line 1102
const response = await fetch("../blueprint.json", { cache: "no-store" });
scripts/benchmark_codex.py, line 258
with socket.create_connection(Endpoint, timeout=3):
scripts/benchmark_codex.py, line 287
socket.create_connection(""" + repr(Endpoint) + """, timeout=2).close()
Show more
scripts/benchmark_proxy_bridge.py, line 21
with socket.create_connection(("127.0.0.1", 7897), timeout=10) as Upstream:
Secrets
Pass
No read of a credential file or secret environment variable found.
Agent instructions
Pass
No instruction to ignore earlier instructions or to hide a step.
Obfuscation
Note
a file was over the read cap and was not fully read. the file cap was reached before every file was read.
OBFUSCATION_FILE_OVER_READ_CAP OBFUSCATION_FILE_CAP_REACHED
benchmarks/codex-20260908-q9/evidence/invalid-initial-A/artifacts/runs/rigorous-open-math-research/q9/branches_scan.json, line 1
{
benchmarks/codex-20260908-q9/evidence/q9-A-solver/artifacts/runs/q9/counterexample_log.md, line 1
# Counterexample record
Licence
Pass
A licence file is present (LICENSE).
Maintainer activity
Pass
The latest commit is within the last 365 days.
Note
Hygiene check of commit af360f8f1fdf. requests shell access. No manifest field names shell or command execution. can reach a host that is not written as a fixed address. a file was over the read cap and was not fully read. the file cap was reached before every file was read.
Date and source
Date checked:
github.com
Commit graded: af360f8f1fdf2df60c8c0f18d84d4e3740a13776
This link goes to the original host. PlugVet does not host or check what you download from there, and installing it is your own decision and risk.