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):
- Install SpecFact CLI:
pip install specfact-cli - 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-commit | Catching issues before they enter the repo | 2 minutes |
| VS Code | Real-time validation while coding | 2 minutes |
| Cursor | Validating AI suggestions | 2 minutes |
| GitHub Actions | Automated PR blocking | 5 minutes |
| CrossHair | Finding edge cases via formal verification | 5 minutes |
What Makes These Integrations Work
- CLI-First Design: Works with any tool, no platform lock-in
- Standard Exit Codes: Integrates with any CI/CD system
- Fast Execution: < 10 seconds for most validations
- Formal Guarantees: Runtime contracts + symbolic execution
- 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:
- ⚡ VS Code: Async race condition caught locally
- 🤖 Cursor: AI regression prevented
- 🔄 GitHub Actions: Type mismatch blocked from merging
- 🔒 Pre-commit: Breaking change detected before commit
- 🧮 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.