/ ReadMe.md
ReadMe.md
1 # FerrisProof 2 3 > **Rust. Verified. Proven.**: *Making Rust systems provably correct, one layer at a time.* 4 5 FerrisProof is a **full-stack correctness pipeline** for Rust applications, combining **formal modeling (TLA+, Alloy)**, **Rust's type system**, and **property-based testing** to ensure your systems are **memory-safe, structurally sound, and functionally correct**. 6 7 [](https://codecov.io/gh/yumin-chen/ferris-proof) 8 [](http://creativecommons.org/publicdomain/zero/1.0/) 9 10 > **🚧 Active Development**: FerrisProof is currently in active development. Core infrastructure and CLI tools are complete, with verification layers being progressively implemented. 11 12 Multi-layer correctness pipeline for Rust applications that combines formal modeling, type-level verification, and property-based testing to ensure systems are memory-safe, structurally sound, and functionally correct. 13 14 --- 15 16 ## Quick Start 17 18 ### Installation 19 20 ```bash 21 # Clone the repository 22 git clone https://github.com/yumin-chen/ferris-proof.git 23 cd ferris-proof 24 25 # Build and install the CLI tool 26 cargo install --path ferris-proof-cli 27 ``` 28 29 ### Initialise a New Project 30 31 ```bash 32 # Initialise with standard verification level 33 ferris-proof init --level standard 34 35 # Interactive initialization with prompts 36 ferris-proof init --interactive 37 38 # Initialise with formal verification level 39 ferris-proof init --level formal 40 ``` 41 42 ### Basic Commands 43 44 ```bash 45 # Show project configuration 46 ferris-proof config 47 48 # Validate configuration 49 ferris-proof config --validate 50 51 # Show configuration for specific file 52 ferris-proof config --file src/main.rs 53 54 # Explain error codes 55 ferris-proof explain FP-CF-001 56 57 # Get help 58 ferris-proof --help 59 ferris-proof init --help 60 61 # Cache management 62 ferris-proof cache info 63 ferris-proof cache health 64 ferris-proof cache cleanup 65 ferris-proof cache clear 66 ``` 67 68 --- 69 70 ## Features 71 72 - **🚀 Command-Line Interface**: Full-featured CLI with project initialization, configuration management, and error explanation 73 - **📊 Multi-Layer Verification**: Four progressive verification layers targeting different classes of errors 74 - **📝 Formal Specifications**: TLA+ and Alloy integration for protocol-level correctness 75 - **🔒 Type-Level Verification**: Session types and refinement types for compile-time guarantees 76 - **🧪 Property-Based Testing**: Comprehensive property testing with proptest integration 77 - **📈 Production Monitoring**: Runtime assertions and observability hooks 78 - **⬆️ Progressive Adoption**: Gradual verification level upgrades with automated scaffolding 79 - **🔄 CI/CD Integration**: GitHub Actions support with configurable enforcement modes 80 - **⚙️ Hierarchical Configuration**: Module-level and item-level verification overrides 81 - **💾 Comprehensive Caching**: Content-addressed verification result caching with Blake3 hashing, AST normalization, zstd compression, and management commands 82 - **🔐 Security-First**: Sandboxed execution and local-only verification options 83 84 --- 85 86 ## Architecture Overview 87 88 ### Multi-Layer Verification Architecture 89 90 ```mermaid 91 graph TB 92 %% Core FerrisProof Components 93 subgraph "FerrisProof Core" 94 CLI["CLI Tool"] 95 CM["Configuration Manager"] 96 VE["Verification Engine"] 97 Cache["Verification Cache"] 98 Metrics["Metrics Collector"] 99 PM["Plugin Manager"] 100 end 101 102 %% Verification Layers (DAG with Rust guarantees) 103 subgraph "Verification Layers" 104 L1["Layer 1: Formal Spec (TLA+/Alloy)"] 105 L2["Layer 2: Type-Level Verification (Session & Refinement Types)"] 106 L3["Layer 3: Property-Based Testing (Proptest/Kani/Bolero)"] 107 L4["Layer 4: Production Monitoring (Runtime Assertions, Metrics)"] 108 end 109 110 %% Rust Type Guarantees 111 subgraph "Rust-Specific Safety" 112 TS["Typestate & Linear Types"] 113 RT["Refinement Types"] 114 AST["AST Validation & Attribute Macros"] 115 end 116 117 %% Sandboxed External Tools 118 subgraph "External Tools (Sandboxed)" 119 TLA["TLA+ TLC"] 120 ALLOY["Alloy Analyzer"] 121 PROP["Proptest"] 122 KANI["Kani Verifier"] 123 LOOM["Loom Concurrency"] 124 end 125 126 %% CLI & Config Flow 127 CLI --> CM 128 CLI --> VE 129 CM --> VE 130 VE --> Cache 131 VE --> Metrics 132 VE --> PM 133 134 %% Layer Execution with Rust Guarantees 135 VE --> L1 136 L1 --> TS 137 L1 --> ALLOY 138 VE --> L2 139 L2 --> TS 140 L2 --> RT 141 VE --> L3 142 L3 --> AST 143 VE --> L4 144 145 %% Layer DAG Enforcement 146 L1 -->|success| L2 147 L2 -->|success| L3 148 L3 -->|success| L4 149 150 %% Plugin Manager & Sandbox 151 PM --> TLA 152 PM --> ALLOY 153 PM --> PROP 154 PM --> KANI 155 PM --> LOOM 156 157 TLA --> FS1["Filesystem: Restricted Paths"] 158 ALLOY --> FS1 159 PROP --> FS2["Filesystem: Restricted Paths"] 160 KANI --> FS2 161 LOOM --> FS2 162 163 TLA --> NET1["Network: Denied/Allowlist"] 164 ALLOY --> NET1 165 PROP --> NET2["Network: Denied/Allowlist"] 166 KANI --> NET2 167 LOOM --> NET2 168 169 %% Cache Awareness 170 L1 --> Cache 171 L2 --> Cache 172 L3 --> Cache 173 L4 --> Cache 174 175 %% Metrics & Observability 176 L1 --> Metrics 177 L2 --> Metrics 178 L3 --> Metrics 179 L4 --> Metrics 180 181 %% Styling 182 classDef rustType fill:#c6f5d0,stroke:#2a9d8f,stroke-width:2px; 183 class CLI,CM,VE,Cache,Metrics,PM,L1,L2,L3,L4,TS,RT,AST rustType 184 classDef sandbox fill:#fdf6e3,stroke:#f4a261,stroke-width:2px; 185 class TLA,ALLOY,PROP,KANI,LOOM,FS1,FS2,NET1,NET2 sandbox 186 ``` 187 188 ### **Highlights** 189 190 1. **Rust-Centric Type Guarantees** 191 192 * Typestate & linear types enforce layer dependencies at compile-time. 193 * Refinement types validate value-level invariants. 194 * AST validation ensures attribute macros and configuration correctness. 195 196 2. **Layered DAG Enforcement** 197 198 * Each layer only executes if prior layers pass successfully. 199 * Ensures **formal → type → property → monitoring** sequence is never violated. 200 201 3. **Incremental Verification & Caching** 202 203 * All layers are cache-aware; avoids redundant execution. 204 * Cache keyed by **AST content, configuration hash, and tool versions**. 205 206 4. **Sandboxed Plugin Execution** 207 208 * External tools run in isolated sandboxes with: 209 210 * Restricted filesystem access 211 * Network denied or allowlist 212 * Resource limits (CPU, memory, file descriptors) 213 * Captures outputs for structured parsing. 214 215 5. **Observability & Metrics** 216 217 * Metrics collected for all layers: execution time, cache hits, violations. 218 * Supports structured logs for CI and human-readable output. 219 220 6. **Unified Orchestration** 221 222 * CLI → Config → Verification Engine → Plugin Manager → Layers → Cache/Metrics 223 * Ensures reproducible, safe, and type-checked verification runs. 224 225 ### Configuration Hierarchy 226 227 ```mermaid 228 graph TD 229 ROOT[Root Config<br/>ferrisproof.toml] 230 231 subgraph "Module Overrides" 232 CRYPTO[crypto/*<br/>level: formal] 233 API[api/*<br/>level: standard] 234 UTILS[utils/*<br/>level: minimal] 235 end 236 237 subgraph "Item Attributes" 238 FUNC["Function Level<br/><code>#[verification(level = strict)]</code>"] 239 MOD["Module Level<br/><code>#[verification(spec = raft.tla)]</code>"] 240 end 241 242 ROOT --> CRYPTO 243 ROOT --> API 244 ROOT --> UTILS 245 246 CRYPTO --> FUNC 247 API --> MOD 248 ``` 249 250 --- 251 252 ## Project Structure 253 254 ``` 255 ferris-proof/ 256 ├── ferris-proof-cli/ # Command-line interface 257 ├── ferris-proof-core/ # Core verification engine 258 ├── ferris-proof-config/ # Configuration management 259 ├── ferris-proof-plugins/ # Plugin system and tool integrations 260 ├── scripts/ # CI/CD and development scripts 261 │ ├── run-tests.sh # Unified test runner with comprehensive options 262 │ ├── ci-local.sh # Local CI pipeline 263 │ ├── ci-setup.sh # Development environment setup 264 │ ├── container-build.sh # Container build script 265 │ └── verify-containerfiles.sh # Container validation script 266 ├── docs/ # Documentation 267 │ ├── ferris-proof.tsd.specs.md # Detailed architecture design 268 │ ├── ferris-proof.prd.specs.md # Functional requirements 269 │ └── ci-pipeline.md # CI/CD documentation 270 ├── Cargo.toml # Workspace configuration 271 ├── Containerfile # Standard container build 272 ├── Containerfile.alpine # Minimal Alpine container build 273 ├── Makefile # Common development tasks 274 ├── .gitlab-ci.yml # GitLab CI/CD pipeline with comprehensive testing 275 ├── .github/ # GitHub Actions workflows 276 │ ├── workflows/ci.yml # Main CI pipeline with multi-platform testing 277 │ ├── workflows/property-tests.yml # Dedicated property-based testing workflow 278 │ └── workflows/release.yml # Release automation 279 ├── proptest.toml # Property-based test configuration 280 ├── ReadMe.md # This file 281 ├── Contributing.md # Contribution guidelines 282 └── Licence.md # CC0 1.0 Universal licence 283 ``` 284 285 --- 286 287 ## Development Status 288 289 ### ✅ Completed 290 - **Core Infrastructure**: Rust workspace with 4 crates 291 - **CLI Tool**: Complete command-line interface with project initialization, configuration management, error explanation, and cache management 292 - **Configuration System**: Hierarchical TOML configuration with validation and discovery 293 - **Plugin Architecture**: Extensible verification tool integration with sandboxed execution and network isolation 294 - **Property-Based Testing**: Framework for correctness validation with comprehensive test coverage (20+ property tests) 295 - **Verification Cache**: Complete content-addressed caching system with Blake3 hashing, AST normalization, compression, and management commands 296 - **CI/CD Pipeline**: Comprehensive automated testing with GitHub Actions and GitLab CI, multi-platform support, property-based test automation, extended fuzzing, regression detection, and configurable test parameters 297 - **Test Automation**: Unified test runner script with support for unit, integration, and property tests, configurable parameters, coverage reporting, and environment variable integration 298 - **Documentation**: Comprehensive specs, API docs, getting-started guides, and CI pipeline documentation 299 - **Security**: Sandboxed execution, input validation, network isolation, and local-only verification 300 301 ### 🚧 In Progress 302 - **Verification Engine**: Core orchestration logic for multi-layer verification 303 - **Formal Specification Integration**: TLA+ and Alloy tool integration 304 - **Type-Level Verification**: Session types and refinement types implementation 305 306 ### 📋 Planned 307 - **Production Monitoring**: Runtime assertions and observability hooks 308 - **Advanced Tool Integrations**: Kani, Loom, and additional verification backends 309 - **Performance Optimisations**: Parallel verification and advanced caching strategies 310 311 ## Setup & Installation 312 313 ### Prerequisites 314 315 - **Rust 1.83+** (specified in `rust-toolchain.toml`) 316 - **Git** for version control 317 - **pkg-config** and **libssl-dev** (Linux) or **openssl** (macOS) for SSL support 318 319 ### Optional Tools (for full verification) 320 321 - **TLA+ Toolbox**: [Download here](https://lamport.azurewebsites.net/tla/tools.html) 322 - **Alloy Analyzer**: [Download here](http://alloytools.org/) 323 324 ### Build from Source 325 326 ```bash 327 # Clone the repository 328 git clone https://github.com/yumin-chen/ferris-proof.git 329 cd ferris-proof 330 331 # Build all crates 332 cargo build --all-features 333 334 # Run tests using the unified test runner 335 ./scripts/run-tests.sh # Run all tests with default settings 336 ./scripts/run-tests.sh -t unit # Unit tests only 337 ./scripts/run-tests.sh -t integration # Integration tests only 338 ./scripts/run-tests.sh -t property # Property-based tests only 339 ./scripts/run-tests.sh -t all # All tests explicitly 340 341 # Run tests with custom configuration 342 ./scripts/run-tests.sh -t property -c 5000 -s 50000 # 5000 cases, 50000 shrink iterations 343 ./scripts/run-tests.sh -C # Generate coverage report 344 ./scripts/run-tests.sh -v -t all # Verbose output for all tests 345 346 # Traditional cargo test (also works) 347 cargo test --all-features 348 349 # Install CLI tool 350 cargo install --path ferris-proof-cli 351 352 # Verify installation 353 ferris-proof --version 354 ``` 355 356 ### Using the CLI Tool 357 358 ```bash 359 # Initialise a new project 360 ferris-proof init --level standard 361 362 # Show project configuration 363 ferris-proof config 364 365 # Validate configuration 366 ferris-proof config --validate 367 368 # Explain error codes 369 ferris-proof explain FP-CF-001 370 371 # Get help for any command 372 ferris-proof --help 373 ferris-proof init --help 374 ``` 375 376 --- 377 378 ## Verification Cache System 379 380 FerrisProof includes a sophisticated verification cache system that dramatically improves performance by avoiding redundant verification work: 381 382 ### Cache Features 383 384 - **Content-Addressed Storage**: Cache entries organized by Blake3 content hashes 385 - **AST Normalization**: Rust files normalized to ignore comments and whitespace changes 386 - **Tool Version Tracking**: Automatic invalidation when external tool versions change 387 - **Zstd Compression**: Efficient storage with transparent compression/decompression 388 - **Atomic Operations**: Safe concurrent access with atomic file operations 389 - **Persistence**: Cache survives across verification runs and system restarts 390 391 ### Cache Management Commands 392 393 ```bash 394 # Show cache statistics and health information 395 ferris-proof cache info 396 397 # Check cache integrity and get recommendations 398 ferris-proof cache health 399 400 # Remove expired cache entries 401 ferris-proof cache cleanup 402 403 # Clear all cache entries (with confirmation) 404 ferris-proof cache clear 405 406 # Optimise cache storage and remove expired entries 407 ferris-proof cache compact 408 409 # Repair corrupted cache entries 410 ferris-proof cache repair 411 ``` 412 413 ### Cache Configuration 414 415 The cache system is configured in your `ferrisproof.toml`: 416 417 ```toml 418 [features] 419 cache_enabled = true # Enable/disable caching 420 cache_ttl = 86400 # Cache entry TTL in seconds (24 hours) 421 422 [thresholds] 423 max_memory_usage = 2147483648 # Maximum memory usage (2GB) 424 ``` 425 426 ### Cache Performance 427 428 The cache system provides significant performance improvements: 429 430 - **Cache Hit Rate**: Typically 70-90% for incremental changes 431 - **Storage Efficiency**: 60-80% compression ratio with zstd 432 - **Access Speed**: Sub-millisecond cache lookups 433 - **Memory Usage**: Configurable limits with automatic cleanup 434 435 --- 436 437 ## Configuration 438 439 FerrisProof uses hierarchical TOML configuration. Initialise a project to get started: 440 441 ```bash 442 # Initialise with interactive prompts 443 ferris-proof init --interactive 444 445 # Or initialise with a specific level 446 ferris-proof init --level standard 447 ``` 448 449 This creates a `ferrisproof.toml` file in your project root: 450 451 ```toml 452 [profile] 453 level = "standard" 454 enforcement = "warning" 455 enabled_techniques = ["TypeSafety", "PropertyTests"] 456 457 [tools.proptest] 458 cases = 1000 459 max_shrink_iters = 10000 460 461 [features] 462 cache_enabled = true 463 parallel_execution = true 464 generate_reports = true 465 466 [thresholds] 467 max_verification_time = 300 # 5 minutes 468 max_memory_usage = 2147483648 # 2GB 469 cache_ttl = 86400 # 24 hours 470 ``` 471 472 ### Verification Levels 473 474 - **Minimal**: Type safety only 475 - **Standard**: Type safety + Property-based testing 476 - **Strict**: + Session types, refinement types, concurrency testing 477 - **Formal**: + Formal specifications (TLA+, Alloy) 478 479 ### Configuration Commands 480 481 ```bash 482 # Show current configuration 483 ferris-proof config 484 485 # Validate configuration 486 ferris-proof config --validate 487 488 # Show effective configuration for a specific file 489 ferris-proof config --file src/main.rs 490 ``` 491 492 ### Configuration Hierarchy 493 494 FerrisProof uses hierarchical TOML configuration with the following precedence (highest to lowest): 495 496 1. **Item-level attributes** (`#[verification(...)]`) 497 2. **Module-level glob patterns** (most specific path match) 498 3. **Module configuration files** (nearest ancestor directory) 499 4. **Root configuration** (`ferrisproof.toml`) 500 501 --- 502 503 ## Verification Reports 504 505 FerrisProof generates comprehensive verification reports in multiple formats: 506 507 - **JSON**: Machine-readable for CI integration 508 - **Markdown**: Human-readable with rich formatting 509 - **HTML**: Interactive web-based reports 510 511 Report contents include: 512 - Verification status per layer 513 - Violations with severity levels 514 - Performance metrics and timing 515 - Cache hit rates and efficiency 516 - Tool versions and configurations 517 518 --- 519 520 ## Security & Privacy 521 522 FerrisProof is designed with security in mind: 523 524 - **No external data transmission** without explicit consent 525 - **Local-only verification** for sensitive codebases 526 - **Sandboxed execution** of external tools 527 - **Input validation** to prevent path traversal 528 - **Secure configuration parsing** 529 530 --- 531 532 ## Performance Targets 533 534 | Verification Level | Project Size | Target Duration | Memory Usage | Cache Hit Rate | 535 |--------------------|--------------|-----------------|--------------|----------------| 536 | Minimal | <100k LOC | <30s | <500 MB | 85-95% | 537 | Standard | <100k LOC | <5 min | <2 GB | 75-90% | 538 | Strict | <50k LOC | <10 min | <4 GB | 70-85% | 539 | Formal | <10k LOC | <30 min | <8 GB | 60-80% | 540 541 --- 542 543 ## Error Handling 544 545 FerrisProof provides comprehensive error handling with detailed explanations: 546 547 ```bash 548 # Explain any error code 549 ferris-proof explain FP-CF-001 550 ferris-proof explain FP-VR-001 551 ferris-proof explain FP-TL-001 552 ``` 553 554 ### Error Code Categories 555 556 - **FP-CF-XXX**: Configuration errors 557 - **FP-VR-XXX**: Verification errors 558 - **FP-TL-XXX**: Tool errors 559 - **FP-IO-XXX**: I/O and file system errors 560 - **FP-CH-XXX**: Cache system errors 561 562 ### Common Error Codes 563 564 | Code | Description | Suggested Fix | 565 |------|-------------|---------------| 566 | FP-CF-001 | Invalid verification level | Use: minimal, standard, strict, formal | 567 | FP-CF-002 | Missing required configuration field | Run `ferris-proof init` | 568 | FP-VR-001 | Property test failure | Review counterexample | 569 | FP-TL-001 | TLA+ TLC not found | Install TLA+ tools | 570 | FP-CH-001 | Cache corruption detected | Run `ferris-proof cache repair` | 571 | FP-CH-002 | Cache storage full | Run `ferris-proof cache cleanup` | 572 573 Each error explanation includes: 574 - Detailed description 575 - Common causes 576 - Step-by-step solutions 577 - Code examples 578 - Related error codes 579 580 --- 581 582 ## CLI Reference 583 584 ### Global Options 585 586 ```bash 587 ferris-proof [OPTIONS] <COMMAND> 588 589 Options: 590 --config <FILE> Path to configuration file 591 -v, --verbose... Enable verbose output (can be repeated) 592 --output-format <FORMAT> Output format: human, json, compact 593 --no-color Disable colored output 594 -h, --help Print help 595 -V, --version Print version 596 ``` 597 598 ### Commands 599 600 #### `init` - Initialise Project 601 ```bash 602 ferris-proof init [OPTIONS] 603 604 Options: 605 --level <LEVEL> Verification level [default: standard] 606 --interactive Use interactive mode 607 --template <TEMPLATE> Project template to use 608 ``` 609 610 #### `config` - Show Configuration 611 ```bash 612 ferris-proof config [OPTIONS] 613 614 Options: 615 --file <FILE> Show config for specific file 616 --validate Validate configuration 617 ``` 618 619 #### `cache` - Cache Management 620 ```bash 621 ferris-proof cache <SUBCOMMAND> 622 623 Subcommands: 624 info Show cache statistics and information 625 health Check cache health and integrity 626 cleanup Remove expired cache entries 627 clear Clear all cache entries 628 compact Optimise cache storage 629 repair Repair corrupted cache entries 630 ``` 631 632 ### Test Runner Script 633 634 The unified test runner script (`scripts/run-tests.sh`) provides comprehensive test execution: 635 636 ```bash 637 ./scripts/run-tests.sh [OPTIONS] 638 639 Options: 640 -t, --type TYPE Test type: unit, integration, property, all (default: all) 641 -v, --verbose Enable verbose output 642 -c, --cases NUM Number of property test cases (default: 1000) 643 -s, --shrink NUM Max shrink iterations for property tests (default: 10000) 644 -T, --timeout MIN Timeout in minutes (default: 30) 645 -j, --parallel Run tests in parallel (default: true) 646 -C, --coverage Generate code coverage report 647 -h, --help Show help message 648 649 Examples: 650 ./scripts/run-tests.sh # Run all tests with defaults 651 ./scripts/run-tests.sh -t unit # Run only unit tests 652 ./scripts/run-tests.sh -t property -c 5000 # Run property tests with 5000 cases 653 ./scripts/run-tests.sh -C # Run all tests with coverage 654 ./scripts/run-tests.sh -v -t all # Run all tests with verbose output 655 656 Environment Variables: 657 PROPTEST_CASES Override property test case count 658 PROPTEST_MAX_SHRINK_ITERS Override max shrink iterations 659 PROPTEST_TIMEOUT Override property test timeout (ms) 660 RUST_BACKTRACE Enable Rust backtraces (0, 1, full) 661 CARGO_TERM_COLOR Control colored output (auto, always, never) 662 ``` 663 664 --- 665 666 ## Workflow Examples 667 668 ### Project Initialization 669 670 ```mermaid 671 sequenceDiagram 672 participant U as User 673 participant CLI as CLI Tool 674 participant CM as Config Manager 675 participant FS as File System 676 677 U->>CLI: ferris-proof init --level standard 678 CLI->>CLI: Parse arguments and validate level 679 CLI->>CM: create_config_for_level(standard) 680 CM->>FS: write ferrisproof.toml 681 FS-->>CM: Success 682 CLI->>FS: create directory structure 683 CLI->>FS: create template files (if specified) 684 CLI-->>U: ✓ Project initialised successfully 685 ``` 686 687 ### Configuration Management 688 689 ```mermaid 690 sequenceDiagram 691 participant U as User 692 participant CLI as CLI Tool 693 participant CM as Config Manager 694 participant V as Validator 695 696 U->>CLI: ferris-proof config --validate 697 CLI->>CM: load_project_config() 698 CM->>CM: discover_config_files() 699 CM->>CM: merge_hierarchical_configs() 700 CM->>V: validate_config() 701 alt Valid Configuration 702 V-->>CM: ValidationResult::Ok 703 CM-->>CLI: Configuration valid 704 CLI-->>U: ✓ Configuration is valid 705 else Invalid Configuration 706 V-->>CM: ValidationResult::Error(details) 707 CM-->>CLI: Validation errors 708 CLI-->>U: ✗ Configuration validation failed 709 end 710 ``` 711 712 ### Error Code Explanation 713 714 ```mermaid 715 sequenceDiagram 716 participant U as User 717 participant CLI as CLI Tool 718 participant EC as Error Catalog 719 720 U->>CLI: ferris-proof explain FP-CF-001 721 CLI->>EC: lookup_error_code("FP-CF-001") 722 alt Known Error Code 723 EC-->>CLI: ErrorExplanation{title, description, causes, solutions} 724 CLI-->>U: Display formatted explanation 725 else Unknown Error Code 726 EC-->>CLI: None 727 CLI-->>U: Unknown error code + suggestions 728 end 729 ``` 730 731 ### Verification with Caching 732 733 ```mermaid 734 sequenceDiagram 735 participant CLI as CLI Tool 736 participant VE as Verification Engine 737 participant Cache as Verification Cache 738 participant CM as Config Manager 739 participant PM as Plugin Manager 740 participant TLA as TLA+ TLC 741 742 CLI->>VE: verify(targets) 743 VE->>CM: for_file(target.path) 744 CM-->>VE: EffectiveConfig 745 746 VE->>Cache: get(target, config_hash) 747 alt Cache Hit 748 Cache-->>VE: CachedResult 749 VE-->>CLI: VerificationResult (cached) 750 else Cache Miss 751 VE->>PM: plugins_for_technique(FormalSpecs) 752 PM-->>VE: [TLA+ Plugin] 753 VE->>TLA: verify(spec.tla) 754 TLA-->>VE: ModelCheckResult 755 VE->>Cache: store(target, result) 756 VE-->>CLI: VerificationResult (fresh) 757 end 758 ``` 759 760 --- 761 ## Documentation 762 763 - [Getting Started Guide](docs/getting-started.md) 764 - [CLI Reference](#cli-reference) - Complete command-line interface documentation 765 - [Configuration Guide](#configuration) - Hierarchical configuration system 766 - [Error Handling](#error-handling) - Comprehensive error code catalog 767 - [CI Pipeline](docs/ci-pipeline.md) 768 - [API Documentation](https://docs.rs/ferris-proof) 769 770 For detailed technical information: 771 772 - **[Design Document](docs/ferris-proof.tsd.specs.md)** - Comprehensive architecture and implementation details 773 - **[Requirements Document](docs/ferris-proof.prd.specs.md)** - Functional requirements and acceptance criteria 774 - **[Task Tracking](.kiro/specs/ferris-proof/tasks.md)** - Implementation progress and task status 775 776 --- 777 778 ## Future Directions 779 780 * Auto-generate Rust property tests from Alloy/TLA+ models 781 * Extend support for distributed multi-agent systems 782 * Continuous verification in CI/CD pipelines 783 * Runtime trace comparison with TLA+ execution paths 784 * Plugin ecosystem for additional verification backends 785 * Advanced cache analytics and performance optimisation 786 * Distributed cache sharing for team environments 787 788 --- 789 790 ## Contributing 791 792 We welcome contributions! Please see [Contributing.md](Contributing.md) for guidelines. 793 794 ## Licence 795 796 This work is dedicated to the public domain under the [CC0 1.0 Universal](Licence.md) licence. 797 798 To the extent possible under law, the contributors have waived all copyright and related or neighbouring rights to this work.