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.

Source facts

Repository
Z3Prover/a3-python-skill
Last source activity
February 18, 2026 at 22:52
Detected SKILL.md language
English
Stars
1
Forks
0

Install options

The review-first prompt is selected by default. You can switch to a direct command or download a local copy.

Review the source files

Read SKILL.md and any companion files shown by SkillsMP before deciding whether to install.

Showing SKILL.md

SKILL.md
Source instructions · Read-only preview
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