A3 Python

A3-Python Static Analysis Skill

A3 (Advanced Automated Analysis) combines non-LLM static analysis with optional agentic LLM triage to find real bugs in Python codebases with 99%+ accuracy.

When to Use This Skill

Use this skill when you need to:

• Analyze Python code for potential bugs, vulnerabilities, or runtime errors
• Perform static analysis on Python projects
• Set up continuous integration scanning for Python repositories
• Triage security findings with high accuracy
• Reduce false positives in static analysis results

Installation

Recommended: Container Image (via GitHub Container Registry)

Before using this skill, set up a3-python via the container image:

# Pull the latest image
docker pull ghcr.io/thehalleyyoung/a3-python:latest

# Create a convenient alias (add to ~/.bashrc or ~/.zshrc)
alias a3='docker run --rm -v "$(pwd):/workspace" -w /workspace ghcr.io/thehalleyyoung/a3-python:latest a3'

The alias allows you to use a3 commands naturally. All examples below assume this alias is set up.

For commands that need API keys (like triage), pass them as environment variables:

# Example with OpenAI key
docker run --rm -v "$(pwd):/workspace" -w /workspace \
  -e OPENAI_API_KEY="$OPENAI_API_KEY" \
  ghcr.io/thehalleyyoung/a3-python:latest a3 scan . --triage

Optional: Local Installation via PyPI

For local development or if you prefer native installation:

# Basic installation
pip install a3-python

# With CI features (GitHub Actions, LLM triage, SARIF output)
pip install a3-python[ci]

Requires Python ≥ 3.11.

Basic Usage

Note: All examples below assume you've set up the a3 alias as shown in the Installation section. If you haven't, prefix commands with the full docker run invocation.

Quick Scan

To scan a Python project:

a3 scan . --output-sarif results.sarif

This runs a 7-step pipeline including:

• Call graph construction
• Crash summary computation
• Guard detection
• Barrier-certificate proofs using Z3
• DSE (Dynamic Symbolic Execution) confirmation

Scan with Agentic Triage

For end-to-end analysis with LLM-based triage in a single command:

# With alias (use full docker command below for API key support)
a3 scan . --triage

# Or with full docker command, passing API keys with -e flags
docker run --rm -v "$(pwd):/workspace" -w /workspace \
  -e OPENAI_API_KEY="$OPENAI_API_KEY" \
  -e ANTHROPIC_API_KEY="$ANTHROPIC_API_KEY" \
  -e GITHUB_TOKEN="$GITHUB_TOKEN" \
  ghcr.io/thehalleyyoung/a3-python:latest a3 scan . --triage

This automatically:

1. Runs static analysis
2. Detects your API key (OPENAI_API_KEY, ANTHROPIC_API_KEY, or GITHUB_TOKEN)
3. Launches agentic triage where the LLM explores the codebase
4. Only reports confirmed true positives

You can specify the provider explicitly:

a3 scan . --triage openai --output-sarif results.sarif
a3 scan . --triage github  # uses GITHUB_TOKEN, free in CI
a3 scan . --triage anthropic  # uses ANTHROPIC_API_KEY

Advanced Scanning Options

Enable all features for comprehensive analysis:

a3 scan /path/to/project \
  --interprocedural \
  --dse-verify \
  --deduplicate \
  --min-confidence 0.3

Key flags:

• --interprocedural: Cross-function analysis with call graph
• --dse-verify: Verify bugs with Z3-backed symbolic execution
• --deduplicate: Remove duplicate findings
• --min-confidence: Set minimum confidence threshold (0.0-1.0)
• --no-kitchensink: Disable symbolic execution portfolio (not recommended)

CI Integration

Quick Setup for GitHub Actions

Add A3 scanning to any repository in 60 seconds using the container image:

cd your-repo/

# Using the a3 alias
a3 init . --copilot

# Or with full docker command
docker run --rm -v "$(pwd):/workspace" -w /workspace \
  ghcr.io/thehalleyyoung/a3-python:latest a3 init . --copilot

# Commit generated files
git add .github/ .a3.yml .a3-baseline.json
git commit -m "ci: add a3 static analysis"
git push

This creates:

• .github/workflows/a3-pr-scan.yml: Scans every push and PR with agentic triage
• .github/workflows/a3-scheduled-scan.yml: Weekly full-repo scan
• .a3.yml: Configuration file
• .a3-baseline.json: Baseline for tracking known issues

How CI Works

The generated workflows use the container image ghcr.io/thehalleyyoung/a3-python:latest to:

1. Non-LLM static analysis scans the repo and proves 99% of candidates as false positives
2. Agentic LLM triage investigates the remaining 1% by reading files, searching for guards, checking callers and tests
3. Baseline ratchet check blocks CI if new bugs are found
4. SARIF uploaded to GitHub Code Scanning dashboard

The workflow uses GITHUB_TOKEN (available in all GitHub Actions) to access GitHub Models for free LLM triage - no API key setup needed.

Configuration

Create a .a3.yml file in your repository root:

analysis:
  interprocedural: true
  dse-verify: true
  min-confidence: 0.3
  deduplicate: true

ci:
  fail-on-new-bugs: true
  baseline-file: .a3-baseline.json
  llm-triage: true
  llm-provider: github  # uses GITHUB_TOKEN - no extra API keys
  llm-model: gpt-4o
  sarif-upload: true

scan:
  exclude:
    - "tests/**"
    - "docs/**"
    - "**/test_*.py"

When this file is present, a3 scan reads it automatically.

Baseline Management

The baseline file tracks accepted findings for incremental adoption:

# Check for new findings (exits 1 if any are new)
a3 baseline diff --sarif results.sarif

# Accept current findings into baseline
a3 baseline accept --sarif results.sarif

This allows you to:

• Block CI on new bugs while ignoring legacy issues
• Track improvements as bugs are fixed
• Avoid being overwhelmed by existing issues in large codebases

Separate Scan and Triage

You can run scan and triage as separate steps:

# Step 1: Scan
a3 scan . --output-sarif results.sarif

# Step 2: Triage
a3 triage \
  --sarif results.sarif \
  --output-sarif triaged.sarif \
  --provider openai \
  --agentic \
  --verbose

Best Practices

1. Start with basic scan: Run a3 scan . to understand your codebase's issues
2. Use triage for accuracy: Add --triage to reduce false positives to near zero
3. Set up CI early: Use a3 init --copilot to catch bugs before they reach production
4. Leverage baselines: In large codebases, use baselines to adopt A3 incrementally
5. Configure exclusions: Exclude test files and vendored code in .a3.yml
6. Use SARIF output: Upload to GitHub Code Scanning for integrated security alerts

Output Formats

A3 supports multiple output formats:

• SARIF: Standard format for code scanning tools (--output-sarif results.sarif)
• Console: Human-readable output (default)
• JSON: Machine-readable format for custom processing

Example Workflow

Here's a typical workflow for analyzing a Python project:

1. Set up the container and alias:

   docker pull ghcr.io/thehalleyyoung/a3-python:latest
   alias a3='docker run --rm -v "$(pwd):/workspace" -w /workspace ghcr.io/thehalleyyoung/a3-python:latest a3'
   

2. Run initial scan with triage:

   # For triage with API keys, use the full docker run command with -e flags
   # (see the Container Image installation section for more details)
   docker run --rm -v "$(pwd):/workspace" -w /workspace \
     -e OPENAI_API_KEY="$OPENAI_API_KEY" \
     ghcr.io/thehalleyyoung/a3-python:latest a3 scan . --triage --output-sarif results.sarif
   

3. Review findings and fix confirmed bugs

4. Set up CI integration:

   a3 init . --copilot
   git add .github/ .a3.yml .a3-baseline.json
   git commit -m "ci: add a3 scanning"
   

5. Push and let CI protect your codebase going forward

Additional Resources

• Container Image: https://github.com/thehalleyyoung/a3-python/pkgs/container/a3-python
• PyPI package: https://pypi.org/project/a3-python/
• Documentation: Run a3 --help for command-line reference
• GitHub Actions integration is fully automated with a3 init --copilot

Notes

• A3 uses Z3 solver for symbolic execution and formal proofs
• The agentic triage feature requires an LLM API (OpenAI, Anthropic, or GitHub Models)
• GitHub Models via GITHUB_TOKEN is free in CI environments
• Results integrate with GitHub Security → Code Scanning dashboard
• Supports Python 3.11 and higher