when-to-use-z3

class PricingValidator:
    def validate(self, original, discount, final):
        expected = original * (1 - discount / 100)
        return final == expected  # Just checks THIS value

from z3 import *

def prove_pricing_formula_is_correct():
    """Proves the formula works for ALL inputs"""
    original = Real('original')
    discount = Real('discount')
    final = Real('final')

    solver = Solver()

    # The formula we claim is correct
    solver.add(final == original * (1 - discount / 100))

    # Add constraints
    solver.add(original >= 0)
    solver.add(And(discount >= 0, discount <= 100))

    # Try to find a counterexample
    solver.add(final < 0)  # This should be impossible

    if solver.check() == unsat:
        return "✅ PROVEN: Formula never produces negative prices"
    else:
        return "❌ FOUND COUNTEREXAMPLE!"

{
  "Effect": "Allow",
  "Action": ["s3:*"],
  "Resource": "arn:aws:s3:::my-bucket/*",
  "Condition": {
    "IpAddress": {
      "aws:SourceIp": ["203.0.113.0/24", "198.51.100.0/24"]
    }
  }
}

def validate_policy(policy):
    # Check specific test cases
    assert has_ip_condition(policy)
    assert action_is_scoped(policy)
    # Misses: What if someone adds another condition?

from z3 import *

# Model the policy as logical formula
def verify_policy_never_grants_admin():
    # Variables
    action = String('action')
    ip = String('source_ip')
    resource = String('resource')

    solver = Solver()

    # Policy rules (encoded as logic)
    solver.add(Or(
        action == "s3:GetObject",
        action == "s3:PutObject"
    ))
    solver.add(Or(
        PrefixOf("203.0.113.", ip),
        PrefixOf("198.51.100.", ip)
    ))

    # Try to find case where admin is granted
    solver.add(action == "iam:CreateUser")  # Admin action

    if solver.check() == unsat:
        return "✅ PROVEN: Policy never grants admin access"
    else:
        return "❌ SECURITY HOLE FOUND!"

from z3 import *

class DynamicConstraintValidator:
    def __init__(self):
        self.solver = Solver()

    def validate_restaurant(self, people, dishes, custom_rules):
        """
        Validate with context-specific rules

        custom_rules example:
        {
            "Alice": {"allergies": ["dairy", "gluten"]},
            "Bob": {"diet": "vegetarian", "exclude": ["salmon"]},
            "Carol": {"copies": "Bob"}
        }
        """

        # Create variables dynamically
        assignments = {
            person: Int(f'{person}_dish')
            for person in people
        }

        # Add dynamic constraints based on context
        for person, rules in custom_rules.items():

            # Allergy constraints (dynamic based on person)
            if "allergies" in rules:
                allowed_dishes = [
                    dish_id for dish_id, dish in enumerate(dishes)
                    if not any(allergen in dish["contains"]
                              for allergen in rules["allergies"])
                ]
                self.solver.add(Or([
                    assignments[person] == dish_id
                    for dish_id in allowed_dishes
                ]))

            # Diet constraints (vegetarian, vegan, etc.)
            if "diet" in rules:
                if rules["diet"] == "vegetarian":
                    veg_dishes = [
                        i for i, d in enumerate(dishes)
                        if d["vegetarian"]
                    ]
                    self.solver.add(Or([
                        assignments[person] == i
                        for i in veg_dishes
                    ]))

            # Dependency constraints (eat same as someone)
            if "copies" in rules:
                other_person = rules["copies"]
                self.solver.add(
                    assignments[person] == assignments[other_person]
                )

        return self.solver.check() == sat

# Usage with different contexts
validator = DynamicConstraintValidator()

# Context 1: Just allergies
result1 = validator.validate_restaurant(
    people=["Alice", "Bob"],
    dishes=[...],
    custom_rules={
        "Alice": {"allergies": ["dairy"]}
    }
)

# Context 2: Complex rules
result2 = validator.validate_restaurant(
    people=["Alice", "Bob", "Carol"],
    dishes=[...],
    custom_rules={
        "Alice": {"allergies": ["dairy", "gluten"]},
        "Bob": {"diet": "vegetarian"},
        "Carol": {"copies": "Bob"}
    }
)

# Normal validator - only checks specific cases
def validate_invoice(subtotal, tax_rate, discount, total):
    expected = (subtotal - discount) * (1 + tax_rate)
    return abs(total - expected) < 0.01  # Checks ONE case

# Z3 - proves formula is correct for ALL cases
def prove_invoice_formula():
    subtotal = Real('subtotal')
    tax = Real('tax_rate')
    discount = Real('discount')
    total = Real('total')

    solver = Solver()
    solver.add(total == (subtotal - discount) * (1 + tax))

    # Business rules
    solver.add(subtotal >= 0)
    solver.add(And(tax >= 0, tax <= 1))
    solver.add(And(discount >= 0, discount <= subtotal))

    # Prove total is never negative
    solver.add(total < 0)

    if solver.check() == unsat:
        return "✅ PROVEN: Formula never produces negative invoices"

# Normal validator - can't handle policy combinations
def check_access(user, action, resource):
    # You'd have to enumerate all combinations
    # Misses edge cases!
    pass

# Z3 - proves no unauthorized access is possible
def verify_no_unauthorized_access():
    # Model all policies as logical formulas
    # Z3 searches ALL possible combinations
    # Returns proof or counterexample
    pass

# Normal validator - dangerous to only test specific cases!
def validate_dosage(weight, age, dose):
    max_safe = weight * 0.5
    return dose <= max_safe  # Only checks THIS case

# Z3 - proves dosage is ALWAYS safe
def prove_dosage_always_safe():
    weight = Real('weight')
    age = Real('age')
    dose = Real('dose')

    solver = Solver()

    # Dosage formula
    solver.add(dose == weight * 0.5 * (age / 100))

    # Constraints
    solver.add(And(weight >= 0, weight <= 200))  # kg
    solver.add(And(age >= 0, age <= 120))        # years

    # Prove dose never exceeds safe limit
    solver.add(dose > weight * 0.5)

    if solver.check() == unsat:
        return "✅ PROVEN: Dosage formula is always safe"
    else:
        model = solver.model()
        return f"❌ DANGEROUS! Counterexample found: {model}"

def validate(assignments):
    if assignments["Alice"] == "Grilled Salmon":
        assert is_vegetarian(assignments["David"])

solver = Solver()

# Existing constraints
solver.add(alice_dish == 2)  # Must eat salmon (only option)

# New constraint
solver.add(Implies(
    alice_dish == 2,  # If Alice eats salmon
    Or(david_dish == 1, david_dish == 3, david_dish == 4)  # David vegetarian
))

# David must be unique
solver.add(david_dish != bob_dish)  # Bob has dish 1
solver.add(david_dish != carol_dish)  # Carol has dish 1

if solver.check() == unsat:
    print("❌ IMPOSSIBLE! Constraints contradict each other")
    # Z3 found the bug automatically!

User Query → LLM → Response
                      ↓
               Is it high-stakes?
                 ↙️        ↘️
              YES         NO
               ↓           ↓
        Z3 Verification  Return
               ↓
         Valid/Invalid