# Violation Analyzer

A smart contract formal verification rule analysis tool that identifies false positives by analyzing state reachability and consistency using AI-powered analysis.

## Overview

The Violation Analyzer processes formal verification rule violations from Certora Prover runs and classifies them as either:

- **FALSE_POSITIVE**: Violations caused by impossible pre-states or verification tool artifacts
- **POTENTIAL_TRUE_POSITIVE**: Genuine contract issues or violations with reachable pre-states

The tool uses Claude Opus with majority voting to provide reliable classifications and groups results into actionable categories based on missing invariants.

## Features

- **Dual Input Modes**: Analyze single contract files or automatically collect all .sol files from a job
- **Multiple Data Sources**: Work with local job directories (`emv-*`) or remote Certora job URLs
- **AI-Powered Analysis**: Uses Claude Opus with sophisticated prompts for accurate classification
- **Majority Voting**: Configurable voting system for reliable results
- **Smart Categorization**: Groups violations by missing invariants to guide specification improvements
- **Efficient Caching**: Context caching for improved performance on large jobs

## Installation

Ensure you have Python 3.11+ and install dependencies:

```bash
pip install -r requirements.txt
```

Set your Anthropic API key:
```bash
export ANTHROPIC_API_KEY="your-api-key-here"
```

## Usage

### Basic Command Structure

```bash
python violation_analyzer.py [DATA_SOURCE] [CONTRACT_SOURCE] [OPTIONS]
```

### Data Source Options (required, mutually exclusive)

**Local job directory:**
```bash
--job-dir /path/to/emv-*
```

**Remote job URL:**
```bash
--job-url "https://prover.certora.com/output/12345/abc123/?anonymousKey=xyz"
```

### Contract Source Options (required, mutually exclusive)

**Single contract file:**
```bash
--contract-file /path/to/Contract.sol
```

**Collect all .sol files from job:**
```bash
--collect-sources
```

### Optional Parameters

- `--output-file FILENAME`: Output file for results (default: `analysis_results.json`)
- `--num-votes N`: Number of votes for majority voting (default: 3)
- `--vote-threshold RATIO`: Threshold for false positive classification (default: 0.5)

## Examples

### Analyze with single contract file and local job directory
```bash
python violation_analyzer.py \
  --job-dir ./emv-3-certora-17-Jul--11-17 \
  --contract-file ./contracts/MyContract.sol \
  --output-file my_analysis.json
```

### Analyze with collected sources from remote job
```bash
python violation_analyzer.py \
  --job-url "https://prover.certora.com/output/12345/abc123/?anonymousKey=xyz" \
  --collect-sources \
  --num-votes 5 \
  --vote-threshold 0.6
```

### Analyze local job with collected sources
```bash
python violation_analyzer.py \
  --job-dir ./emv-3-certora-17-Jul--11-17 \
  --collect-sources
```

## Output Format

The tool generates a JSON file with two main sections:

### Majority Vote Results
Individual violation analysis with voting details:
```json
{
  "rule_name": "rule_example",
  "final_classification": "FALSE_POSITIVE",
  "individual_votes": [...],
  "false_positive_votes": 2,
  "potential_true_positive_votes": 1
}
```

### Categorization
Grouped violations by missing invariants:
```json
{
  "categories": [
    {
      "category_name": "Potential True Positives",
      "description": "Violations requiring manual review",
      "rule_names": ["rule1", "rule2"]
    },
    {
      "category_name": "Block timestamps must be monotonically increasing",
      "description": "Add temporal invariant for timestamp ordering",
      "rule_names": ["rule3", "rule4"]
    }
  ]
}
```

## Analysis Framework

The tool focuses on **property-relevant analysis**, examining only pre-state elements that are actually relevant to the violated property. Key analysis areas include:

- **Pre-State Reachability**: Can this combination of storage variables, inputs, and builtins realistically occur?
- **Property Relevance**: Which elements actually affect the violated property?
- **Contract Bug vs Tool Artifact**: Does this represent a genuine contract issue or a verification tool limitation?

## Configuration

### Voting Parameters
- `num_votes`: Higher values increase reliability but cost more
- `vote-threshold`: Higher values are more cautious (require more votes to mark as false positive)

### Performance Considerations
- The tool uses three-phase context caching for optimal performance
- Large jobs with many violations benefit from higher concurrency limits
- Remote jobs may be slower due to API rate limits

## Troubleshooting

**"No rule violations found"**: Check that the job actually has violated rules in the treeView status.

**API errors**: Verify your Anthropic API key is set correctly and you have sufficient credits.

**Hidden directory files**: The tool automatically ignores .sol files in hidden directories (those starting with '.').

## Architecture

- `violation_analyzer.py`: Main script with argument parsing and orchestration
- `prover_utils.py`: Utilities for processing Certora data and API interactions
- Uses structured output with Pydantic models for reliable AI responses
- Implements sophisticated context caching for performance optimization

## Contributing

When modifying the analysis prompts, test with diverse violation types to ensure the classification logic remains sound. The tool errs on the side of caution to avoid missing genuine security issues.
