# auto_formal_verifier

**Repository Path**: w1060/auto_formal_verifier

## Basic Information

- **Project Name**: auto_formal_verifier
- **Description**: No description available
- **Primary Language**: Unknown
- **License**: Not specified
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2026-02-01
- **Last Updated**: 2026-02-01

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# AutoFormalVerifier 🔍⚡

> **World-Class Multi-Agent System for Automated PoC Validation & Halmos Formal Verification**

## 🎯 Mission

Automatically transform incomplete Solidity PoC code slices into **production-grade Halmos symbolic tests** that prove security properties under realistic constraints.

## 🏗️ Architecture

```
┌─────────────────────────────────────────────────────────────┐
│                  AutoFormalVerifier Pipeline                 │
└─────────────────────────────────────────────────────────────┘
                              │
                              ▼
        ┌─────────────────────────────────────┐
        │   Input: Incomplete PoC Slice       │
        └─────────────────────────────────────┘
                              │
        ╔═════════════════════╧═════════════════════╗
        ║         PHASE 1: CODE RESURRECTION        ║
        ║  Agent A: Iterative Resurrector           ║
        ║  - Add imports, interfaces, setup         ║
        ║  - Self-healing compilation loop          ║
        ║  - Max retries: 3                         ║
        ╚═══════════════════╤═══════════════════════╝
                            │
                  ┌─────────▼─────────┐
                  │  forge build      │◄──┐
                  └─────────┬─────────┘   │
                            │              │
                       ✓ Success?          │
                            │ No───────────┘
                            │ Yes
        ╔═════════════════════╧═════════════════════╗
        ║      PHASE 2: HOLISTIC ASSESSMENT         ║
        ║  Agent B: Security Auditor (GPT-4o)       ║
        ║  - Environment dependency analysis        ║
        ║  - State consistency verification         ║
        ║  - Atomicity & access control check       ║
        ║  - Asset conservation law validation      ║
        ║  - Economic incentive evaluation          ║
        ║  Output: Risk Level + Verification Strategy║
        ╚═══════════════════╤═══════════════════════╝
                            │
        ╔═════════════════════╧═════════════════════╗
        ║   PHASE 3: SYMBOLIC TEST GENERATION       ║
        ║  Agent C: Verification Engineer           ║
        ║  - Replace cheats with svm.createUint256  ║
        ║  - Add realistic vm.assume constraints    ║
        ║  - Convert to property-based assertions   ║
        ║  - Self-healing compilation loop          ║
        ╚═══════════════════╤═══════════════════════╝
                            │
                  ┌─────────▼─────────┐
                  │  forge build      │◄──┐
                  └─────────┬─────────┘   │
                            │              │
                       ✓ Success?          │
                            │ No───────────┘
                            │ Yes
        ┌─────────────────────▼──────────────────────┐
        │  Output: Compilable Halmos Test + Report   │
        └────────────────────────────────────────────┘
```

## 🚀 Quick Start

### Installation

```bash
# Clone the repository
cd auto_formal_verifier

# Edit config.toml and add your API keys:
# [agents.resurrector]
# api_key = "sk-your-deepseek-api-key"
# [agents.assessor]
# api_key = "sk-your-openai-api-key"

# Build the project
cargo build --release

# Run the system
cargo run --release -- --input examples/poc_slice.sol --output ./results
```

### Usage

```bash
auto_formal_verifier \
  --input path/to/poc_slice.sol \
  --config config.toml \
  --output ./verification_results \
  --verbose
```

## 📋 Configuration

Edit `config.toml` to customize agents:

```toml
[agents.resurrector]
provider = "deepseek"
model = "deepseek-coder"
max_retries = 3
temperature = 0.2

[agents.assessor]
provider = "openai"
model = "gpt-4o"
max_retries = 2
temperature = 0.3

[agents.verifier]
provider = "deepseek"
model = "deepseek-coder"
max_retries = 3
temperature = 0.1
```

## 🤖 Agent Roles

### Agent A: Iterative Resurrector
- **Model**: DeepSeek-Coder (optimized for code generation)
- **Task**: Complete incomplete PoC code
- **Features**:
  - Automatic import detection
  - Interface generation
  - Self-healing on compilation errors (max 3 retries)

### Agent B: Holistic Assessor
- **Model**: GPT-4o (high reasoning capability)
- **Task**: 5-dimensional security audit
- **Dimensions**:
  1. Environment Dependency (Mock vs. Real)
  2. State Consistency (Achievable vs. Fabricated)
  3. Atomicity & Access Control
  4. Asset Conservation Law
  5. Economic Incentive
- **Output**: Risk level + verification strategy

### Agent C: Verification Engineer
- **Model**: DeepSeek-Coder
- **Task**: Generate Halmos symbolic tests
- **Transformations**:
  - `vm.deal()` → `svm.createUint256()` + `vm.assume()`
  - Concrete assertions → Property-based invariants
  - Mock elimination

## 🔧 Technical Stack

| Component | Technology |
|-----------|-----------|
| Language | Rust (Edition 2021) |
| Async Runtime | Tokio |
| HTTP Client | Reqwest |
| Serialization | Serde |
| Compiler | Foundry (forge) |
| Symbolic Testing | Halmos |
| Logging | Tracing |

## 📊 Output Artifacts

The system generates:

1. **`report_<session_id>.json`**: Complete audit report
   ```json
   {
     "session_id": "uuid",
     "success": true,
     "assessment": {
       "is_valid": false,
       "risk_level": "FalsePositive",
       "dimensions": { ... },
       "strategy_for_formal_verification": "..."
     },
     "halmos_test": "...",
     "compilation_logs": [ ... ]
   }
   ```

2. **`resurrected.t.sol`**: Compilable PoC code
3. **`halmos_test.t.sol`**: Symbolic verification test

## 🎯 Example Workflow

**Input** (`poc_slice.sol`):
```solidity
// Incomplete PoC
function test_vulnerability() {
    vault.withdraw(exploitAmount);
    assertGt(attacker.balance(), initial);
}
```

**Output** (`halmos_test.t.sol`):
```solidity
function check_NoExcessWithdrawal() public {
    uint256 exploitAmount = svm.createUint256('exploitAmount');
    uint256 vaultBalance = svm.createUint256('vaultBalance');
    
    vm.assume(exploitAmount > 0 && exploitAmount <= 1_000_000 ether);
    vm.assume(vaultBalance >= exploitAmount);
    
    uint256 attackerBalanceBefore = attacker.balance();
    vault.withdraw(exploitAmount);
    
    // Property: Withdrawal cannot exceed deposited amount
    assert(attacker.balance() - attackerBalanceBefore <= vaultBalance);
}
```

## 🧪 Testing

```bash
# Run unit tests
cargo test

# Run with specific test
cargo test test_compilation_loop

# Run example workflow
cargo run --example simple_poc
```

## 🔬 Advanced Features

### Retry Logic with Error Feedback

The system implements a **self-healing loop**:

```rust
for attempt in 1..=max_retries {
    let output = agent.execute(&input).await?;
    let code = output.content;
    
    let compilation = compiler.compile(&code)?;
    
    if compilation.success {
        return Ok(code);
    }
    
    // Feed error back to agent
    input = input.with_error(compilation.error_details);
}
```

### Model Specialization

Different models for different tasks:
- **Code Generation**: DeepSeek-Coder (low temp 0.1-0.2)
- **Reasoning**: GPT-4o (medium temp 0.3)

### Symbolic Constraint Generation

Automatic conversion:
```
vm.deal(user, 1000 ether)
    ↓
uint256 balance = svm.createUint256('balance');
vm.assume(balance > 0 && balance <= 10000 ether);
```

## 📚 Architecture Details

### Directory Structure

```
auto_formal_verifier/
├── Cargo.toml
├── config.toml
├── src/
│   ├── main.rs              # CLI entry point
│   ├── config.rs            # Configuration management
│   ├── llm.rs               # LLM client wrapper
│   ├── workflow.rs          # Main orchestrator
│   ├── agents/
│   │   ├── mod.rs           # Agent trait definition
│   │   ├── resurrector.rs   # Agent A implementation
│   │   ├── assessor.rs      # Agent B implementation
│   │   └── verifier.rs      # Agent C implementation
│   └── tools/
│       ├── mod.rs
│       └── compiler.rs      # Forge wrapper
└── README.md
```

### Key Design Patterns

1. **Trait-based Agent Interface**: Enables polymorphism and testing
2. **Async/Await**: Non-blocking LLM calls
3. **Builder Pattern**: Fluent API for agent inputs
4. **Error Propagation**: Context-rich errors with `anyhow`

## 🛡️ Security Considerations

The system detects common PoC anti-patterns:

- ✅ Mock contract usage
- ✅ Arbitrary state manipulation (vm.store)
- ✅ Asset conservation violations
- ✅ Permission bypasses
- ✅ Unrealistic economic assumptions

## 🔮 Future Enhancements

- [ ] Support for more LLM providers (Anthropic, Cohere)
- [ ] Parallel agent execution for speed
- [ ] Interactive mode with human-in-the-loop
- [ ] Integration with CI/CD pipelines
- [ ] Web UI dashboard

## 📖 License

MIT License - see LICENSE file for details

## 🤝 Contributing

Contributions welcome! Please read CONTRIBUTING.md

---

**Built with ❤️ by the AutoFormalVerifier team**