### Install Speca CLI Source: https://speca.pages.dev/docs/guide/try-it Installs the Speca CLI globally. Use `npx` for individual commands if you prefer not to install globally. Run `speca doctor` to verify your environment setup. ```bash npm install -g speca-cli ``` ```bash speca doctor ``` -------------------------------- ### Install SPECA from Source Source: https://speca.pages.dev/docs/getting-started/installation Clone the repository, install Python dependencies using `uv`, build the CLI frontend, and then link the local build to your PATH or run it directly. ```bash git clone https://github.com/NyxFoundation/speca.git cd speca uv sync cd cli && npm install && npm run build && cd .. ``` ```bash npm link --prefix cli ``` ```bash node cli/dist/cli.js doctor ``` -------------------------------- ### Install SPECA CLI Globally Source: https://speca.pages.dev/docs/getting-started/installation Use this command for a one-time environment check or for persistent installation of the SPECA CLI. This makes the `speca` command available in your PATH. ```bash npx speca-cli@latest doctor ``` ```bash npm install -g speca-cli speca doctor ``` -------------------------------- ### Check SPECA Environment Source: https://speca.pages.dev/docs/getting-started/installation Run this command to verify your SPECA installation and environment setup. It checks Node.js, Python, CLI authentication, and MCP server status. ```bash speca doctor ``` -------------------------------- ### Proof Gap Example Source: https://speca.pages.dev/docs/concepts/proof-attempt This example illustrates a 'Proof Gap' identified during the auditing process. It specifies the exact location (line 85 in error_handler) and condition (if (!cache_hit)) where the property fails to hold, indicating a potential finding. ```text Claim: "authenticate() は sensitive_data() の前に呼ばれる" Gap at line 85 in error_handler(): if (!cache_hit) { sensitive_data(); // <-- authenticate() 呼ばれていない } ``` -------------------------------- ### Mermaid State Diagram Example Source: https://speca.pages.dev/docs/pipeline/01b-subgraph-extraction Illustrates a state diagram generated from specification sections, including states, transitions, and invariants noted within state boxes. ```mermaid stateDiagram-v2 [*] --> StateA StateA --> StateB: transition_label StateB --> [*] note right of StateA INV-001: Property X must hold INV-002: Invariant Y end note ``` -------------------------------- ### Example Browse Output Line Source: https://speca.pages.dev/docs/getting-started/quickstart A typical line from `speca browse` output, showing finding ID, severity, verdict, source location, proof gap, and gate status. ```text PROP-001 HIGH CONFIRMED_VULNERABILITY src/auth.rs:85 proof_gap: "Missing auth check in error_handler() — unreachable path skips verify_auth() before sensitive_data()" gates: dead_code=PASS · trust_boundary=PASS · scope=PASS ``` -------------------------------- ### Partial JSON Output Example Source: https://speca.pages.dev/docs/pipeline/01b-subgraph-extraction Represents a partial JSON output detailing extracted subgraph information, including specification section ID, text, states, transitions, invariants, and the associated Mermaid file. ```json { "spec_section_id": "FN-001", "spec_text": "...", "subgraph": { "states": ["state_a", "state_b"], "transitions": [{"from": "state_a", "to": "state_b", "label": "event"}], "invariants": ["INV-001", "INV-002"] }, "mermaid_file": "outputs/graphs/FN-001.mmd" } ``` -------------------------------- ### Example Output JSON for 3-Gate Review Source: https://speca.pages.dev/docs/pipeline/review This JSON structure represents the output of the 3-gate review process. It includes property and finding IDs, the final verdict, results from each gate, and the determined severity. Use this format to understand the outcome of the review. ```json { "property_id": "PROP-001", "finding_id": "FINDING-001", "verdict": "CONFIRMED_VULNERABILITY", "gate_results": [ {"gate": "dead_code", "passed": true}, {"gate": "trust_boundary", "passed": true}, {"gate": "scope_check", "passed": true} ], "severity": "HIGH" } ``` -------------------------------- ### Phase 01b: Subgraph Extraction Mermaid and JSON Source: https://speca.pages.dev/docs/concepts/worked-example This example shows the state transition graph extracted from a specification section and its JSON representation, including invariants. ```mermaid stateDiagram-v2 [*] --> BlockReceived BlockReceived --> SignatureVerified: verify_block_sig() SignatureVerified --> StateApplied: apply_block() StateApplied --> [*] note right of BlockReceived INV-001: signature MUST be verified before state application end note ``` ```json { "spec_section_id": "FN-042", "spec_text": "MUST verify the validator's signature on every block before applying it to the local state.", "subgraph": { "states": ["BlockReceived", "SignatureVerified", "StateApplied"], "transitions": [ {"from": "BlockReceived", "to": "SignatureVerified", "label": "verify_block_sig()"}, {"from": "SignatureVerified", "to": "StateApplied", "label": "apply_block()"} ], "invariants": ["INV-001"] }, "mermaid_file": "outputs/graphs/FN-042.mmd" } ``` -------------------------------- ### Audit Output Example Source: https://speca.pages.dev/docs/pipeline/audit-map This JSON structure represents the output of the audit process, detailing a specific property's ID, the verdict (FINDING, NO_FINDING, or UNCERTAIN), and the specifics of the proof attempt, including the claim, evidence, confidence level, and the identified proof gap. ```json { "property_id": "PROP-001", "verdict": "FINDING", "proof_attempt": { "claim": "verify_auth() is always called before resource access", "evidence": "Code path exists where resource access occurs at line 85 without prior verify_auth() call", "confidence": "HIGH", "proof_gap": "Missing auth check in error handler at line 85" } } ``` -------------------------------- ### Initialize Project with `speca init` Source: https://speca.pages.dev/docs/getting-started/cli-reference Generate `outputs/TARGET_INFO.json` and `outputs/BUG_BOUNTY_SCOPE.json` files required for the pipeline. All flags are optional and will prompt for input if not provided. Use `--non-interactive` to provide all values via flags. ```bash speca init ``` -------------------------------- ### CLI を更新する Source: https://speca.pages.dev/docs/guide/faq CLI を最新バージョンに更新し、正常に動作するか確認します。 ```bash npm update -g speca-cli ``` ```bash speca doctor ``` -------------------------------- ### Generate Configuration File Source: https://speca.pages.dev/docs/guide/try-it Creates configuration files (`outputs/TARGET_INFO.json` and `outputs/BUG_BOUNTY_SCOPE.json`) by prompting for repository URL, language, layers, and scope. Manual configuration is also possible. ```bash speca init ``` -------------------------------- ### Sharing Rubrics Across Implementations Source: https://speca.pages.dev/docs/getting-started/config-files Example of sharing scope descriptions across multiple implementations using a `common_rubric` block. ```json { "program_name": "kzg-batch-verify-v2", "common_rubric": { "in_scope": [ "KZG parameter generation (setup)", "Commitment creation", "Batch verification (main algorithm)", "Polynomial operations" ], "out_of_scope": [ "Serialization / deserialization", "Performance optimizations", "Logging / debugging" ] } } ``` -------------------------------- ### Recommended Reading Order for Harness Extension Source: https://speca.pages.dev/docs/agent-design/harness Suggests a reading order for understanding and extending the Harness codebase, highlighting key modules and their dependencies. ```markdown If you plan to extend the Harness, we recommend reading in this order: `config.py` (declarative), `base.py` (orchestration), `runner.py` (process management), and `watchdog.py` (cost + log stream). Dependencies are intentionally shallow, and each module is under 600 LOC. ``` -------------------------------- ### Traditional LLM Prompt Source: https://speca.pages.dev/docs/concepts/proof-attempt This is an example of a vague prompt used with traditional LLM-based tools, which often leads to speculative and poorly-founded results. ```text "このコードにバグがないか調べてください" ``` -------------------------------- ### Directly Publish Benchmark Artifacts Locally Source: https://speca.pages.dev/docs/operations/release-artifacts When data is available on a self-hosted runner, use this command to first generate the tarball and manifest, and then create a GitHub release with these artifacts. This is an alternative to using the GitHub Action. ```bash bash benchmarks/scripts/publish-results.sh \ benchmarks/results/rq2a/speca_sonnet4 \ bench-rq2a-20260508-sonnet4 gh release create bench-rq2a-20260508-sonnet4 \ --title bench-rq2a-20260508-sonnet4 \ --prerelease \ --notes "Local publish from $(git rev-parse --short HEAD)" \ dist/bench-artifacts/bench-rq2a-20260508-sonnet4.tar.zst \ dist/bench-artifacts/bench-rq2a-20260508-sonnet4.manifest.json ``` -------------------------------- ### Generate Configuration File Source: https://speca.pages.dev/docs/getting-started/quickstart Initialize Speca by generating configuration files. This interactive process prompts for repository URL, commit/tag, target language, layer, and rubric scope. Alternatively, use the non-interactive command with flags. ```bash speca init ``` ```bash speca init \ --target-repo https://github.com/sigp/lighthouse \ --target-commit v5.1.3 \ --target-language Rust \ --target-layer consensus \ --rubric default \ --non-interactive ``` -------------------------------- ### Sign in to Claude Source: https://speca.pages.dev/docs/getting-started/quickstart Log in to Claude once to set up authentication. You can save your API key or use an existing `claude` session. Check authentication status with `speca auth status`. ```bash speca auth login ``` -------------------------------- ### Apply SPECA to a New C/C++ Project Source: https://speca.pages.dev/docs/operations/benchmark-rq2a Adapt the SPECA benchmark harness for new C/C++ projects. This involves creating target information and scope definition files, running the SPECA audit, and preparing baseline data for visualization. ```bash # 1. Create outputs/TARGET_INFO.json for the target codebase (target_repo + target_commit) # 2. Define scope in outputs/BUG_BOUNTY_SCOPE.json (target modules / exclude paths) # 3. Run SPECA with scripts/run_phase.py --target 04 # 4. Prepare comparison data in the format of benchmarks/rq2a/published_baselines.yaml for existing visualization scripts. ``` -------------------------------- ### Configure Bug Bounty Scope Source: https://speca.pages.dev/docs/tutorial/audit-walkthrough Define the scope of the audit, including in-scope files, out-of-scope directories, and severity classifications with associated CWEs and examples. This helps tailor the audit process. ```json { "program_name": "openzeppelin-ownable-walkthrough", "scope_version": "1.0", "in_scope": ["contracts/access/Ownable.sol"], "out_of_scope": ["test/", "scripts/"], "severity_classification": { "HIGH": { "description": "Unauthorized owner change", "cwe": ["CWE-862", "CWE-863"], "examples": ["Bypass of onlyOwner"] }, "MEDIUM": { "description": "Two-step transfer divergence from spec", "cwe": ["CWE-841"], "examples": ["Pending owner not cleared"] }, "LOW": { "description": "Quality / informational", "cwe": ["CWE-710"], "examples": ["Misleading event"] } }, "scope_notes": "Walkthrough — single contract." } ``` -------------------------------- ### Generate Security Property JSON Source: https://speca.pages.dev/docs/pipeline/01e-property-generation Example of a generated security property in JSON format. This includes property details, classification, related CWEs, and reachability information based on bug bounty scope. ```json { "property_id": "PROP-001", "type": "Invariant", "description": "Authentication state must be verified before accessing protected resources", "covers": "FN-001", "classification": "STRIDE_ElevationOfPrivilege", "cwe_related": ["CWE-862"], "reachability": { "classification": "PUBLIC_API", "entry_points": ["authenticate()", "verify_token()"], "attacker_controlled": ["user_input", "token"], "bug_bounty_scope": "in_scope" } } ``` -------------------------------- ### Run Orchestrator Source: https://speca.pages.dev/docs/agent-design/harness Initiates the orchestrator for a specific target. ```bash speca run --target 04 ``` -------------------------------- ### 実行中のワークフローを監視 Source: https://speca.pages.dev/docs/operations/dataset-refresh dispatch したワークフローの実行状況を監視するためのコマンドです。run ID を指定して詳細を確認できます。 ```bash gh run watch -R NyxFoundation/speca ``` -------------------------------- ### Publish Benchmark Artifacts via GitHub Action Source: https://speca.pages.dev/docs/operations/release-artifacts Trigger the 'Publish benchmark artifacts' GitHub Action workflow to create a new release. Specify the subdirectory containing the results to be published. ```bash gh workflow run publish-bench-artifacts.yml -R NyxFoundation/speca \ --ref main \ -f subdir=rq2a/speca_sonnet4 ``` -------------------------------- ### GitHub Actions Workflow の Dispatch Source: https://speca.pages.dev/docs/operations/dataset-refresh GitHub UI または gh CLI を使用して、データセット公開ワークフローをトリガーします。`domain` と `dry_run` パラメータを指定します。 ```bash gh workflow run datasets-publish.yml -R NyxFoundation/speca \ --ref main \ -f domain=defi \ -f dry_run=false ``` -------------------------------- ### Generate Baseline Figures Source: https://speca.pages.dev/docs/operations/benchmark-rq2b Run this command to generate baseline figures for the ProFuzzBench dataset. The output includes PNG images and a LaTeX table. ```bash uv run python3 benchmarks/rq2b/visualize.py ``` -------------------------------- ### List Benchmark Releases Source: https://speca.pages.dev/docs/operations/release-artifacts Use this command to list all GitHub releases for the speca repository that match the benchmark tag naming convention. ```bash gh release list --repo NyxFoundation/speca | grep '^bench-' ``` -------------------------------- ### Cost Management with Budget Source: https://speca.pages.dev/docs/agent-design/harness Tracks token consumption per batch and accumulates USD costs per phase, with an option to set a budget that triggers an exit on exceeding the limit. ```markdown CostTracker tracks token consumption from each batch's stream-json output and accumulates USD per phase. The pricing model is keyed by the models used in that phase. If `--budget ` is specified, it throws BudgetExceeded when the total exceeds the limit, which is converted to exit code **64** on the runner side. ``` -------------------------------- ### Benchmark Artifact Distribution Workflow Source: https://speca.pages.dev/docs/operations/overview This diagram outlines the workflow for distributing benchmark artifacts. It covers bundling results into a GitHub Release and restoring them. ```text benchmarks/results/// (eval pipeline 出力) ↓ Publish benchmark artifacts (workflow_dispatch) ↓ GitHub Release `bench---` ↓ restore-results.sh で再展開 ``` -------------------------------- ### Run Pipeline with `speca run` Source: https://speca.pages.dev/docs/getting-started/cli-reference Execute the pipeline, which typically displays a TUI dashboard. Use flags like `--phase` to specify stages, `--target` to run up to a certain dependency, or `--force` to ignore resume states. For CI environments, use `--no-tui` or `--json` for plain text or NDJSON output. ```bash speca run --target 04 --workers 4 ``` ```bash speca run --phase 01a 01b 01e ``` ```bash speca run --phase 03 --force --json ``` -------------------------------- ### コスト上限を設定する Source: https://speca.pages.dev/docs/guide/faq 監査の最大予算を設定し、指定した金額を超えた場合に実行を停止します。 ```bash speca run --target 04 --budget 50 ``` -------------------------------- ### Restore Benchmark Results Source: https://speca.pages.dev/docs/operations/benchmark-rq2a Use these commands to restore the necessary result files from release tags before running visualization or evaluation scripts. Replace `` with the actual date found using the provided command. ```bash bash benchmarks/scripts/restore-results.sh bench-rq2a--speca bash benchmarks/scripts/restore-results.sh bench-rq2a--sonnet4 bash benchmarks/scripts/restore-results.sh bench-rq2a--deepseek_r1 bash benchmarks/scripts/restore-results.sh bench-rq2a--figures ``` -------------------------------- ### スクレイピングスクリプトの実行 Source: https://speca.pages.dev/docs/operations/dataset-refresh ローカル環境で Code4rena, Sherlock, CodeHawks からデータをスクレイピングするためのコマンドです。GitHub CLI での認証が必要です。 ```bash cd speca uv run python3 scripts/scrape_code4rena.py uv run python3 scripts/scrape_sherlock.py uv run python3 scripts/scrape_codehawks.py ``` -------------------------------- ### Download and Restore Benchmark Artifacts Source: https://speca.pages.dev/docs/operations/release-artifacts This command downloads a specific benchmark release tarball and restores its contents to the original location using the provided script. The script verifies the archive using a manifest and expands files in-place. ```bash bash benchmarks/scripts/restore-results.sh bench-rq2a-20260508-sonnet4 ``` -------------------------------- ### Resume Functionality Source: https://speca.pages.dev/docs/agent-design/harness Saves tokens by scanning for previously processed item IDs in partial files, allowing execution to resume from where it left off. ```markdown Before phase execution: 1. `ResumeManager` reads all `outputs/_PARTIAL_*.json`. 2. Creates a set of `item_id`s that have already produced results. 3. The batch builder excludes those IDs from the queue. ``` -------------------------------- ### SPECA Pipeline Dependency Graph Source: https://speca.pages.dev/docs/pipeline/overview Illustrates the sequential dependencies between the six stages of the SPECA pipeline. Phases 1-3 are reusable across implementations, while phases 4-6 are implementation-specific. ```text 01a (Spec Discovery) ↓ 01b (Subgraph Extraction) ↓ 01e (Property Generation) ← BUG_BOUNTY_SCOPE.json 必須 ↓ 02c (Code Pre-resolution) ← TARGET_INFO.json 必須 ↓ 03 (Audit Map: Map → Prove → Stress-Test) ↓ 04 (Review: Dead Code → Trust Boundary → Scope) ``` -------------------------------- ### Regenerate Figures from Existing SPECA Output Source: https://speca.pages.dev/docs/operations/benchmark-rq2a Run these commands to regenerate comparison figures and tables using the `visualize.py` script. This process does not incur API costs. Ensure results are restored beforehand. ```bash # Baseline only uv run python3 benchmarks/rq2a/visualize.py # Overlay Sonnet 4.5 (assuming speca/ is restored) uv run python3 benchmarks/rq2a/visualize.py \ --speca-results benchmarks/results/rq2a/speca/speca_summary.json # Inter-model comparison (for symmetric-comparison + adherence plots) uv run python3 benchmarks/rq2a/visualize.py \ --speca-multi \ "Sonnet 4.5=benchmarks/results/rq2a/speca/speca_summary.json" \ "Sonnet 4=benchmarks/results/rq2a/speca_sonnet4/speca_summary.json" \ "DeepSeek R1=benchmarks/results/rq2a/speca_deepseek_r1/speca_summary.json" ``` -------------------------------- ### Run SPECA End-to-End on 15 Projects Source: https://speca.pages.dev/docs/operations/benchmark-rq2a Execute these commands to perform the full SPECA audit across the 15 RepoAudit projects. This involves setting up the dataset, running the audit for different models, and then evaluating the results. ```bash # 1. Clone RepoAudit dataset into target_workspace/ gh workflow run rq2a-01-setup-dataset.yml # 2. Run SPECA (workflows are separated by model) gh workflow run rq2a-03-audit-map-sonnet4.yml -f projects=all gh workflow run rq2a-03-audit-map-deepseek-r1.yml -f projects=all # 3. Evaluate + Visualize gh workflow run rq2a-04-evaluate-sonnet4.yml -f projects=all ``` -------------------------------- ### Interact with Claude Code via `speca ask` Source: https://speca.pages.dev/docs/getting-started/cli-reference Open a Claude Code session pre-loaded with the context of a specific finding. This is useful for asking questions about the finding's details, requesting patches, or determining if it's a false positive. You can select a finding interactively, specify a file, or resume an existing session. ```bash speca ask # 最初の finding を対話的に選択 ``` ```bash speca ask PROP-abc-001 --from outputs/04_PARTIAL_*.json ``` ```bash speca ask --session 9f1c2e0a-... # 既存セッションを再開 ``` ```bash speca ask --no-tui --from finding.json --max-context 10000 ``` -------------------------------- ### Dataset Update Workflow Source: https://speca.pages.dev/docs/operations/overview This diagram illustrates the process for updating the dataset. It involves scraping data, converting it to CSV, and publishing it to HuggingFace. ```text scrape_*.py (手元で実行) ↓ benchmarks/data/defi_audit_reports/*.csv ↓ Publish dataset to HuggingFace (workflow_dispatch) ↓ https://huggingface.co/datasets/NyxFoundation/vulnerability-reports ``` -------------------------------- ### Run Audit with `speca run` Source: https://speca.pages.dev/docs/tutorial/audit-walkthrough Execute the audit process using the `speca run` command with specified targets and worker count. This command initiates the analysis and displays progress. ```bash speca run --target 04 --workers 4 ``` ```json {"phase":"01a","status":"running","found":3} {"phase":"01b","status":"running","subgraph":"Ownable-ownership-transfer"} {"phase":"01e","status":"running","property":"PROP-001", "description":"onlyOwner is applied to all administrative functions"} {"phase":"02c","status":"running","resolved":5} {"phase":"03","status":"running","property":"PROP-001","result":"gap_found"} {"phase":"04","status":"running","verdict":"CONFIRMED_POTENTIAL"} ``` -------------------------------- ### Manage Claude API Authentication with `speca auth` Source: https://speca.pages.dev/docs/getting-started/cli-reference Manage your Claude API credentials using `speca auth login` for interactive login or `speca auth status` to view the current authentication source. Authentication is saved to `~/.config/speca/auth.json` or can be set via the `ANTHROPIC_API_KEY` environment variable. ```bash speca auth login # 対話式: API キー or claude セッション ``` ```bash speca auth status # 現在の認証ソースを表示 ``` -------------------------------- ### Check Environment with `speca doctor` Source: https://speca.pages.dev/docs/tutorial/audit-walkthrough Run this command to verify that your environment meets the necessary requirements for using the Speca CLI. Ensure all checks show '[ok]'. ```bash speca doctor ``` ```text [ok] Node.js 20.x [ok] Python 3.11 (uv) [ok] Claude Code CLI authenticated [ok] MCP servers: fetch, tree_sitter ```