CsFv.SmtGen 11.2.6

CS-FV: C# Formal Verification

Status: v6.0 In Progress (Phase 34 of 39 complete) Latest Release: v5.0.0 (2026-02-09) - Production-Ready with Comprehensive V5 Feature Set

CS-FV is a production-ready formal verification tool for C# that uses Roslyn semantic analysis and CVC5 SMT solving to verify correctness properties of modern C# code, supporting C# 11-14 features, async/await patterns, LINQ, and advanced async patterns (ValueTask, IAsyncEnumerable, Channels).

---

✨ Highlights

• ✅ Modern C# 11-14 Support - Full verification of modern C# features
• ✅ Advanced Async Patterns - ValueTask, async iterators, channels with producer-consumer semantics
• ✅ Production-Ready - 2,000+ passing tests, zero regressions, five shipped milestones
• ✅ CLI & Library - Command-line tool and NuGet packages for library integration
• 🚀 High Performance - ❤️% regression vs baseline with comprehensive optimization

---

Quick Start

Installation

Option 1: Install from NuGet (Recommended)

# Add to your project — includes contract attributes + Roslyn analyzer
dotnet add package CsFv

# Install the CLI tool globally (optional — for command-line verification)
dotnet tool install -g CsFv.Cli

Option 2: Build from Source

git clone https://github.com/hapyy/cs-fv.git
cd cs-fv
dotnet build
dotnet tool install -g --add-source ./artifacts CsFv.Cli

Prerequisites

An SMT solver is required for verification:

# macOS
brew install cvc5

# Ubuntu/Debian
sudo apt-get install cvc5

# Verify
cvc5 --version    # 1.0.0 or later
dotnet --version  # 8.0.0 or later

NuGet Packages

Package	Description	Install
CsFv	All-in-one — contracts + analyzer	dotnet add package CsFv
CsFv.Cli	Command-line tool	dotnet tool install -g CsFv.Cli
CsFv.Contracts	Contract attributes only	dotnet add package CsFv.Contracts
CsFv.Analyzers	Roslyn analyzer only	dotnet add package CsFv.Analyzers
CsFv.Core	Core pipeline (library use)	dotnet add package CsFv.Core
CsFv.SmtGen	SMT-LIB2 generator (library use)	dotnet add package CsFv.SmtGen
CsFv.Verification	SMT solver integration (library use)	dotnet add package CsFv.Verification

Usage

# Initialize configuration in your project
cs-fv init

# Verify a C# file
cs-fv verify MyClass.cs

# Check contract syntax (fast, no verification)
cs-fv check src/

# Verbose output with SMT code
cs-fv verify --verbose MyClass.cs

Example Contract

using CsFv.Contracts;

public class Calculator
{
    [Requires("x > 0")]
    [Requires("y > 0")]
    [Ensures("result > 0")]
    [Ensures("result >= x")]
    [Ensures("result >= y")]
    public int Add(int x, int y)
    {
        return x + y;
    }
}

Verify it:

cs-fv verify Calculator.cs
# ✅ Calculator.Add verified (0.3s)

---

Documentation

Document	Description
FEATURES.md	Complete feature matrix with C# 13/14 support, requirement traceability, and test coverage
USAGE.md	Comprehensive usage guide with CLI reference, contract syntax, and examples
OUTPUT-REFERENCE.md	Verification result formats, diagnostic messages, and exit codes
.planning/ROADMAP.md	Detailed phase-by-phase project roadmap
examples/	Sample C# files with contracts

---

Feature Highlights

✅ C# Language Support (C# 11-14)

Version	Support	Features	Tests	Status
C# 11	Full	Record types, init-only properties, required keyword	150 tests	✅ Complete
C# 12	Full	Primary constructors, collection expressions	612 tests	✅ Complete
C# 13	Full	Params collections, partial properties, ref structs	90 tests	✅ Complete
C# 14	Full	Field keyword, extension members, array views	60 tests	✅ Complete

C# 13 Features:

• params collections (Span<T>, ReadOnlySpan<T>)
• Partial properties and indexers
• From-the-end index (^) in object initializers
• ref struct interfaces
• ref struct as generic type parameters
• \e escape sequence

C# 14 Features:

• Extension members detection
• field keyword (backing field access)
• Unbound generic types in nameof()
• C# 14 overload resolution rules
• CollectionEncoder (array views)
• ReadOnlySpan<T> immutability
• Span lifetime tracking
• Array-to-span conversion safety

✅ Advanced Language Features (v2.0.0)

• Control Flow Graph Foundation - CFG analysis for nullability and async flows
• Nullability Flow Analysis - Flow-sensitive null safety verification
• Lambda Expressions - Closures with ref/scoped/in/out modifiers
• Async/Await Patterns - Task<T> state machine encoding
• LINQ Query Expressions - Deferred execution modeling
• Dynamic Binding - Conservative approximation with precision warnings
• Parameter Modifiers & Generics - ref/in/out/scoped + generic variance

✅ Advanced Async Patterns (v3.0)

• ValueTask<T> - Allocation-free async with anti-pattern detection
• IAsyncEnumerable<T> - Async iterators with yield return, resource cleanup
• CancellationToken - Linked tokens, timeout cancellation, composition
• System.Threading.Channels - Bounded/unbounded channels, deadlock detection, FIFO ordering

✅ Classic C# Features (v6.0 - In Progress)

Completed:

• ✅ Enums - Simple and flag enums with exhaustiveness checking (Phase 34, 91 tests)

In Progress:

• 🚧 Delegates - Single-target and multicast delegates (Phase 35)
• 🚧 Events - Event declarations and event handling (Phase 36)
• 🚧 Synchronous Iterators - yield return in non-async methods (Phase 37)
• 🚧 Anonymous Types - Anonymous object creation and LINQ projections (Phase 38)

Note: v6.0 completes classic C# 1.0-3.0 language features that were missing from the modern-first approach (v1.0-v5.0). See the ROADMAP for detailed phase information.

---

Architecture

┌──────────────────────────┐
│  C# Source Code          │
│  + [Contract Attributes] │
└────────────┬─────────────┘
             │
             ▼
┌──────────────────────────┐
│  Roslyn Parser           │
│  + Semantic Model        │
│  + Control Flow Graph    │
└────────────┬─────────────┘
             │
             ▼
┌──────────────────────────┐
│  Feature Analyzers       │
│  - Async/Await           │
│  - LINQ                  │
│  - Channels              │
│  - Nullability Flow      │
└────────────┬─────────────┘
             │
             ▼
┌──────────────────────────┐
│  SMT-LIB2 Generator      │
│  - OO semantics encoding │
│  - State machine models  │
└────────────┬─────────────┘
             │
             ▼
┌──────────────────────────┐
│  CVC5 SMT Solver         │
│  (+ Z3 in Phase 17)      │
└────────────┬─────────────┘
             │
             ▼
┌──────────────────────────┐
│  Verification Results    │
│  + CLI Diagnostics       │
└──────────────────────────┘

---

CLI Commands

verify - Formal verification

cs-fv verify <file> [options]

Options:
  --method <name>       Verify only specified method
  --verbose             Show detailed SMT output
  --timeout <seconds>   CVC5 timeout (default: 30)
  --cvc5-path <path>    Path to CVC5 executable

check - Contract syntax check

cs-fv check <path> [options]

Options:
  --verbose             Show all warnings

Checks contract syntax without verification. Fast linting for contract attributes.

init - Initialize configuration

cs-fv init [options]

Options:
  --force               Overwrite existing config
  --verbose             Show generated configuration

Creates .cs-fv.json configuration file with defaults.

version - Version information

cs-fv version

Shows CS-FV version, components, and requirements.

See USAGE.md for detailed command reference and examples.

---

Project Status

Milestones

Milestone	Status	Phases	Requirements	Tests	Shipped
v1.0.0 - C# 14 Modernization	✅ Complete	0-5	40/40	762	2026-02-01
v2.0.0 - Full C# Language Spec	✅ Complete	6-13	70/70	1,639	2026-02-04
v3.0 - Async Patterns & Production	✅ Complete	14-16	33/33	1,355	2026-02-08
v4.0 - Enterprise & Optimization	✅ Complete	17-20	40/40	1,950	2026-02-09
v5.0 - Production Release	✅ Complete	21-33	45/45	2,100+	2026-02-10

Current Version Status

v5.0 Production Release - Complete and shipped as of 2026-02-10

All 33 planned phases (0-33) have been completed:

• ✅ Phases 0-5: C# 14 Modernization and foundational features
• ✅ Phases 6-13: Full C# language specification coverage
• ✅ Phases 14-16: Advanced async pattern support
• ✅ Phases 17-20: Enterprise features and multi-solver integration
• ✅ Phases 21-33: Production optimization, E2E testing, and performance benchmarking

Test Coverage: 2,100+ tests across unit, integration, performance, and E2E categories Requirements Met: 100% (all 45 v5.0 requirements satisfied)

---

Requirements

Dependencies

• .NET SDK 8.0+ (Required)
• Roslyn 5.0.0+ with C# 14 support (Included)
• CVC5 1.0.0+ (Required, SMT solver)
• Z3 4.12.2+ (Optional, Phase 17+)

Installation

See Quick Start above for full installation instructions (NuGet, source build, prerequisites).

---

Examples

The examples/ directory contains sample C# files with contracts:

• GettingStarted.cs - Basic calculator with simple contracts
• BinarySearch.cs - Array bounds safety and search correctness
• Stack.cs - Generic stack with class invariants
• SimpleCalculator.cs - Multiple methods with preconditions/postconditions

Try it:

cs-fv verify examples/GettingStarted.cs

---

Contract Syntax

Supported Attributes

using CsFv.Contracts;

[Requires("precondition")]     // Method precondition
[Ensures("postcondition")]      // Method postcondition
[Invariant("class-invariant")]  // Class invariant

Expression Syntax

Operators:

• Arithmetic: +, -, *, /, %
• Comparison: <, <=, >, >=, ==, !=
• Logical: &&, ||, !, =>
• Special: result (return value in [Ensures])

Example:

[Requires("x > 0 && y > 0")]
[Ensures("result > 0")]
[Ensures("result >= x && result >= y")]
public int Add(int x, int y) { return x + y; }

See USAGE.md for complete syntax reference and best practices.

---

Performance

CS-FV maintains excellent performance across all milestones:

Milestone	Test Count	Pass Rate	Performance	Regressions
v1.0.0	762	100%	0.04x-0.24x	0
v2.0.0	1,639	100%	<1x baseline	0
v3.0	1,355	100%	<1x baseline	0
v4.0	1,950	100%	<1x baseline	0
v5.0 (current)	2,100+	100%	<1x baseline	0

Target: ❤️x baseline compilation time Achieved: Actual verification faster than baseline (0.5x-0.8x)

---

Testing

CS-FV has comprehensive test coverage:

• Unit Tests: ~80% of total (individual components)
• Integration Tests: ~15% (end-to-end verification workflows)
• Performance Tests: ~3% (threshold validation)
• Requirement Traceability: ~2% (explicit requirement validation)

Test Organization:

tests/
├── CSharp12/           # C# 12 baseline (207 test files)
├── CSharp13/           # C# 13 features (15 test files)
├── CSharp14/           # C# 14 features (12 test files)
└── CsFv.*.Tests/       # Component tests

Run Tests:

dotnet test

---

Contributing

Current Status: Active development (v3.0 milestone)

Development Guidelines

• TDD: Test-first development (write failing test, implement, refactor)
• Type Safety: Strongly-typed code, no any types
• SOLID Principles: Single Responsibility, Open/Closed, Liskov Substitution, etc.
• Zero Regressions: All existing tests must pass before merging

See CLAUDE.md for detailed development guidelines.

Building from Source

git clone https://github.com/hapyy/cs-fv.git
cd cs-fv
dotnet restore
dotnet build
dotnet test

---

Research Background

CS-FV chose Roslyn→CVC5 direct verification over C# → C + ACSL transpilation to preserve object-oriented semantics:

Dimension	Roslyn→CVC5 (Chosen)	ACSL-Frama-C
OO Semantics	✅ Full preservation	❌ Lost in C transpilation
C# Features	✅ All (generics, LINQ, async)	⚠️ Subset only
IDE Integration	✅ Real-time feedback	❌ Offline tool
Developer UX	✅ C# attributes	⚠️ ACSL comments

Research Documents:

• research/ROSLYN-CVC5-FEASIBILITY.md - Feasibility analysis
• research/RESEARCH-003-SUMMARY.md - ACSL-Frama-C validation (comparison baseline)
• research/OO-SMT-ENCODING-PATTERNS.md - OO→SMT encoding patterns

---

Version History

v5.0 (Current - Production):

• All 33 phases complete (0-33)
• 2,100+ comprehensive tests
• Enterprise-ready with multi-solver support (CVC5 + Z3)
• Enhanced diagnostics and performance optimizations
• E2E workflows and production benchmarks

See .planning/ROADMAP.md for detailed phase breakdown and historical timeline.

---

License

CS-FV is dual-licensed:

• Non-commercial (free): CC BY-NC-ND 4.0 — personal, academic, research, and non-profit use. See LICENSE.
• Commercial (paid): Contact sales@hupyy.com for a commercial license. See COMMERCIAL-LICENSE.md.

Copyright (c) 2026 Alex Fedin @ Hupyy, Inc.

---

References

Tools & Technologies

• Roslyn - C# compiler platform
• CVC5 - SMT solver
• Z3 - Alternative SMT solver (Phase 17+)

Related Projects

• Code Contracts - Microsoft's C# contract system (deprecated)
• Dafny - Verification-aware language
• Boogie - Intermediate verification language

---

Support

• Documentation: See FEATURES.md, USAGE.md, OUTPUT-REFERENCE.md
• Issues: https://github.com/hapyy/cs-fv/issues
• Examples: See examples/ directory

---

Last Updated: 2026-02-10 Status: v5.0 shipped (All 33 phases complete, 100% of requirements satisfied) Maintenance Mode: Stability, optimization, and community support