1  ---
   2  Name: "FerrisProof: Multi-Layer Correctness Pipeline"
   3  Type: Technical Specification Document
   4  Status: Draft
   5  Date: 2025-12-31
   6  ---
   7  
   8  # FerrisProof: Multi-Layer Correctness Pipeline
   9  
  10  ## Overview
  11  
  12  FerrisProof is a comprehensive correctness pipeline for Rust applications that combines formal modeling, type-level verification, and property-based testing. The system operates through four progressive verification layers, each targeting different classes of errors with configurable enforcement levels and gradual adoption paths.
  13  
  14  The architecture follows a layered approach where each layer builds upon the previous one:
  15  - **Layer 1**: Formal Specification (TLA+/Alloy) for protocol-level correctness
  16  - **Layer 2**: Type-Level Verification (session types, refinement types) for compile-time guarantees  
  17  - **Layer 3**: Property-Based Testing for runtime invariant verification
  18  - **Layer 4**: Production Monitoring for observability and runtime assertions
  19  
  20  ## Architecture
  21  
  22  ### System Architecture Overview
  23  
  24  ```mermaid
  25  graph TB
  26      subgraph "FerrisProof Core"
  27          CM[Configuration Manager]
  28          VE[Verification Engine]
  29          CLI[CLI Tool]
  30          PM[Plugin Manager]
  31      end
  32      
  33      subgraph "Verification Layers"
  34          L1[Layer 1: Formal Specs<br/>TLA+/Alloy]
  35          L2[Layer 2: Type-Level<br/>Session/Refinement Types]
  36          L3[Layer 3: Property-Based<br/>Testing]
  37          L4[Layer 4: Production<br/>Monitoring]
  38      end
  39      
  40      subgraph "External Tools"
  41          TLA[TLA+ TLC]
  42          ALLOY[Alloy Analyzer]
  43          PROP[Proptest/Bolero]
  44          KANI[Kani Verifier]
  45          LOOM[Loom]
  46      end
  47      
  48      subgraph "Configuration Sources"
  49          ROOT[ferrisproof.toml]
  50          MOD[Module Configs]
  51          ATTR[Attribute Macros]
  52      end
  53      
  54      CLI --> CM
  55      CM --> ROOT
  56      CM --> MOD
  57      CM --> ATTR
  58      
  59      VE --> L1
  60      VE --> L2
  61      VE --> L3
  62      VE --> L4
  63      
  64      L1 --> TLA
  65      L1 --> ALLOY
  66      L3 --> PROP
  67      L3 --> KANI
  68      L3 --> LOOM
  69      
  70      PM --> TLA
  71      PM --> ALLOY
  72      PM --> PROP
  73      PM --> KANI
  74      PM --> LOOM
  75  ```
  76  
  77  ### Configuration Hierarchy
  78  
  79  ```mermaid
  80  graph TD
  81      ROOT[Root Config<br/>ferrisproof.toml]
  82      
  83      subgraph "Module Overrides"
  84          CRYPTO[crypto/*<br/>level: formal]
  85          API[api/*<br/>level: standard]
  86          UTILS[utils/*<br/>level: minimal]
  87      end
  88      
  89      subgraph "Item Attributes"
  90          FUNC[#[verification(level="strict")]<br/>Function Level]
  91          MOD[#[verification(spec="raft.tla")]<br/>Module Level]
  92      end
  93      
  94      ROOT --> CRYPTO
  95      ROOT --> API
  96      ROOT --> UTILS
  97      
  98      CRYPTO --> FUNC
  99      API --> MOD
 100  ```
 101  
 102  ## Interaction Patterns and Workflows
 103  
 104  ### Workflow 1: Project Initialization
 105  
 106  ```mermaid
 107  sequenceDiagram
 108      participant U as User
 109      participant CLI as CLI Tool
 110      participant CM as Config Manager
 111      participant SV as Schema Validator
 112      participant FS as File System
 113  
 114      U->>CLI: ferris-proof init --level standard
 115      CLI->>CLI: Parse arguments
 116      CLI->>CM: create_default_config(level=standard)
 117      CM->>SV: validate_schema(config)
 118      SV-->>CM: ValidationResult::Ok
 119      CM->>FS: write ferrisproof.toml
 120      FS-->>CM: Success
 121      CM->>FS: create specs/ directory
 122      CM->>FS: create templates
 123      CLI-->>U: ✓ Project initialized
 124  ```
 125  
 126  ### Workflow 2: Verification Execution with Caching
 127  
 128  ```mermaid
 129  sequenceDiagram
 130      participant CLI as CLI Tool
 131      participant VE as Verification Engine
 132      participant Cache as Verification Cache
 133      participant CM as Config Manager
 134      participant PM as Plugin Manager
 135      participant TLA as TLA+ TLC
 136  
 137      CLI->>VE: verify(targets)
 138      VE->>CM: for_file(target.path)
 139      CM-->>VE: EffectiveConfig
 140      
 141      VE->>Cache: get(target, config_hash)
 142      alt Cache Hit
 143          Cache-->>VE: CachedResult
 144          VE-->>CLI: VerificationResult (cached)
 145      else Cache Miss
 146          VE->>PM: plugins_for_technique(FormalSpecs)
 147          PM-->>VE: [TLA+ Plugin]
 148          VE->>TLA: verify(spec.tla)
 149          TLA-->>VE: ModelCheckResult
 150          VE->>Cache: store(target, result)
 151          VE-->>CLI: VerificationResult (fresh)
 152      end
 153  ```
 154  
 155  ### Workflow 3: Configuration Discovery and Merging
 156  
 157  ```mermaid
 158  sequenceDiagram
 159      participant VE as Verification Engine
 160      participant CM as Config Manager
 161      participant FS as File System
 162  
 163      VE->>CM: for_file("src/consensus/raft.rs")
 164      
 165      CM->>FS: read("ferrisproof.toml")
 166      FS-->>CM: root_config
 167      
 168      CM->>FS: walk("src/")
 169      FS-->>CM: ["src/ferrisproof.toml", "src/consensus/ferrisproof.toml"]
 170      
 171      CM->>CM: merge(root_config, src_config)
 172      CM->>CM: merge(merged, consensus_config)
 173      
 174      CM->>CM: apply_glob_patterns("consensus::*")
 175      CM->>CM: check_attribute_overrides(raft.rs)
 176      
 177      CM-->>VE: EffectiveConfig { level: Formal, ... }
 178  ```
 179  
 180  ### Diagram Notation
 181  - **Solid arrows (→)**: Direct function calls or synchronous communication
 182  - **Dashed arrows (-->)**: Return values or responses
 183  - **Thick arrows (==>)**: Data flow or configuration propagation
 184  - **Subgraphs**: Logical component groupings or deployment boundaries
 185  - **Colors**:
 186    - Blue: Core FerrisProof components
 187    - Green: External verification tools
 188    - Yellow: Configuration sources
 189    - Gray: File system or external resources
 190  
 191  ## Configuration Resolution Algorithm
 192  
 193  ### Precedence Rules
 194  
 195  Configuration resolution follows a **hierarchical merge strategy** with the following precedence (highest to lowest):
 196  
 197  1. **Item-level attributes** (`#[verification(...)]`)
 198  2. **Module-level glob patterns** (most specific path match)
 199  3. **Module configuration files** (nearest ancestor directory)
 200  4. **Root configuration** (`ferrisproof.toml` at project root)
 201  
 202  ### Merging Algorithm
 203  
 204  ```rust
 205  impl ConfigManager {
 206      /// Resolve effective configuration for a file
 207      fn resolve_config(&self, file_path: &Path) -> EffectiveConfig {
 208          let mut config = self.root_config.clone();
 209          
 210          // 1. Apply ancestor module configs (bottom-up)
 211          for ancestor_config in self.find_ancestor_configs(file_path) {
 212              config = self.merge(config, ancestor_config);
 213          }
 214          
 215          // 2. Apply glob pattern matches (most specific first)
 216          let module_path = self.file_to_module_path(file_path);
 217          let matching_patterns = self.find_matching_patterns(&module_path);
 218          
 219          // Sort by specificity (longest path = most specific)
 220          let sorted_patterns = matching_patterns
 221              .sort_by_key(|p| p.path_components().len())
 222              .rev();
 223          
 224          for pattern_config in sorted_patterns {
 225              config = self.merge(config, pattern_config);
 226          }
 227          
 228          // 3. Apply item-level attributes (parsed from AST)
 229          if let Some(attr_config) = self.parse_item_attributes(file_path) {
 230              config = self.merge(config, attr_config);
 231          }
 232          
 233          config.into()
 234      }
 235      
 236      /// Merge two configurations (override takes precedence)
 237      fn merge(&self, base: Config, override_config: Config) -> Config {
 238          Config {
 239              level: override_config.level.or(base.level),
 240              enforcement: override_config.enforcement.or(base.enforcement),
 241              enabled_techniques: self.merge_techniques(
 242                  base.enabled_techniques, 
 243                  override_config.enabled_techniques
 244              ),
 245              tool_config: self.merge_tool_config(
 246                  base.tool_config, 
 247                  override_config.tool_config
 248              ),
 249              // ... other fields
 250          }
 251      }
 252  }
 253  ```
 254  
 255  ### Glob Pattern Specificity
 256  
 257  Specificity is determined by:
 258  - **Path depth**: `consensus::raft::*` > `consensus::*`
 259  - **Wildcard type**: Exact match > single wildcard (*) > double wildcard (**)
 260  - **Declaration order**: Later declarations win for equal specificity
 261  
 262  ## Verification Cache Design
 263  
 264  ### Cache Key Generation
 265  
 266  ```rust
 267  #[derive(Debug, Clone, Hash, Eq, PartialEq)]
 268  pub struct CacheKey {
 269      /// Content hash of verification target
 270      content_hash: ContentHash,
 271      
 272      /// Hash of effective configuration
 273      config_hash: ConfigHash,
 274      
 275      /// Version of FerrisProof and external tools
 276      tool_versions: ToolVersions,
 277      
 278      /// Verification layer
 279      layer: Layer,
 280  }
 281  
 282  impl CacheKey {
 283      fn compute_content_hash(target: &Target) -> ContentHash {
 284          // For Rust files: hash AST (ignore whitespace/comments)
 285          // For formal specs: hash normalized specification
 286          let mut hasher = Blake3::new();
 287          
 288          match target {
 289              Target::RustFile(path) => {
 290                  let ast = syn::parse_file(&fs::read_to_string(path)?)?;
 291                  let normalized = self.normalize_ast(&ast);
 292                  hasher.update(&normalized);
 293              }
 294              Target::FormalSpec(path) => {
 295                  let spec = fs::read_to_string(path)?;
 296                  let normalized = self.normalize_spec(&spec);
 297                  hasher.update(&normalized);
 298              }
 299          }
 300          
 301          ContentHash(hasher.finalize())
 302      }
 303  }
 304  ```
 305  
 306  ### Cache Invalidation Strategy
 307  
 308  Cache entries are invalidated when:
 309  - **Content changes**: File modification detected via content hash mismatch
 310  - **Configuration changes**: Effective config hash differs
 311  - **Tool version changes**: External tool upgraded/downgraded
 312  - **Dependency changes**: Transitive dependencies modified
 313  - **Manual invalidation**: User runs `ferris-proof clean --cache`
 314  - **Age threshold**: Entries older than 30 days (configurable)
 315  
 316  ## Components and Interfaces
 317  
 318  ### Configuration Manager
 319  
 320  The Configuration Manager handles hierarchical configuration resolution and caching.
 321  
 322  ```rust
 323  pub struct ConfigManager {
 324      root_config: Config,
 325      module_overrides: HashMap<PathBuf, Config>,
 326      cache: ConfigCache,
 327      schema_validator: SchemaValidator,
 328  }
 329  
 330  impl ConfigManager {
 331      /// Load configuration from project root with validation
 332      pub fn from_project_root(root: &Path) -> Result<Self, ConfigError>;
 333      
 334      /// Get effective configuration for a specific file
 335      pub fn for_file(&self, file_path: &Path) -> EffectiveConfig;
 336      
 337      /// Validate configuration against schema
 338      pub fn validate(&self) -> Result<(), Vec<ValidationError>>;
 339      
 340      /// Merge configurations with precedence rules
 341      fn merge_configs(&self, base: Config, overrides: &[Config]) -> Config;
 342  }
 343  
 344  #[derive(Debug, Clone)]
 345  pub struct EffectiveConfig {
 346      pub level: VerificationLevel,
 347      pub enforcement: EnforcementMode,
 348      pub enabled_techniques: Vec<Technique>,
 349      pub tool_config: ToolConfig,
 350      pub thresholds: Thresholds,
 351  }
 352  ```
 353  
 354  ### Verification Engine
 355  
 356  The core engine orchestrates verification across all layers.
 357  
 358  ```rust
 359  pub struct VerificationEngine {
 360      config_manager: ConfigManager,
 361      plugin_manager: PluginManager,
 362      cache: VerificationCache,
 363      metrics: MetricsCollector,
 364  }
 365  
 366  impl VerificationEngine {
 367      /// Run verification for specified targets
 368      pub async fn verify(&self, targets: &[Target]) -> VerificationResult;
 369      
 370      /// Run specific verification layer
 371      pub async fn verify_layer(&self, layer: Layer, target: &Target) -> LayerResult;
 372      
 373      /// Check if verification is required (cache validation)
 374      pub fn needs_verification(&self, target: &Target) -> bool;
 375      
 376      /// Generate verification artifacts
 377      pub fn generate_artifacts(&self, target: &Target) -> Result<Vec<Artifact>, Error>;
 378  }
 379  
 380  #[derive(Debug)]
 381  pub struct VerificationResult {
 382      pub overall_status: Status,
 383      pub layer_results: HashMap<Layer, LayerResult>,
 384      pub metrics: VerificationMetrics,
 385      pub artifacts: Vec<Artifact>,
 386  }
 387  ```
 388  
 389  ### Plugin Manager
 390  
 391  Manages external tool integration with version compatibility checking.
 392  
 393  ```rust
 394  pub struct PluginManager {
 395      plugins: HashMap<ToolName, Box<dyn VerificationPlugin>>,
 396      tool_registry: ToolRegistry,
 397      version_checker: VersionChecker,
 398  }
 399  
 400  pub trait VerificationPlugin: Send + Sync {
 401      fn name(&self) -> &str;
 402      fn supported_versions(&self) -> VersionRange;
 403      fn check_availability(&self) -> Result<ToolInfo, ToolError>;
 404      fn verify(&self, input: VerificationInput) -> Result<VerificationOutput, ToolError>;
 405      fn parse_output(&self, raw_output: &str) -> Result<StructuredResult, ParseError>;
 406  }
 407  
 408  impl PluginManager {
 409      /// Register a verification plugin
 410      pub fn register_plugin(&mut self, plugin: Box<dyn VerificationPlugin>);
 411      
 412      /// Get available plugins for a technique
 413      pub fn plugins_for_technique(&self, technique: Technique) -> Vec<&dyn VerificationPlugin>;
 414      
 415      /// Validate tool versions and availability
 416      pub fn validate_tools(&self) -> Result<(), Vec<ToolError>>;
 417  }
 418  ```
 419  
 420  ### CLI Interface
 421  
 422  Command-line interface with comprehensive subcommands and user experience features.
 423  
 424  ```rust
 425  #[derive(Parser)]
 426  #[command(name = "ferris-proof")]
 427  pub struct Cli {
 428      #[command(subcommand)]
 429      pub command: Commands,
 430      
 431      #[arg(long, global = true)]
 432      pub config: Option<PathBuf>,
 433      
 434      #[arg(long, global = true)]
 435      pub verbose: bool,
 436      
 437      #[arg(long, global = true)]
 438      pub output_format: Option<OutputFormat>,
 439  }
 440  
 441  #[derive(Subcommand)]
 442  pub enum Commands {
 443      /// Initialize project with verification configuration
 444      Init {
 445          #[arg(long, default_value = "standard")]
 446          level: VerificationLevel,
 447          #[arg(long)]
 448          interactive: bool,
 449          #[arg(long)]
 450          template: Option<String>,
 451      },
 452      
 453      /// Run verification checks
 454      Check {
 455          #[arg(long)]
 456          module: Option<String>,
 457          #[arg(long)]
 458          layer: Option<Layer>,
 459          #[arg(long)]
 460          fix: bool,
 461      },
 462      
 463      /// Show effective configuration
 464      Config {
 465          #[arg(long)]
 466          file: Option<PathBuf>,
 467          #[arg(long)]
 468          validate: bool,
 469      },
 470      
 471      /// Upgrade verification level
 472      Upgrade {
 473          #[arg(long)]
 474          to: VerificationLevel,
 475          #[arg(long)]
 476          dry_run: bool,
 477          #[arg(long)]
 478          interactive: bool,
 479      },
 480      
 481      /// Generate verification artifacts
 482      Generate {
 483          #[arg(long)]
 484          target: GenerateTarget,
 485          #[arg(long)]
 486          output_dir: Option<PathBuf>,
 487      },
 488      
 489      /// Explain error codes and provide guidance
 490      Explain {
 491          error_code: String,
 492      },
 493  }
 494  ```
 495  
 496  ## Data Models
 497  
 498  ### Configuration Schema
 499  
 500  ```rust
 501  #[derive(Debug, Clone, Serialize, Deserialize)]
 502  pub struct Config {
 503      pub profile: ProfileConfig,
 504      pub tools: ToolConfig,
 505      pub modules: HashMap<String, ModuleConfig>,
 506      pub features: FeatureConfig,
 507      pub thresholds: Thresholds,
 508      pub ci: CiConfig,
 509  }
 510  
 511  #[derive(Debug, Clone, Serialize, Deserialize)]
 512  pub struct ProfileConfig {
 513      pub level: VerificationLevel,
 514      pub enforcement: EnforcementMode,
 515      pub enabled_techniques: Vec<Technique>,
 516  }
 517  
 518  #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)]
 519  pub enum VerificationLevel {
 520      Minimal,    // Type safety only
 521      Standard,   // + Property-based testing
 522      Strict,     // + Session types, refinement types, concurrency testing
 523      Formal,     // + Formal specifications
 524  }
 525  
 526  #[derive(Debug, Clone, Copy)]
 527  pub enum EnforcementMode {
 528      Advisory,   // Log violations, don't fail builds
 529      Warning,    // Emit compiler warnings
 530      Error,      // Fail compilation/tests
 531  }
 532  
 533  #[derive(Debug, Clone)]
 534  pub enum Technique {
 535      TypeSafety,
 536      PropertyTests,
 537      SessionTypes,
 538      RefinementTypes,
 539      ConcurrencyTesting,
 540      FormalSpecs,
 541      ModelChecking,
 542  }
 543  ```
 544  
 545  ### Verification Results
 546  
 547  ```rust
 548  #[derive(Debug, Clone, Serialize, Deserialize)]
 549  pub struct VerificationReport {
 550      pub metadata: ReportMetadata,
 551      pub summary: VerificationSummary,
 552      pub layer_results: HashMap<Layer, LayerResult>,
 553      pub violations: Vec<Violation>,
 554      pub metrics: VerificationMetrics,
 555      pub recommendations: Vec<Recommendation>,
 556  }
 557  
 558  #[derive(Debug, Clone)]
 559  pub struct ReportMetadata {
 560      pub timestamp: DateTime<Utc>,
 561      pub ferris_proof_version: String,
 562      pub git_commit: Option<String>,
 563      pub config_snapshot: Config,
 564      pub platform_info: PlatformInfo,
 565  }
 566  
 567  #[derive(Debug, Clone)]
 568  pub struct Violation {
 569      pub id: String,
 570      pub severity: Severity,
 571      pub location: Location,
 572      pub message: String,
 573      pub suggestion: Option<String>,
 574      pub rule: String,
 575  }
 576  
 577  #[derive(Debug, Clone)]
 578  pub enum Severity {
 579      Error,
 580      Warning,
 581      Info,
 582  }
 583  ```
 584  
 585  ### Formal Specification Integration
 586  
 587  ```rust
 588  #[derive(Debug, Clone)]
 589  pub struct FormalSpec {
 590      pub path: PathBuf,
 591      pub language: SpecLanguage,
 592      pub invariants: Vec<String>,
 593      pub temporal_properties: Vec<String>,
 594      pub linked_modules: Vec<String>,
 595  }
 596  
 597  #[derive(Debug, Clone, Copy)]
 598  pub enum SpecLanguage {
 599      TLAPlus,
 600      Alloy,
 601      EventB,
 602      MCRL2,
 603  }
 604  
 605  pub struct SpecificationBinding {
 606      pub spec: FormalSpec,
 607      pub rust_bindings: Vec<TypeBinding>,
 608      pub property_links: Vec<PropertyLink>,
 609  }
 610  
 611  #[derive(Debug, Clone)]
 612  pub struct TypeBinding {
 613      pub spec_type: String,
 614      pub rust_type: TokenStream,
 615      pub invariants: Vec<String>,
 616  }
 617  ```
 618  
 619  ## Correctness Properties
 620  
 621  *A property is a characteristic or behavior that should hold true across all valid executions of a system—essentially, a formal statement about what the system should do. Properties serve as the bridge between human-readable specifications and machine-verifiable correctness guarantees.*
 622  
 623  <function_calls>
 624  <invoke name="prework">
 625  <parameter name="featureName">ferris-proof
 626  
 627  ### Property Reflection
 628  
 629  After analyzing the acceptance criteria, several properties can be consolidated to avoid redundancy:
 630  
 631  - **Configuration Level Properties (2.2-2.5)**: These can be combined into a single comprehensive property that tests all verification levels
 632  - **Tool Integration Properties (3.1, 3.2, 5.1)**: These are specific examples rather than universal properties
 633  - **Report Generation Properties (8.3, 15.3)**: These can be combined into a single property about multi-format output support
 634  
 635  ### Correctness Properties
 636  
 637  Property 1: Layer activation behavior
 638  *For any* verification configuration with specific layers enabled, the system should activate exactly the expected verification techniques for those layers
 639  **Validates: Requirements 1.2, 1.4, 1.5**
 640  
 641  Property 2: Configuration level enforcement
 642  *For any* verification level setting (minimal, standard, strict, formal), the system should enable exactly the techniques specified for that level and no others
 643  **Validates: Requirements 2.2, 2.3, 2.4, 2.5**
 644  
 645  Property 3: Configuration discovery and merging
 646  *For any* directory structure containing ferrisproof.toml files, the configuration manager should discover all files recursively and merge them with child configurations overriding parent configurations
 647  **Validates: Requirements 2.8, 2.9**
 648  
 649  Property 4: Formal specification processing
 650  *For any* valid formal specification file (TLA+ or Alloy), when formal verification is enabled, the system should invoke the appropriate model checker and generate corresponding Rust type scaffolding
 651  **Validates: Requirements 3.3, 3.4**
 652  
 653  Property 5: Property test linking
 654  *For any* property test definition with formal specification references, the system should establish and maintain links between the property tests and the corresponding specification invariants
 655  **Validates: Requirements 5.4**
 656  
 657  Property 6: CLI verification level initialization
 658  *For any* valid verification level specified during project initialization, the CLI should create a configuration that enables exactly the techniques for that level
 659  **Validates: Requirements 6.1**
 660  
 661  Property 7: Violation detection and reporting
 662  *For any* project with verification violations, the CLI should detect all violations and generate reports in all requested output formats (JSON, Markdown, HTML)
 663  **Validates: Requirements 6.3, 8.3, 15.3**
 664  
 665  Property 8: Exit code consistency
 666  *For any* verification execution scenario (success, verification failure, configuration error, tool unavailable), the system should return the appropriate standard exit code (0, 1, 2, 3 respectively)
 667  **Validates: Requirements 9.7**
 668  
 669  Property 9: Configuration validation
 670  *For any* configuration file with syntax or semantic errors, the configuration manager should reject the configuration and provide detailed error messages with suggested fixes
 671  **Validates: Requirements 10.1, 10.2**
 672  
 673  Property 10: Verification result caching
 674  *For any* verification target that has not changed since the last verification, the system should reuse cached results instead of re-running verification
 675  **Validates: Requirements 11.3**
 676  
 677  Property 11: Network isolation
 678  *For any* verification execution without explicit external service consent, the system should not initiate any network connections to external services
 679  **Validates: Requirements 12.1**
 680  
 681  ## Security Architecture
 682  
 683  ### Threat Model
 684  
 685  FerrisProof considers the following threats:
 686  
 687  1. **Malicious Formal Specifications**: User-provided TLA+/Alloy specs that attempt code execution
 688  2. **Supply Chain Attacks**: Compromised external tool binaries
 689  3. **Data Exfiltration**: Verification tools attempting to send code to external servers
 690  4. **Resource Exhaustion**: Specifications causing infinite loops or memory exhaustion
 691  5. **Path Traversal**: Configuration files attempting to read/write outside project directory
 692  6. **Code Injection**: User input in configuration parsed unsafely
 693  
 694  ### Mitigation Strategies
 695  
 696  ```rust
 697  /// Sandboxing for external tool execution
 698  pub struct SandboxedExecutor {
 699      /// Allowed file system access
 700      allowed_paths: Vec<PathBuf>,
 701      
 702      /// Network access policy
 703      network_policy: NetworkPolicy,
 704      
 705      /// Resource limits
 706      limits: ResourceLimits,
 707  }
 708  
 709  #[derive(Debug, Clone)]
 710  pub enum NetworkPolicy {
 711      /// No network access allowed
 712      Denied,
 713      
 714      /// Allow connections to specified hosts only
 715      AllowList(Vec<String>),
 716      
 717      /// Allow all connections (user explicitly opted in)
 718      Unrestricted { user_consent: Consent },
 719  }
 720  
 721  #[derive(Debug, Clone)]
 722  pub struct ResourceLimits {
 723      /// Maximum memory (bytes)
 724      pub max_memory: u64,
 725      
 726      /// Maximum CPU time (seconds)
 727      pub max_cpu_time: u64,
 728      
 729      /// Maximum open files
 730      pub max_file_descriptors: u32,
 731      
 732      /// Maximum child processes
 733      pub max_processes: u32,
 734  }
 735  ```
 736  
 737  ### Input Validation
 738  
 739  All user-provided inputs undergo strict validation:
 740  
 741  ```rust
 742  pub struct InputValidator;
 743  
 744  impl InputValidator {
 745      /// Validate configuration file paths
 746      pub fn validate_path(path: &Path, project_root: &Path) -> Result<(), ValidationError> {
 747          // Reject absolute paths outside project
 748          let canonical = path.canonicalize()?;
 749          if !canonical.starts_with(project_root) {
 750              return Err(ValidationError::PathTraversal {
 751                  attempted: path.to_owned(),
 752                  project_root: project_root.to_owned(),
 753              });
 754          }
 755          
 756          // Reject symlinks pointing outside project
 757          if path.is_symlink() {
 758              let target = fs::read_link(path)?;
 759              if !target.starts_with(project_root) {
 760                  return Err(ValidationError::SuspiciousSymlink);
 761              }
 762          }
 763          
 764          Ok(())
 765      }
 766      
 767      /// Validate glob patterns don't escape project
 768      pub fn validate_glob(pattern: &str) -> Result<(), ValidationError> {
 769          if pattern.contains("..") || pattern.starts_with("/") {
 770              return Err(ValidationError::UnsafeGlobPattern);
 771          }
 772          Ok(())
 773      }
 774  }
 775  ```
 776  
 777  ## Performance Benchmarks and Targets
 778  
 779  ### Reference Hardware
 780  
 781  **"Standard CI Runner"** is defined as:
 782  - **CPU**: 2 vCPUs @ 2.4 GHz (equivalent to GitHub Actions `ubuntu-latest`)
 783  - **RAM**: 7 GB available
 784  - **Disk**: SSD with 50 MB/s sustained write
 785  - **Network**: 100 Mbps (for tool downloads)
 786  
 787  ### Performance Targets
 788  
 789  | Verification Level | Project Size | Target Duration | P95 Duration | Memory Usage |
 790  |--------------------|--------------|-----------------|--------------|--------------|
 791  | Minimal            | <100k LOC    | <30s           | <60s         | <500 MB      |
 792  | Standard           | <100k LOC    | <5 min         | <10 min      | <2 GB        |
 793  | Strict             | <50k LOC     | <10 min        | <20 min      | <4 GB        |
 794  | Formal             | <10k LOC     | <30 min        | <60 min      | <8 GB        |
 795  
 796  ### Scalability Characteristics
 797  
 798  ```rust
 799  /// Expected time complexity for verification operations
 800  pub enum Complexity {
 801      /// O(n) where n = lines of code
 802      Linear,
 803      
 804      /// O(n log n) for indexed operations
 805      Logarithmic,
 806      
 807      /// O(n²) for model checking with state explosion
 808      Quadratic,
 809      
 810      /// Bounded by timeout, potentially exponential
 811      Bounded { max_time: Duration },
 812  }
 813  
 814  impl Layer {
 815      pub fn complexity(&self) -> Complexity {
 816          match self {
 817              Layer::TypeLevel => Complexity::Linear,
 818              Layer::PropertyBased => Complexity::Logarithmic,
 819              Layer::Formal => Complexity::Bounded { 
 820                  max_time: Duration::from_secs(600) 
 821              },
 822              Layer::Monitoring => Complexity::Linear,
 823          }
 824      }
 825  }
 826  ```
 827  
 828  ## Error Handling
 829  
 830  ### Error Classification
 831  
 832  FerrisProof implements a comprehensive error handling strategy with structured error types:
 833  
 834  ```rust
 835  #[derive(Debug, thiserror::Error)]
 836  pub enum FerrisProofError {
 837      #[error("Configuration error: {message}")]
 838      Configuration { 
 839          message: String, 
 840          location: Option<Location>,
 841          suggestions: Vec<String>,
 842      },
 843      
 844      #[error("Tool error: {tool} - {message}")]
 845      Tool { 
 846          tool: String, 
 847          message: String,
 848          exit_code: Option<i32>,
 849          stderr: Option<String>,
 850      },
 851      
 852      #[error("Verification failed: {violations} violation(s)")]
 853      Verification { 
 854          violations: Vec<Violation>,
 855          partial_results: Option<VerificationResult>,
 856      },
 857      
 858      #[error("IO error: {message}")]
 859      Io { 
 860          message: String, 
 861          path: Option<PathBuf>,
 862          #[source]
 863          source: std::io::Error,
 864      },
 865      
 866      #[error("Parse error: {message}")]
 867      Parse { 
 868          message: String,
 869          location: Location,
 870          expected: Option<String>,
 871      },
 872  }
 873  ```
 874  
 875  ### Error Recovery Strategies
 876  
 877  1. **Configuration Errors**: Provide detailed diagnostics with suggested fixes and configuration templates
 878  2. **Tool Unavailability**: Graceful degradation with alternative tools or reduced verification levels
 879  3. **Timeout Handling**: Partial result preservation and configurable timeout limits
 880  4. **Network Failures**: Offline mode with cached results and local-only verification
 881  5. **Resource Exhaustion**: Memory-bounded verification with progress checkpointing
 882  
 883  ### Logging and Observability
 884  
 885  ```rust
 886  pub struct Logger {
 887      level: LogLevel,
 888      format: LogFormat,
 889      outputs: Vec<LogOutput>,
 890  }
 891  
 892  #[derive(Debug, Clone)]
 893  pub enum LogLevel {
 894      Error,
 895      Warn, 
 896      Info,
 897      Debug,
 898      Trace,
 899  }
 900  
 901  #[derive(Debug, Clone)]
 902  pub enum LogFormat {
 903      Human,      // Colored, human-readable
 904      Json,       // Structured JSON for machine parsing
 905      Compact,    // Single-line format for CI
 906  }
 907  ```
 908  
 909  ### Error Code Catalog
 910  
 911  #### Error Code Format
 912  
 913  Error codes follow the pattern: `FP-<CATEGORY>-<NUMBER>`
 914  
 915  - **FP**: FerrisProof prefix
 916  - **CATEGORY**: 2-letter category code
 917  - **NUMBER**: 3-digit error number
 918  
 919  #### Categories
 920  
 921  - **CF**: Configuration errors (FP-CF-001 to FP-CF-999)
 922  - **VR**: Verification errors (FP-VR-001 to FP-VR-999)
 923  - **TL**: Tool errors (FP-TL-001 to FP-TL-999)
 924  - **IO**: I/O and file system errors (FP-IO-001 to FP-IO-999)
 925  - **PS**: Parse errors (FP-PS-001 to FP-PS-999)
 926  
 927  #### Common Error Codes
 928  
 929  | Code | Description | Suggested Fix |
 930  |------|-------------|---------------|
 931  | FP-CF-001 | Invalid verification level in configuration | Use one of: minimal, standard, strict, formal |
 932  | FP-CF-002 | Missing required configuration field | Add required field or use `ferris-proof init` |
 933  | FP-CF-003 | Conflicting module-level overrides | Remove duplicate glob patterns or use more specific paths |
 934  | FP-VR-001 | Property test failure | Review counterexample and fix implementation |
 935  | FP-VR-002 | Formal specification violation | Check TLA+ invariant against implementation |
 936  | FP-TL-001 | TLA+ TLC not found | Install TLA+ tools: `ferris-proof install tla` |
 937  | FP-TL-002 | Tool version incompatible | Upgrade/downgrade tool to supported version range |
 938  | FP-IO-001 | Cannot read specification file | Check file exists and has read permissions |
 939  
 940  ```rust
 941  impl FerrisProofError {
 942      pub fn code(&self) -> &str {
 943          match self {
 944              Self::Configuration { .. } => "FP-CF-001",
 945              Self::Tool { .. } => "FP-TL-001",
 946              Self::Verification { .. } => "FP-VR-001",
 947              // ...
 948          }
 949      }
 950      
 951      pub fn explanation(&self) -> String {
 952          match self.code() {
 953              "FP-CF-001" => include_str!("explanations/FP-CF-001.md").to_string(),
 954              "FP-VR-002" => include_str!("explanations/FP-VR-002.md").to_string(),
 955              // ...
 956              _ => format!("No detailed explanation available for error code {}", self.code()),
 957          }
 958      }
 959  }
 960  ```
 961  
 962  ## Property Test Implementation Examples
 963  
 964  ### Property 1: Layer Activation Behavior
 965  
 966  ```rust
 967  proptest! {
 968      #[test]
 969      /// **Feature: ferris-proof, Property 1: Layer activation behavior**
 970      fn layer_activation_matches_configuration(
 971          enabled_layers in prop::collection::hash_set(
 972              prop::sample::select(vec![Layer::Formal, Layer::TypeLevel, Layer::PropertyBased, Layer::Monitoring]),
 973              1..=4
 974          )
 975      ) {
 976          let mut config = Config::default();
 977          config.profile.enabled_techniques = enabled_layers
 978              .iter()
 979              .flat_map(|layer| layer.techniques())
 980              .collect();
 981          
 982          let engine = VerificationEngine::with_config(config.clone());
 983          
 984          for layer in &[Layer::Formal, Layer::TypeLevel, Layer::PropertyBased, Layer::Monitoring] {
 985              let expected_active = enabled_layers.contains(layer);
 986              let actually_active = engine.is_layer_active(layer);
 987              
 988              prop_assert_eq!(
 989                  expected_active, 
 990                  actually_active,
 991                  "Layer {:?} activation mismatch: expected {}, got {}",
 992                  layer, expected_active, actually_active
 993              );
 994          }
 995      }
 996  }
 997  ```
 998  
 999  ### Property 2: Configuration Level Enforcement
1000  
1001  ```rust
1002  proptest! {
1003      #[test]
1004      /// **Feature: ferris-proof, Property 2: Configuration level enforcement**
1005      fn verification_level_determines_techniques(
1006          level in any::<VerificationLevel>()
1007      ) {
1008          let config = Config {
1009              profile: ProfileConfig {
1010                  level,
1011                  enforcement: EnforcementMode::Error,
1012                  enabled_techniques: level.required_techniques(),
1013              },
1014              ..Default::default()
1015          };
1016          
1017          let expected_techniques: HashSet<_> = level.required_techniques().into_iter().collect();
1018          let actual_techniques: HashSet<_> = config.profile.enabled_techniques.iter().cloned().collect();
1019          
1020          prop_assert_eq!(
1021              expected_techniques,
1022              actual_techniques,
1023              "Level {:?} should enable exactly {:?}, but enabled {:?}",
1024              level, expected_techniques, actual_techniques
1025          );
1026          
1027          // Verify hierarchical inclusion
1028          if level >= VerificationLevel::Standard {
1029              prop_assert!(actual_techniques.contains(&Technique::PropertyTests));
1030          }
1031          if level >= VerificationLevel::Strict {
1032              prop_assert!(actual_techniques.contains(&Technique::SessionTypes));
1033          }
1034          if level >= VerificationLevel::Formal {
1035              prop_assert!(actual_techniques.contains(&Technique::FormalSpecs));
1036          }
1037      }
1038  }
1039  ```
1040  
1041  ### Property 10: Verification Result Caching
1042  
1043  ```rust
1044  proptest! {
1045      #[test]
1046      /// **Feature: ferris-proof, Property 10: Verification result caching**
1047      fn unchanged_targets_use_cache(
1048          content in arb_rust_code(),
1049          config in any::<Config>(),
1050      ) {
1051          let temp_dir = TempDir::new().unwrap();
1052          let file_path = temp_dir.path().join("test.rs");
1053          
1054          // Write initial content
1055          fs::write(&file_path, &content).unwrap();
1056          
1057          let engine = VerificationEngine::with_config(config);
1058          
1059          // First verification
1060          let start1 = Instant::now();
1061          let result1 = engine.verify(&[Target::RustFile(file_path.clone())]).unwrap();
1062          let duration1 = start1.elapsed();
1063          
1064          // Second verification (should use cache)
1065          let start2 = Instant::now();
1066          let result2 = engine.verify(&[Target::RustFile(file_path.clone())]).unwrap();
1067          let duration2 = start2.elapsed();
1068          
1069          // Results should be identical
1070          prop_assert_eq!(result1.overall_status, result2.overall_status);
1071          
1072          // Second run should be significantly faster (at least 50% faster)
1073          prop_assert!(
1074              duration2 < duration1 / 2,
1075              "Cached verification should be at least 50% faster: {:?} vs {:?}",
1076              duration1, duration2
1077          );
1078          
1079          // Cache hit should be recorded in metrics
1080          prop_assert!(result2.metrics.cache_hit);
1081      }
1082  }
1083  
1084  fn arb_rust_code() -> impl Strategy<Value = String> {
1085      // Generate valid Rust code snippets
1086      prop_oneof![
1087          Just("fn main() {}".to_string()),
1088          Just("struct Point { x: i32, y: i32 }".to_string()),
1089          // ... more variants
1090      ]
1091  }
1092  ```
1093  
1094  ## Testing Strategy
1095  
1096  ### Dual Testing Approach
1097  
1098  FerrisProof employs both unit testing and property-based testing for comprehensive coverage:
1099  
1100  **Unit Tests**:
1101  - Configuration parsing and validation logic
1102  - CLI command parsing and execution
1103  - Error message formatting and suggestions
1104  - Tool integration and version checking
1105  - Cache invalidation and cleanup
1106  
1107  **Property-Based Tests**:
1108  - Configuration merging across arbitrary directory structures
1109  - Verification result consistency across different input variations
1110  - Error handling robustness with malformed inputs
1111  - Performance characteristics under various load conditions
1112  - Security properties with adversarial inputs
1113  
1114  ### Property-Based Testing Configuration
1115  
1116  All property tests will use **proptest** as the primary PBT library with the following configuration:
1117  - **Minimum 100 iterations** per property test
1118  - **Maximum 10,000 shrinking iterations** for counterexample minimization
1119  - **Deterministic seeding** for reproducible CI builds
1120  - **Timeout limits** of 60 seconds per property test
1121  
1122  Each property test must include a comment tag referencing its design document property:
1123  ```rust
1124  proptest! {
1125      #[test]
1126      /// **Feature: ferris-proof, Property 2: Configuration level enforcement**
1127      fn test_verification_level_techniques(level in any::<VerificationLevel>()) {
1128          // Test implementation
1129      }
1130  }
1131  ```
1132  
1133  ### Integration Testing
1134  
1135  - **End-to-end CLI workflows** with temporary project directories
1136  - **Multi-tool integration** testing with Docker containers
1137  - **Performance regression** testing with benchmark suites
1138  - **Cross-platform compatibility** testing on Linux, macOS, and Windows
1139  - **Security testing** with isolated environments and network monitoring
1140  
1141  ### Self-Verification
1142  
1143  FerrisProof applies its own verification pipeline at the **formal level**:
1144  - Property-based tests for all configuration parsing logic
1145  - Formal specifications for critical algorithms (configuration merging, caching)
1146  - Session types for CLI command state machines
1147  - Comprehensive error injection testing
1148  - Supply chain security verification with SBOM generation
1149  
1150  The self-verification suite must maintain **minimum 80% code coverage** and complete within **10 minutes** on standard CI runners.
1151  ## Deployment and Distribution
1152  
1153  ### Package Formats
1154  
1155  FerrisProof is distributed via multiple channels:
1156  
1157  1. **crates.io**: Primary Rust package registry
1158     ```bash
1159     cargo install ferris-proof-cli
1160     ```
1161  
1162  2. **GitHub Releases**: Pre-built binaries for major platforms
1163     ```bash
1164     # Linux x86_64
1165     wget https://github.com/ferris-proof/releases/download/v0.1.0/ferris-proof-linux-x86_64.tar.gz
1166     
1167     # macOS (Apple Silicon)
1168     wget https://github.com/ferris-proof/releases/download/v0.1.0/ferris-proof-darwin-aarch64.tar.gz
1169     ```
1170  
1171  3. **Docker Images**: Containerized environment with all tools
1172     ```bash
1173     docker pull ferrisproof/ferris-proof:latest
1174     docker run -v $(pwd):/workspace ferrisproof/ferris-proof check --all
1175     ```
1176  
1177  4. **System Package Managers**:
1178     ```bash
1179     # Homebrew (macOS/Linux)
1180     brew install ferris-proof
1181     
1182     # APT (Debian/Ubuntu)
1183     apt install ferris-proof
1184     
1185     # DNF (Fedora/RHEL)
1186     dnf install ferris-proof
1187     ```
1188  
1189  ### Docker Image Variants
1190  
1191  ```dockerfile
1192  # Full image with all verification tools (~500 MB)
1193  FROM ferrisproof/ferris-proof:latest
1194  
1195  # Minimal image (Rust + basic tools, ~150 MB)
1196  FROM ferrisproof/ferris-proof:minimal
1197  
1198  # Specific verification level
1199  FROM ferrisproof/ferris-proof:standard
1200  FROM ferrisproof/ferris-proof:formal
1201  ```
1202  
1203  ### CI/CD Integration Templates
1204  
1205  #### GitHub Actions
1206  
1207  ```yaml
1208  # .github/workflows/ferris-proof.yml (generated by `ferris-proof init`)
1209  name: Verification
1210  on: [push, pull_request]
1211  
1212  jobs:
1213    verify:
1214      runs-on: ubuntu-latest
1215      container: ferrisproof/ferris-proof:latest
1216      steps:
1217        - uses: actions/checkout@v4
1218        - run: ferris-proof check --all
1219        - uses: actions/upload-artifact@v4
1220          if: always()
1221          with:
1222            name: verification-report
1223            path: target/ferris-proof-report.md
1224  ```
1225  
1226  #### GitLab CI
1227  
1228  ```yaml
1229  # .gitlab-ci.yml
1230  verify:
1231    image: ferrisproof/ferris-proof:latest
1232    script:
1233      - ferris-proof check --all
1234    artifacts:
1235      reports:
1236        junit: target/ferris-proof-junit.xml
1237      paths:
1238        - target/ferris-proof-report.md
1239  ```
1240  
1241  ### Version Management
1242  
1243  ```toml
1244  # ferrisproof.toml - Lock tool versions for reproducibility
1245  
1246  [tools.versions]
1247  ferris-proof = "0.1.0"
1248  tla-tools = "1.8.0"
1249  proptest = "1.4.0"
1250  kani = "0.56.0"
1251  
1252  [tools.lock]
1253  # Auto-generated lock file hash
1254  lock_hash = "sha256:abc123..."
1255  ```
1256  
1257  ## Architectural Decision Records (ADRs)
1258  
1259  ### ADR-001: Use TOML for Configuration
1260  
1261  **Context**: Need human-editable configuration format
1262  
1263  **Decision**: Use TOML instead of YAML or JSON
1264  
1265  **Rationale**:
1266  - Rust ecosystem standard (Cargo.toml)
1267  - Strict parsing (no YAML ambiguities)
1268  - Good error messages
1269  - Better for hierarchical data than JSON
1270  
1271  **Consequences**:
1272  - Limited to TOML expressiveness
1273  - Must provide schema validation
1274  - Easier for users familiar with Cargo
1275  
1276  ### ADR-002: Plugin ABI via abi_stable
1277  
1278  **Context**: Need cross-version plugin compatibility
1279  
1280  **Decision**: Use `abi_stable` crate for C-ABI interface
1281  
1282  **Rationale**:
1283  - Stable across Rust versions
1284  - Well-tested in production
1285  - Cross-language compatibility potential
1286  
1287  **Consequences**:
1288  - Extra abstraction layer
1289  - Performance overhead (minimal)
1290  - Requires FFI-safe types
1291  
1292  ### ADR-003: Content-Addressed Cache
1293  
1294  **Context**: Need reliable cache invalidation
1295  
1296  **Decision**: Use Blake3 content hashing for cache keys
1297  
1298  **Rationale**:
1299  - Cryptographically secure prevents collisions
1300  - Fast hashing performance (1+ GB/s)
1301  - Deduplication across projects
1302  
1303  **Consequences**:
1304  - Larger cache keys (32 bytes)
1305  - Requires AST normalization
1306  - Excellent cache hit rates
1307  
1308  ## Metrics Collection Design
1309  
1310  ```rust
1311  #[derive(Debug, Clone)]
1312  pub struct VerificationMetrics {
1313      pub total_duration: Duration,
1314      pub layer_durations: HashMap<Layer, Duration>,
1315      pub cache_hits: u32,
1316      pub cache_misses: u32,
1317      pub files_verified: u32,
1318      pub violations_found: u32,
1319      pub memory_peak_mb: u64,
1320      pub tool_invocations: HashMap<String, u32>,
1321  }
1322  
1323  impl MetricsCollector {
1324      pub fn record_event(&mut self, event: MetricEvent);
1325      pub fn export_prometheus(&self) -> String;
1326      pub fn export_json(&self) -> serde_json::Value;
1327  }
1328  ```
1329  
1330  ## CI Testing Matrix
1331  
1332  | Test Suite | Trigger | Duration | Platforms |
1333  |------------|---------|----------|-----------|
1334  | Unit Tests | Every commit | <2 min | Linux only |
1335  | Property Tests | Every commit | <5 min | Linux only |
1336  | Integration Tests | PR | <10 min | Linux, macOS, Windows |
1337  | Performance Regression | Nightly | <30 min | Linux |
1338  | Security Scan | Weekly | <10 min | Linux |
1339  | Cross-platform E2E | Release | <60 min | All platforms |