SPECA

https://speca.pages.dev/docs/
Admin
SPECA is an automated security auditing framework that derives security properties from...
Tokens:28,105
Snippets:311
Trust Score:7.2
Update:5 months ago
Show doc for...
Tokens:
Raw
### 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 <run-id> -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 <usd>` 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/<rq>/<run>/  (eval pipeline 出力)  

        ↓  

  Publish benchmark artifacts (workflow_dispatch)  

        ↓  

  GitHub Release `bench-<rq>-<date>-<suffix>`  

        ↓  

  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 `<date>` with the actual date found using the provided command.

```bash
bash benchmarks/scripts/restore-results.sh bench-rq2a-<date>-speca
bash benchmarks/scripts/restore-results.sh bench-rq2a-<date>-sonnet4
bash benchmarks/scripts/restore-results.sh bench-rq2a-<date>-deepseek_r1
bash benchmarks/scripts/restore-results.sh bench-rq2a-<date>-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/<phase>_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  
```
Tokens:
Raw