- name
- a3-python
- description
- 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.
# 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
View on GitHub