SpecFact CLI works with your existing tools — no new platform to learn. These examples show real bugs that were caught through different integrations: VS Code, Cursor, GitHub Actions, pre-commit hooks, and AI assistants.

Why These Examples Matter

Every tool claims to catch bugs. But which bugs? In what context?

We documented 5 real scenarios where SpecFact CLI caught bugs that other tools missed — each using a different integration point. No hypotheticals, no "potential issues" — these are actual bugs that would have reached production.


Bug #1: Async Race Condition (VS Code Integration)

The Problem

A developer was refactoring a legacy Django view to use async/await. The code looked correct but had a subtle async bug that would cause race conditions in production.

# views.py - Legacy Django view being modernized
def process_payment(request):
    user = get_user(request.user_id)
    payment = create_payment(user.id, request.amount)
    send_notification(user.email, payment.id)  # ⚠️ Blocking call in async context
    return JsonResponse({status": "success"})

The Integration

Setup (one-time, takes 2 minutes):

  1. Install SpecFact CLI: pip install specfact-cli
  2. Add a pre-commit hook:
# .git/hooks/pre-commit
#!/bin/sh
specfact --no-banner enforce stage --preset balanced
specfact --no-banner repro --fail-fast

What SpecFact Caught

🚫 Contract Violation: Blocking I/O in async context
   File: views.py:45
   Function: process_payment
   Issue: send_notification() is a blocking call
   Severity: HIGH
   Fix: Use async version or move to background task

The Fix

# Fixed code
async def process_payment(request):
    user = await get_user_async(request.user_id)
    payment = await create_payment_async(user.id, request.amount)
    await send_notification_async(user.email, payment.id)  # ✅ Async call
    return JsonResponse({status": "success"})

✅ Result

  • Bug caught: Before commit (local validation)
  • Time saved: Prevented production race condition
  • Integration: VS Code + pre-commit hook

Bug #2: AI-Suggested Regression (Cursor Integration)

The Problem

A developer was using Cursor AI to refactor a legacy data pipeline. The AI assistant suggested changes that looked correct but would have broken a critical edge case.

# pipeline.py - Legacy data processing
def process_data(data: list[dict]) -> dict:
    if not data:
        return {status": "empty", "count": 0}
    
    # Critical: handles None values in data
    filtered = [d for d in data if d is not None and d.get("value") is not None]
    
    if len(filtered) == 0:
        return {status": "no_valid_data", "count": 0}
    
    return {
        "status": "success",
        "count": len(filtered),
        "total": sum(d["value"] for d in filtered)
    }

The Problem with AI's Suggestion

The AI suggested removing the None check to "simplify" the code. This would have broken production:

# AI's suggestion (would break!)
def process_data(data: list[dict]) -> dict:
    if not data:
        return {status": "empty", "count": 0}
    
    # ⚠️ None check removed - breaks edge case!
    return {
        "status": "success",
        "count": len(data),
        "total": sum(d["value"] for d in data)  # 💥 KeyError on None values
    }

What SpecFact Caught

🚫 Contract Violation: Missing None check
   File: pipeline.py:12
   Function: process_data
   Issue: Suggested code removes None check, breaking edge case
   Severity: HIGH
   Contract: Must handle None values in input data
   Fix: Keep None check or add explicit contract

The Fix

# AI suggestion rejected, kept original with contract
@icontract.require(lambda data: isinstance(data, list))
@icontract.ensure(lambda result: result["count"] >= 0)
def process_data(data: list[dict]) -> dict:
    if not data:
        return {status": "empty", "count": 0}
    
    # Contract enforces None handling
    filtered = [d for d in data if d is not None and d.get("value") is not None]
    
    if len(filtered) == 0:
        return {status": "no_valid_data", "count": 0}
    
    return {
        "status": "success",
        "count": len(filtered),
        "total": sum(d["value"] for d in filtered)
    }

✅ Result

  • Regression prevented: Edge case preserved
  • AI validation: Cursor suggestions validated before acceptance
  • Contract enforcement: Runtime guarantees maintained

Bug #3: Type Mismatch (GitHub Actions Integration)

The Problem

A developer submitted a PR that added a new feature but introduced a type mismatch that would cause runtime errors.

# api.py - New endpoint added
def get_user_stats(user_id: str) -> dict:
    user = User.objects.get(id=user_id)
    stats = calculate_stats(user)  # Returns int, not dict
    return stats  # ⚠️ Type mismatch: int vs dict

The Integration

Create .github/workflows/specfact-enforce.yml:

name: SpecFact Validation

on:
  pull_request:
    branches: [main]

jobs:
  validate:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - name: Set up Python
        uses: actions/setup-python@v5
        with:
          python-version: "3.11"
      - name: Install SpecFact CLI
        run: pip install specfact-cli
      - name: Configure Enforcement
        run: specfact --no-banner enforce stage --preset balanced
      - name: Run SpecFact Validation
        run: specfact --no-banner repro --repo . --budget 90

What SpecFact Caught

🚫 Contract Violation: Return type mismatch
   File: api.py:45
   Function: get_user_stats
   Issue: Function returns int, but contract requires dict
   Severity: HIGH
   Contract: @ensure(lambda result: isinstance(result, dict))
   Fix: Return dict with stats, not raw int

The Fix

# Fixed code
@icontract.ensure(lambda result: isinstance(result, dict))
def get_user_stats(user_id: str) -> dict:
    user = User.objects.get(id=user_id)
    stats_value = calculate_stats(user)
    return {stats": stats_value}  # ✅ Returns dict

✅ Result

  • Merge blocked: PR failed CI check
  • Type safety: Runtime type error prevented
  • Automated: No manual review needed

Bug #4: Breaking Change (Pre-commit Hook)

The Problem

A developer modified a legacy function's signature without updating callers, breaking backward compatibility.

# legacy.py - Function signature changed
def process_order(order_id: str, user_id: str) -> dict:  # ⚠️ Added required user_id
    # ... implementation
# caller.py - Still using old signature
result = process_order(order_id="123")  # ⚠️ Missing user_id

What SpecFact Caught

🚫 Contract Violation: Breaking change detected
   File: legacy.py:12
   Function: process_order
   Issue: Signature changed from (order_id) to (order_id, user_id)
   Severity: HIGH
   Impact: 3 callers will break
   Fix: Make user_id optional or update all callers

The Fix

# Fixed: Made user_id optional to maintain backward compatibility
def process_order(order_id: str, user_id: str | None = None) -> dict:
    if user_id is None:
        # Legacy behavior
        user_id = get_default_user_id()
    # ... implementation

✅ Result

  • Breaking change caught: Before commit
  • Backward compatibility: Maintained
  • Local validation: No CI delay

Bug #5: Division by Zero (CrossHair Symbolic Execution)

💡 Best Practice: Use /specfact.07-contracts in your AI IDE to add contracts with CrossHair exploration. The slash command orchestrates the full workflow: analyze → generate prompts → apply with LLM validation.

The Problem

A developer was using an AI coding assistant to add input validation. The code looked correct but had an edge case that would cause division by zero.

# validator.py - AI-generated validation
def validate_and_calculate(data: dict) -> float:
    value = data.get("value", 0)
    divisor = data.get("divisor", 1)
    return value / divisor  # ⚠️ Edge case: divisor could be 0

What SpecFact Caught

CrossHair Symbolic Execution discovered the edge case using mathematical proof (not guessing):

🔍 CrossHair Exploration: Found counterexample
   File: validator.py:5
   Function: validate_and_calculate
   Issue: Division by zero when divisor=0
   Counterexample: {value": 10, "divisor": 0}
   Severity: HIGH
   Fix: Add divisor != 0 check

The Fix

# Fixed with contract
@icontract.require(lambda data: data.get("divisor", 1) != 0)
def validate_and_calculate(data: dict) -> float:
    value = data.get("value", 0)
    divisor = data.get("divisor", 1)
    return value / divisor  # ✅ Contract ensures divisor != 0

✅ Result

  • Edge case found: Mathematical proof, not LLM guess
  • Symbolic execution: CrossHair discovered counterexample
  • Formal verification: Deterministic, not probabilistic

Integration Patterns Summary

Integration Best For Setup Time
Pre-commitCatching issues before they enter the repo2 minutes
VS CodeReal-time validation while coding2 minutes
CursorValidating AI suggestions2 minutes
GitHub ActionsAutomated PR blocking5 minutes
CrossHairFinding edge cases via formal verification5 minutes

What Makes These Integrations Work

  1. CLI-First Design: Works with any tool, no platform lock-in
  2. Standard Exit Codes: Integrates with any CI/CD system
  3. Fast Execution: < 10 seconds for most validations
  4. Formal Guarantees: Runtime contracts + symbolic execution
  5. Zero Configuration: Works out of the box

Bugs Caught That Other Tools Missed

  • Async bugs: Blocking calls in async context
  • Type mismatches: Runtime type errors
  • Breaking changes: Backward compatibility issues
  • Edge cases: Division by zero, None handling
  • Contract violations: Missing preconditions/postconditions

Try It Yourself

Pick your integration and add SpecFact validation:

# Create pre-commit hook (sets enforcement + runs validation)
cat > .git/hooks/pre-commit << 'EOF'
#!/bin/sh
specfact --no-banner enforce stage --preset balanced
specfact --no-banner repro --fail-fast
EOF
chmod +x .git/hooks/pre-commit

# Run validation now (manually)
specfact --no-banner enforce stage --preset balanced
specfact --no-banner repro --verbose

Conclusion

These 5 examples demonstrate real bugs caught through different integration points:

  1. VS Code: Async race condition caught locally
  2. 🤖 Cursor: AI regression prevented
  3. 🔄 GitHub Actions: Type mismatch blocked from merging
  4. 🔒 Pre-commit: Breaking change detected before commit
  5. 🧮 CrossHair: Division by zero found via symbolic execution

Remember: SpecFact CLI's core strength is seamless integration into your existing workflow. Start with one integration, then expand as you see value.