AI-powered code review with formal verification. Catch bugs, security vulnerabilities, and logical errors in code—particularly code generated by AI coding assistants.

• AI Semantic Analysis: LLM-powered understanding of code intent, logic, and potential issues
• Formal Verification: Z3 SMT solver provides mathematical proofs for:
  • Null safety violations
  • Array bounds checking
  • Integer overflow detection
  • Division by zero prevention
• GitHub Integration: Seamless PR checks, inline comments, and suggested fixes
• Multi-Language: Supports Python and TypeScript (more coming soon)
• Configurable: Per-repository settings via .codeverify.yml
• Team Dashboard: Track metrics, trends, and findings across your organization

• 🎯 Copilot Trust Score: ML-powered scoring of AI-generated code with risk assessment
• 🔌 Multi-VCS Support: GitHub, GitLab, and Bitbucket integration
• 🐛 Verification Debugger: Step-through Z3 constraint visualization
• 📝 Custom Rule Builder: No-code rule creation with pattern, AST, and semantic rules
• 📊 AI Diff Summarizer: Auto-generated PR descriptions and changelogs
• 🔍 Codebase-Wide Scanning: Scheduled full-repo analysis with trend tracking
• 💬 Slack/Teams Notifications: Real-time alerts for findings and scan results
• 🌐 Public API: RESTful API with webhooks for CI/CD integration
• 💻 VS Code Extension: Real-time verification as you code

CodeVerify combines the intelligence of large language models with the rigor of formal methods to catch bugs that traditional static analysis misses—especially important for AI-generated code.

flowchart TB
    subgraph Input["📥 Input"]
        PR[GitHub PR]
        CLI[CLI Tool]
        IDE[VS Code Extension]
    end

    subgraph GHA["🔗 GitHub App"]
        WH[Webhook Handler]
        Q[Redis Queue]
    end

    subgraph Worker["⚙️ Analysis Worker"]
        direction TB
        Parse[Parse Code]
        
        subgraph Agents["🤖 AI Agents"]
            direction LR
            Semantic[Semantic Agent<br/>GPT-4/Claude]
            Security[Security Agent<br/>OWASP/CWE]
        end
        
        subgraph Verifier["🔬 Formal Verifier"]
            Z3[Z3 SMT Solver]
        end
        
        Synthesis[Synthesis Agent]
    end

    subgraph Output["📤 Output"]
        Comment[PR Comment]
        Check[GitHub Check]
        Dashboard[Web Dashboard]
        SARIF[SARIF Report]
    end

    subgraph Data["💾 Data Layer"]
        PG[(PostgreSQL)]
        Redis[(Redis)]
    end

    PR --> WH
    CLI --> Parse
    IDE --> Parse
    WH --> Q --> Parse
    Parse --> Agents
    Parse --> Verifier
    Agents --> Synthesis
    Verifier --> Synthesis
    Synthesis --> Comment
    Synthesis --> Check
    Synthesis --> Dashboard
    Synthesis --> SARIF
    Synthesis --> PG
    Q --> Redis

codeverify/
├── apps/
│   ├── api/              # FastAPI backend service
│   ├── worker/           # Celery analysis workers
│   ├── web/              # Next.js dashboard
│   └── github-app/       # GitHub webhook handler
├── packages/
│   ├── core/             # Shared models, rules, notifications
│   ├── verifier/         # Z3 formal verification + debugger
│   ├── ai-agents/        # LLM agents (semantic, security, trust score, diff)
│   ├── cli/              # Command-line interface
│   ├── z3-mcp/           # Z3 MCP server (open source)
│   └── vscode-extension/ # VS Code extension for real-time verification
├── docker/               # Docker configurations
├── docs/                 # Documentation
│   └── api/              # API documentation
└── scripts/              # Development utilities

git clone https://github.com/codeverify/codeverify.git
cd codeverify
make setup              # Creates venv, installs deps, starts Postgres + Redis
source .venv/bin/activate
make dev                # Starts API, worker, dashboard, GitHub app

Run make help to see all available commands.

No Docker? No API keys? Just want to see it work?

pip install -e packages/core
python examples/quickstart.py     # Formal verification demo
python examples/custom_rules.py   # Rules engine demo

• Python 3.11+ (python3 --version)
• Node.js 20+ (for web dashboard and GitHub app only)
• Docker & Docker Compose (for PostgreSQL and Redis)
• GitHub App credentials (only for PR integration features)

git clone https://github.com/codeverify/codeverify.git
cd codeverify
cp .env.example .env
# Edit .env with your credentials (or just use defaults for local dev)

# Start infrastructure
docker compose up -d postgres redis

# Install Python packages
pip install -e "packages/core[dev]" \
            -e "packages/verifier[dev]" \
            -e "packages/ai-agents[dev]" \
            -e "apps/api[dev]" \
            -e "apps/worker[dev]"

# Install Node.js packages
cd apps/web && npm install && cd ../..
cd apps/github-app && npm install && cd ../..

# Run migrations
cd apps/api && alembic upgrade head && cd ../..

# Start services (in separate terminals)
uvicorn codeverify_api.main:app --reload      # API on :8000
celery -A codeverify_worker.main worker       # Worker
cd apps/web && npm run dev                     # Dashboard on :3000
cd apps/github-app && npm run dev              # GitHub App on :3001

make validate   # or: python scripts/validate_env.py

version: "1"

languages:
  - python
  - typescript

verification:
  enabled: true
  checks:
    - null_safety
    - array_bounds
    - integer_overflow

ai:
  enabled: true
  semantic: true
  security: true

thresholds:
  critical: 0   # Fail on any critical
  high: 0       # Fail on any high
  medium: 5     # Allow up to 5 medium
  low: 10       # Allow up to 10 low

exclude:
  - "node_modules/**"
  - "venv/**"
  - "tests/**"

See docs/examples/ for more configuration examples.

*At least one LLM API key is required for AI analysis.

# All tests
./scripts/test.sh

# Specific packages
pytest packages/verifier/tests -v
pytest packages/ai-agents/tests -v
pytest apps/api/tests -v
pytest apps/worker/tests -v

# With coverage
pytest --cov=codeverify --cov-report=html

• Getting Started - Full setup guide
• API Reference - REST API documentation
• Architecture - System design
• Verification - Z3 formal verification deep-dive
• Custom Rules - Creating custom rules
• Next-Gen Features - v0.3.0 features guide
• Troubleshooting - Common issues and solutions
• Configuration Examples - Sample .codeverify.yml files

• API Service: FastAPI with async SQLAlchemy
• Worker: Celery with Redis for job queue
• Dashboard: Next.js 14 with Tailwind CSS
• Database: PostgreSQL with Alembic migrations
• Verification: Z3 SMT solver Python bindings

sequenceDiagram
    participant Dev as Developer
    participant GH as GitHub
    participant App as GitHub App
    participant Q as Redis Queue
    participant W as Worker
    participant AI as AI Agents
    participant Z3 as Z3 Verifier
    participant DB as PostgreSQL
    participant API as API Service

    Dev->>GH: Open/Update PR
    GH->>App: Webhook (pull_request)
    App->>App: Verify HMAC signature
    App->>Q: Queue analysis job
    App->>GH: Set check status: pending
    
    Q->>W: Dequeue job
    W->>GH: Fetch PR diff
    W->>W: Parse code (tree-sitter)
    
    par Parallel Analysis
        W->>AI: Semantic analysis
        AI-->>W: Intent, contracts, issues
    and
        W->>AI: Security analysis
        AI-->>W: Vulnerabilities (OWASP/CWE)
    and
        W->>Z3: Formal verification
        Z3-->>W: Proofs, counterexamples
    end
    
    W->>W: Synthesize findings
    W->>DB: Store results
    W->>GH: Post PR comment
    W->>GH: Update check status
    
    Dev->>API: View dashboard
    API->>DB: Query results
    API-->>Dev: Analysis details

1. Add the check to packages/verifier/src/codeverify_verifier/z3_verifier.py
2. Add tests in packages/verifier/tests/
3. Update the config schema in packages/core/src/codeverify_core/config.py
4. Document in docs/verification.md

1. Create the agent in packages/ai-agents/src/codeverify_agents/
2. Inherit from BaseAgent and implement analyze() method
3. Add tests in packages/ai-agents/tests/
4. Register in the analysis pipeline

• VS Code extension — Real-time verification as you code
• Slack/Teams notifications — Real-time alerts for findings
• Custom rule builder — No-code rule creation
• Go + Java language support — Full verification for Go and Java
• CI/CD orchestrator — Multi-platform quality gates
• Supply chain verification — Dependency security and SBOM
• Self-learning rules — ML-powered false positive reduction
• SOC 2 compliance

We welcome contributions! Please see CONTRIBUTING.md for guidelines.

1. Fork the repository
2. Create a feature branch (git checkout -b feature/amazing-feature)
3. Make your changes
4. Run tests (./scripts/test.sh)
5. Submit a pull request

MIT License - see LICENSE for details.

• Z3 Theorem Prover - SMT solver
• OpenAI / Anthropic - LLM providers
• FastAPI - API framework
• Next.js - Dashboard framework