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.
معلومات المصدر
- المستودع
- Z3Prover/a3-python-skill
- آخر نشاط في المصدر
- ١٨ فبراير ٢٠٢٦ في ٢٢:٥٢
- لغة SKILL.md المكتشفة
- الإنجليزية
- النجوم
- ١
- التفرعات
- ٠
خيارات التثبيت
يُحدَّد Prompt الذي يراجع المصدر أولًا بشكل افتراضي. يمكنك التبديل إلى أمر مباشر أو تنزيل نسخة محلية.
مراجعة ملفات المصدر
اقرأ SKILL.md وأي ملفات مرافقة يعرضها SkillsMP قبل أن تقرر التثبيت.
عرض SKILL.md
SKILL.md
تعليمات المصدر · معاينة للقراءة فقط- 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
عرض على GitHub