speca CLAUDE.md

CLAUDE.md

This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository.

Project Overview

SPECA (Specification-to-Property Agentic Auditing) — an automated security audit pipeline that uses Claude Code CLI to analyze codebases for vulnerabilities. The pipeline transforms specifications into formal program graphs, generates security properties, pre-resolves code locations, performs proof-based formal audits against target code, and filters false positives via a recall-safe 3-gate review pipeline (Dead Code, Trust Boundary, Scope Check).

Commands

# Run tests (pre-flight check used in all CI workflows)
uv run python3 -m pytest tests/ -v --tb=short

# Run a single phase
uv run python3 scripts/run_phase.py --phase 01a

# Run multiple phases sequentially
uv run python3 scripts/run_phase.py --phase 01a 01b 01e

# Run all phases up to a target (resolves dependency chain)
uv run python3 scripts/run_phase.py --target 04 --workers 4

# Force re-execution (clears resume state)
uv run python3 scripts/run_phase.py --phase 03 --force --workers 4 --max-concurrent 64

# Dry-run cleanup check
uv run python3 scripts/run_phase.py --phase 03 --cleanup-dry-run

# Register MCP servers
bash scripts/setup_mcp.sh
bash scripts/setup_mcp.sh --verify

Architecture

Orchestrator (scripts/orchestrator/)

The async Python orchestrator manages the full lifecycle of each phase:

1. config.py — PhaseConfig Pydantic models define each phase (prompt path, queue/output patterns, batch strategy, circuit breaker thresholds, cost limits, MCP servers, tool filters). All phases live in PHASE_CONFIGS dict.
2. base.py — BaseOrchestrator loads inputs, validates with Pydantic schemas, filters already-processed items (resume), enriches with context, creates batches, executes in parallel via asyncio. Subclasses: Phase01Orchestrator, Phase02cOrchestrator, Phase03Orchestrator, Phase04Orchestrator, Phase05Orchestrator.
3. runner.py — ClaudeRunner invokes claude CLI per batch with --prompt-path, --stream-json. Includes CircuitBreaker (consecutive failures, total retries, empty results) and retry with exponential backoff (max 3).
4. watchdog.py — LogWatcher tails stream-json logs in real-time via async task; CostTracker enforces per-phase budget (hard stop on BudgetExceeded).
5. resume.py — ResumeManager scans PARTIAL_*.json outputs, extracts processed IDs, enables incremental execution.
6. collector.py — ResultCollector saves partial results immediately after each batch. Validation is lenient (warns but doesn't block) to preserve partial progress. Applies output_fields filtering to keep PARTIALs compact.
7. schemas.py — Pydantic models for all inter-phase data contracts. Cross-phase validation at boundaries (01a→01b→01e→02c→03→04).