TL;DR: Legacy code modernization can introduce regressions that documentation alone does not prevent. Runtime contract enforcement can detect violations, while symbolic execution (CrossHair) explores edge cases mathematically. For high-risk systems in finance, healthcare, and data engineering, evidence from executable checks matters more than probabilistic LLM suggestions.

Verified Versions: This tutorial was tested and verified with the following version:

  • SpecFact CLI: 0.22.1

Commands and workflows in this guide are confirmed to work with this version. Check your version with specfact --version. For compatibility with other versions, refer to the SpecFact documentation.

The Problem

Legacy code modernization can be difficult because teams must change working systems without losing the behaviour that makes them valuable. Market-sizing estimates vary by scope and methodology; regardless of market size, the engineering risk is that changes introduce regressions that documentation alone does not prevent.

Teams struggle with:

  • Undocumented legacy code with no type hints, no tests, and buried business logic
  • Regressions during modernization — changes that break existing functionality
  • High-risk systems in finance, healthcare, and data pipelines where bugs cost millions
  • Developer onboarding taking weeks or months to understand legacy codebases

Traditional approaches focus on documentation — creating specs, writing markdown, generating API docs. But documentation has a fundamental problem: it can drift from code.

Why Documentation Isn't Enough

Documentation is valuable, but it has limitations:

Approach Problem Impact
Markdown specs Can drift from code over time Docs become outdated, misleading
Human code review Misses edge cases, especially in complex logic Bugs slip through to production
LLM suggestions Probabilistic, not guaranteed May miss critical edge cases
Static analysis Can't catch runtime behavior issues Type errors, async bugs, race conditions slip through

Real-world example: A team modernized a legacy Django payment system. They documented the API, wrote specs, and reviewed the code. But during refactoring, they introduced an async race condition that caused duplicate payments. Documentation didn't catch it — runtime enforcement would have.

The Solution: Runtime Contract Enforcement

Runtime contract enforcement is fundamentally different from documentation:

  1. Executable contracts — not just markdown, but actual code that runs
  2. Automatic regression detection — catches violations at runtime, not in review
  3. Formal verification — mathematical guarantees, not probabilistic suggestions
  4. CI/CD integration — blocks bad code automatically, no human review needed

How It Works

SpecFact CLI reverse engineers legacy code into executable contracts:

💡 Recommended: Use slash commands in your AI IDE (Cursor, VS Code + Copilot) for LLM-enriched analysis. The AI adds semantic understanding and business context.

# Option A: AI IDE Mode (Recommended)
# Step 1: Install slash commands
specfact init ide --ide cursor  # or --ide vscode

# Step 2: In your AI IDE, use the slash command:
/specfact.01-import --repo .

# Option B: CLI-Only Mode (Quick Start)
# Step 1: Reverse engineer legacy code
specfact project import from-code --repo . legacy-api

# Step 2: Analyze contracts
specfact code analyze contracts --bundle legacy-api

# Step 3: Enforce at runtime
specfact enforce sdd --sdd .specfact/sdd.yaml

What happens:

  • AST analysis extracts functions, classes, and dependencies
  • Contracts are generated from code patterns (not guessed by LLMs)
  • Runtime enforcement catches violations automatically
  • Symbolic execution (CrossHair) finds edge cases mathematically

Symbolic Execution: Mathematical Proof vs. LLM Guessing

One of SpecFact's unique capabilities is symbolic execution using CrossHair (an SMT solver). This is fundamentally different from LLM-based suggestions:

Approach Method Guarantee
LLM suggestions Probabilistic pattern matching May miss edge cases
Symbolic execution Mathematical proof (SMT solver) Deterministic, finds counterexamples

Example: A developer was refactoring a data validation function. An LLM suggested removing a None check to "simplify" the code. CrossHair symbolic execution found a counterexample proving the None check was necessary — preventing a production bug.

# LLM suggestion (would break!)
def process_data(data: list[dict]) -> dict:
    return {'status': 'success', 'count': len(data)}

# CrossHair found counterexample:
# Input: [None, {'value': 10}]
# Result: KeyError when accessing None['value']
# Fix: Keep None check

SpecFact's Approach

SpecFact CLI is designed for brownfield-first legacy modernization:

1. AST-Based Code Analysis

Unlike LLM-based approaches that "guess" what code does, SpecFact uses AST (Abstract Syntax Tree) analysis to extract actual code structure:

  • Functions, classes, and dependencies extracted from code
  • No type hints required — works with legacy code
  • Deterministic, not probabilistic

2. Runtime Contracts

Contracts are enforced at runtime using icontract and beartype:

  • beartype: Runtime type checking for all public APIs
  • icontract: Preconditions and postconditions
  • CrossHair: Property-based testing for edge case discovery

3. CI/CD Integration

SpecFact integrates seamlessly into existing workflows:

  • VS Code: Real-time validation while coding
  • Cursor: Validates AI suggestions before acceptance
  • GitHub Actions: Automated PR blocking
  • Pre-commit hooks: Catches issues before they enter the repo

Results

Results depend on the codebase, its risk profile, and how teams adopt the workflow. This article does not make generalised savings, defect-prevention, onboarding, or cost-avoidance claims without supporting case-study evidence.

When to Use Runtime Enforcement

Runtime contract enforcement is especially valuable for:

  • High-risk systems: Finance, healthcare, data pipelines where bugs cost millions
  • Legacy modernization: Undocumented codebases with no tests
  • AI-assisted refactoring: Validating LLM suggestions before acceptance
  • Team onboarding: New developers understanding legacy code

Not ideal for:

  • Greenfield projects (documentation-first tools work fine)
  • Low-risk internal tools (overkill for simple CRUD apps)
  • Rapid prototyping (formal verification adds overhead)

Try It Yourself

Ready to see runtime enforcement in action?

# Step 1: Install slash commands in your AI IDE
specfact init ide --ide cursor  # or --ide vscode

# Step 2: In your AI IDE, use the slash command:
/specfact.01-import --repo .

# The slash command runs CLI + LLM enrichment for better feature detection

💡 Best Practice: For best results, use slash commands in your AI IDE (Cursor, VS Code + Copilot). The LLM enriches the CLI output with semantic understanding, business context, and "why" reasoning.

Conclusion

Legacy code modernization is a $25B market, but documentation alone isn't enough. Runtime contract enforcement provides:

  • ✅ Executable contracts that can't drift from code
  • ✅ Automatic regression detection at runtime
  • ✅ Formal verification with mathematical guarantees
  • ✅ CI/CD integration that blocks bad code automatically

For high-risk systems in finance, healthcare, and data engineering, formal verification guarantees matter more than probabilistic LLM suggestions.

SpecFact CLI v0.20+ (Public Beta) is production-ready and designed specifically for brownfield legacy modernization. Try it today:

# Install slash commands
specfact init ide --ide cursor

# Then use in your AI IDE:
/specfact.01-import --repo .