[
https://issues.apache.org/jira/browse/HDDS-16570?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18133310#comment-18133310
]
Ivan Andika edited comment on HDDS-16570 at 10/28/26, 1:17 AM:
---------------------------------------------------------------
Thanks [~smeng] for checking this.
I tried to run this with Codex GPT 6.1 Sol, but it kept getting flagged for
security and terminated early.
Please feel free to take this. Thanks for the help.
was (Author: JIRAUSER298977):
Thanks [~smeng] for checking this.
I tried to run this with Codex GPT 6.1, but it kept getting flagged for
security and terminated early.
Please feel free to take this. Thanks for the help.
> [Specula] Verify scm-node-health (Apache Ozone master @20e6a1c)
> ---------------------------------------------------------------
>
> Key: HDDS-16570
> URL: https://issues.apache.org/jira/browse/HDDS-16570
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: scm-node-health.guidance.md
>
>
> This is a runnable Apache Ozone formal-verification target for the Specula
> pipeline (TLA+ model checking plus trace validation against the real code).
> It has not been run yet. Anyone can pick it up: run Specula against the
> pinned commit, then report findings on this issue. Part of umbrella
> HDDS-15926.
> h3. Target
> {{scm-node-health}}. Scope and code entry points are in the attached guidance
> file [^scm-node-health.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: 20e6a1c0f6039248373efd3eb1d7f2afcf7f1535
> Specula: https://github.com/specula-org/Specula (v1.1.0 or later)
> Toolchain: JDK 21, ~28 GB RAM for TLC, an LLM coding agent
> (claude-code or codex adapter)
> Runtime: hours per target; needs an agent API budget
> {noformat}
> h3. How to run
> # Clone Specula and install per its README; clone apache/ozone and check out
> the pinned commit above.
> # Place the attached guidance file as the target's .prompt-extra.md (see the
> Specula README for target layout).
> # Run:
> {code:none}
> specula run --agent=claude-code --effort=medium --keep-original
> --max-parallel=2 \
> --enable-reviews --confirm-debate --tlc-memory-limit=28G
> --tlc-worker-limit=8 \
> "scm-node-health|apache/ozone|Java|Use the target-specific .prompt-extra.md"
> {code}
> # Deliverables land under the run's {{.specula-output/}}:
> {{confirmed-bugs.md}}, {{bug-severity.md}}, {{summary.md}}, and
> {{confirmation/<id>/investigation.md}}.
> h3. Reporting results
> Comment here with the outcome (0 findings is still useful: it records the
> target as covered at this commit). For each confirmed bug, file a separate
> Ozone Bug and link it to this issue with the "Testing" link type ("Testing
> discovered").
> h3. Notes
> * Code entry-point line numbers in the guidance were captured at an earlier
> commit and may have shifted on this head; treat them as approximate. Specula
> re-analyzes the source, so the run does not depend on them.
> * Recon-building targets need a local Specula patch to skip Maven {{target/}}
> out-of-tree symlinks in {{snapshotlib._validate_source_tree}}, else the run
> crashes at finalize.
> * effort=medium is the tested default for large targets; effort=high can hit
> per-turn timeouts on the biggest ones.
> * Findings are proposals, to be confirmed by human review and testing before
> any fix is merged.
--
This message was sent by Atlassian Jira
(v10.3.26#10030026)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
