Skip to main content

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.

Quellinformationen

Repository
Z3Prover/a3-python-skill
Letzte Quellaktivität
18. Februar 2026 um 22:52
Erkannte Sprache von SKILL.md
Englisch
Sterne
1
Forks
0

Installationsoptionen

Standardmäßig ist der Prompt ausgewählt, der zuerst die Quelle prüft. Sie können zu einem direkten Befehl wechseln oder eine lokale Kopie herunterladen.

Quelldateien prüfen

Lesen Sie SKILL.md und alle von SkillsMP angezeigten Begleitdateien, bevor Sie sich für eine Installation entscheiden.

SKILL.md wird angezeigt

SKILL.md
Quellanweisungen · Schreibgeschützte Vorschau
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
Auf GitHub ansehen