# veriGuard-agent-safety-verification

> Generate safety policies as executable code with formal verification, enabling provably-correct agent behavior through offline policy generation and online runtime enforcement.

- Skill: `adu2021/veriguard-agent-safety-verification` (Agent Skill)
- Install (CLI): `npx skillmds@latest add adu2021/veriguard-agent-safety-verification`
- Raw SKILL.md: https://api.skillmd.com/api/skills/adu2021/veriguard-agent-safety-verification/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: AI & ML
- License: MIT
- Author: adu2021 (https://skillmd.com/u/adu2021)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/adu2021/veriguard-agent-safety-verification

---


# Technique: Formal Verification for Agent Safety Policies

Reactive guardrails for agent safety are prone to evasion. VeriGuard takes a proactive approach by formalizing security requirements as executable policies that are mathematically verified before deployment. Rather than detecting violations reactively, verified policies prevent unsafe actions by construction.

The key insight is treating safety as a code generation and verification problem: translate natural language security requirements into Python code paired with formal constraints, verify the code satisfies constraints mathematically, then enforce at runtime. This "correct-by-construction" approach provides formal guarantees rather than heuristic detection.

## Core Concept

VeriGuard operates through offline and online phases:

1. **Offline Policy Generation**: Translate requirements into executable policies with formal specs
2. **Three-Stage Refinement**: Validation (resolve ambiguities), testing (verify functionality), formal verification (prove correctness)
3. **Online Enforcement**: Runtime monitoring using verified policies

## Architecture Overview

- **Input**: Natural language security requirement
- **Specification**: Translate to Python + formal constraints
- **Validation Phase**: LLM resolves ambiguities in spec
- **Testing Phase**: Execute against test cases, refine on failures
- **Verification Phase**: Formal verifier (e.g., Nagini) proves spec compliance
- **Runtime**: Intercept agent actions, evaluate against verified policies
- **Response**: Block/allow/replicate based on verification result

## Implementation Steps

Implement policy specification generation.

```python
class SafetyPolicyGenerator:
    def __init__(self, llm_model, verifier_tool='nagini'):
        self.model = llm_model
        self.verifier = verifier_tool

    def generate_policy_from_requirement(self, security_requirement, context=''):
        """
        Generate executable policy from natural language requirement.

        Args:
            security_requirement: English description of security constraint
            context: Additional context (e.g., agent action types)

        Returns:
            policy: Dict with 'code', 'spec', 'status'
        """

        prompt = f"""Generate a Python policy function that enforces this requirement:

Requirement: {security_requirement}

Context: {context}

Format your response as:

CODE:
```python
def safety_policy(action, context, **kwargs):
    '''
    Pre-condition: [describe what must be true before]
    Post-condition: [describe what must be true after]
    '''
    # Policy implementation
    if <violation_condition>:
        return {'allowed': False, 'reason': '<reason>'}
    return {'allowed': True}
```

SPEC:
[Formal properties this policy ensures]
"""

        response = self.model.generate(prompt)

        # Parse code and spec
        code = self._extract_code(response)
        spec = self._extract_spec(response)

        return {'code': code, 'spec': spec, 'status': 'generated'}

    def _extract_code(self, response):
        """Extract Python code block."""
        import re
        match = re.search(r'```python\n(.*?)\n```', response, re.DOTALL)
        if match:
            return match.group(1)
        return ""

    def _extract_spec(self, response):
        """Extract formal specification."""
        if 'SPEC:' in response:
            return response.split('SPEC:')[1].strip()
        return ""
```

Implement validation phase for specification refinement.

```python
def validate_policy_specification(generator, code, spec, ambiguity_examples):
    """
    Validate policy by checking for ambiguities and refining.

    Args:
        generator: SafetyPolicyGenerator
        code: Policy code
        spec: Formal specification
        ambiguity_examples: List of edge cases

    Returns:
        refined_policy: Refined code and spec
    """

    validation_prompt = f"""Review this policy for ambiguities:

CODE:
{code}

SPEC:
{spec}

EDGE CASES:
{ambiguity_examples}

Identify potential ambiguities and provide clarifications."""

    clarifications = generator.model.generate(validation_prompt)

    # Refine code based on clarifications
    refinement_prompt = f"""Update the policy to address these clarifications:

Original: {code}
Clarifications: {clarifications}

Provide refined code."""

    refined_code = generator._extract_code(
        generator.model.generate(refinement_prompt)
    )

    return {'code': refined_code, 'spec': spec, 'status': 'validated'}
```

Implement testing phase.

```python
def test_policy(policy_code, test_cases):
    """
    Execute policy against test cases and fix failures.

    Args:
        policy_code: Generated policy function code
        test_cases: List of (action, expected_result) tuples

    Returns:
        test_results: Pass/fail for each test
    """

    # Compile policy function
    exec_globals = {}
    exec(policy_code, exec_globals)
    policy_func = exec_globals['safety_policy']

    test_results = []

    for action, expected_result in test_cases:
        try:
            result = policy_func(action, context={})
            passed = result['allowed'] == expected_result
            test_results.append({
                'action': action,
                'expected': expected_result,
                'actual': result['allowed'],
                'passed': passed
            })
        except Exception as e:
            test_results.append({
                'action': action,
                'error': str(e),
                'passed': False
            })

    return test_results
```

Implement formal verification using Nagini.

```python
def verify_policy_formally(policy_code, formal_spec, verifier_tool='nagini'):
    """
    Formally verify policy meets specification using automated verifier.

    Args:
        policy_code: Python code with pre/postconditions
        formal_spec: Formal specification
        verifier_tool: Verification tool (nagini, dafny, etc.)

    Returns:
        verification_result: {'passed': bool, 'details': str}
    """

    # Prepare code with formal annotations
    annotated_code = add_formal_annotations(policy_code, formal_spec)

    # Run verifier
    if verifier_tool == 'nagini':
        import subprocess
        result = subprocess.run(['nagini', '--python3', '-i'],
                              input=annotated_code, capture_output=True,
                              text=True)

        passed = result.returncode == 0
        details = result.stdout + result.stderr

    else:
        raise ValueError(f"Unknown verifier: {verifier_tool}")

    return {'passed': passed, 'details': details, 'code': annotated_code}


def add_formal_annotations(code, spec):
    """Add Nagini/Dafny annotations to Python code."""
    annotated = f'''# Specification: {spec}
# Pre-condition: Action is not None and has required fields
# Post-condition: Result is dict with 'allowed' key

{code}
'''
    return annotated
```

Implement runtime enforcement.

```python
class PolicyEnforcer:
    def __init__(self, verified_policies):
        """
        Initialize enforcer with verified policies.

        Args:
            verified_policies: List of verified policy codes
        """
        self.policies = []

        for policy_code in verified_policies:
            exec_globals = {}
            exec(policy_code, exec_globals)
            self.policies.append(exec_globals['safety_policy'])

    def evaluate_action(self, action, context):
        """
        Check action against all policies.

        Args:
            action: Proposed action
            context: Execution context

        Returns:
            result: {'allowed': bool, 'blocking_policies': list}
        """

        blocking_policies = []

        for policy in self.policies:
            result = policy(action, context)

            if not result['allowed']:
                blocking_policies.append(result.get('reason', 'Policy violation'))

        allowed = len(blocking_policies) == 0

        return {'allowed': allowed, 'blocking_policies': blocking_policies}
```

## Practical Guidance

| Aspect | Recommendation | Notes |
|--------|---------------|-------|
| Specification language | Clear, unambiguous English | Formal specs derive from natural language; precision critical |
| Verification tool | Nagini for Python | Supports subset of Python with formal reasoning |
| Test coverage | At least 10-20 cases per policy | More cases improve policy quality |
| Verification failure | Refine spec and iterate | Rarely succeed on first attempt; expectation is iteration |
| When to use | Critical safety-sensitive agents | Autonomous systems, financial decisions, access control |
| When NOT to use | Soft constraints or fuzzy requirements | Formal verification requires precise specs |
| Common pitfall | Over-specification or under-specification | Balance between expressiveness and verifiability |

### When to Use VeriGuard

- Autonomous agents in safety-critical domains
- Systems requiring formal guarantees of behavior
- Deployment without continuous human oversight
- Regulatory environments requiring auditable safety

### When NOT to Use VeriGuard

- Soft constraints where violation isn't catastrophic
- Policies requiring complex reasoning beyond formal methods
- Real-time systems where verification latency is prohibitive
- Rapidly changing requirement environments

### Common Pitfalls

- **Spec precision**: Underspecified requirements fail verification; be explicit
- **Completeness**: Policies may miss corner cases; use broad test coverage
- **Maintenance**: Verified policies require re-verification on changes; document updates
- **Overhead**: Verification can be slow; run offline, cache results

## Reference

Paper: https://arxiv.org/abs/2510.05156