# A3 Python

> Advanced Automated Analysis for Python - Find real bugs in Python codebases using static analysis with Z3-backed symbolic execution and optional agentic LLM triage. Use this skill when analyzing Python code for security vulnerabilities, runtime errors, or code quality issues.

- Skill: `z3prover/a3-python` (Agent Skill, multi-file: 5 files)
- Install (CLI): `npx skillmds@latest add z3prover/a3-python`
- Raw SKILL.md: https://api.skillmd.com/api/skills/z3prover/a3-python/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: AI & ML
- Author: Z3Prover (https://skillmd.com/u/z3prover)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/z3prover/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:

```bash
# 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:

```bash
# 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:

```bash
# 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:

```bash
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:

```bash
# 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:

```bash
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:

```bash
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:

```bash
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:

```yaml
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:

```bash
# 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:

```bash
# 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:
   ```bash
   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:
   ```bash
   # 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:
   ```bash
   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