https://docs.rs/certeza

---

Overview

certeza is a comprehensive framework for approaching asymptotic test effectiveness in Rust software systems through the pragmatic integration of:

• Property-based testing (using proptest)
• Mutation testing (using cargo-mutants)
• Structural coverage analysis (using cargo-llvm-cov)
• Selective formal verification (using Kani)

Philosophy

While complete verification remains theoretically impossible (Dijkstra: "testing can only prove the presence of bugs, not their absence"), this framework provides a reproducible methodology for achieving practical maximum confidence in critical systems.

Tiered TDD-X Workflow

The framework implements three-tiered verification that balances rigor with developer productivity:

Tier 1: ON-SAVE (Sub-second feedback)

• Unit tests and focused property tests
• Static analysis (cargo check, cargo clippy)
• Enables rapid iteration in flow state

Command: make tier1

Tier 2: ON-COMMIT (1-5 minutes)

• Full property-based test suite
• Coverage analysis (target: 95%+ line coverage)
• Integration tests
• Pre-commit hook enforcement

Command: make tier2

Tier 3: ON-MERGE/NIGHTLY (Hours)

• Comprehensive mutation testing (target: >85% mutation score)
• Formal verification for critical paths
• Performance benchmarks
• CI/CD gate for main branch

Command: make tier3

Critical Principle: Different verification techniques operate at different time scales. Fast feedback enables flow; slow feedback causes context switching waste. Never run mutation testing or formal verification in the inner development loop.

Quick Start

# Clone the repository
git clone https://github.com/paiml/certeza.git
cd certeza

# Run quick checks (Tier 1)
make tier1

# Run full test suite with coverage (Tier 2)
make tier2

# Build the project
cargo build

# Run all tests
cargo test

# Generate documentation
cargo doc --open

Installation

Add this to your Cargo.toml:

[dependencies]
certeza = "0.1.0"

Usage Example

TruenoVec - Custom Growable Vector

The primary demonstration of the certeza framework is TruenoVec<T>, a custom growable vector implementation that showcases the complete three-tiered testing approach.

use certeza::TruenoVec;

fn main() {
    // Create a new vector
    let mut vec = TruenoVec::new();

    // Push elements
    vec.push(1);
    vec.push(2);
    vec.push(3);

    // Access elements
    assert_eq!(vec.len(), 3);
    assert_eq!(vec.get(1), Some(&2));

    // Pop elements
    assert_eq!(vec.pop(), Some(3));
    assert_eq!(vec.len(), 2);

    // Pre-allocate capacity for performance
    let mut vec2 = TruenoVec::with_capacity(1000);
    for i in 0..1000 {
        vec2.push(i);  // No reallocation
    }
}

Key Features

• Manual Memory Management: Uses NonNull<T> for safe manual allocation
• 2x Growth Factor: Exponential growth for amortized O(1) push operations
• RAII Semantics: Proper Drop implementation ensures no memory leaks
• Thread Safety: Send + Sync where T is Send/Sync
• Zero-Cost Abstraction: 24-byte overhead (ptr + len + capacity)
• Full Iterator Support: Bidirectional iterators (iter, iter_mut, into_iter)
• Advanced Operations: insert, remove, clear with optimal performance
• Complete Trait Support: All standard collection traits (Deref, Clone, Hash, Ord, Display, Borrow, etc.)
• Comprehensive Testing: 260 tests with 97.7% mutation score

Complete Trait Implementation

TruenoVec implements all standard Rust collection traits for full std::Vec feature parity:

Core Traits:

• Default, Drop, Clone
• Send + Sync (thread safety)

Conversion Traits:

• From<Vec<T>>, From<&[T]>
• FromIterator<T>, Extend<T>
• IntoIterator (owned, &, &mut)

Indexing Traits:

• Index<usize>, IndexMut<usize>

Comparison Traits:

• PartialEq, Eq
• PartialOrd, Ord (sorting support)

Hashing:

• Hash (HashMap/HashSet keys)

Ergonomic Traits (Phase 3.1):

• Deref<Target=[T]>, DerefMut (automatic slice coercion)
• AsRef<[T]>, AsMut<[T]> (generic bounds)

Display & Formatting (Phase 3.3):

• Debug (pretty printing)
• Display (user-friendly output)

Advanced Borrowing (Phase 3.3):

• Borrow<[T]>, BorrowMut<[T]> (HashMap/BTreeMap lookup support)

This enables TruenoVec to be used in:

• ✅ Generic algorithms accepting &[T] or AsRef<[T]>
• ✅ HashMap and HashSet as keys
• ✅ BTreeMap and BTreeSet as keys
• ✅ Sorting with .sort() or Vec::sort()
• ✅ All slice methods through Deref coercion

Comprehensive Test Coverage

Total Tests: 260 tests across all tiers ✅ 97.7% mutation score

Tier 1: Unit Tests (180+ tests)

• Basic operations: new, with_capacity, push, pop, clear
• Index access: get, get_mut with bounds checking
• Advanced operations: insert, remove at various positions
• Iterator support: iter, iter_mut, into_iter with bidirectional iteration
• Growth behavior and capacity management
• Drop trait verification with destructor counting
• Memory deallocation and leak prevention tests
• Edge case handling (empty vectors, single elements, boundary conditions)
• Mutation-resistant test cases for critical operations
• Phase 3.1 Ergonomic Traits (50 tests):
  • Deref/DerefMut coercion and slice method access
  • AsRef/AsMut with generic functions
  • Slice operation consistency
• Phase 3.2 Comparison & Hash Traits (33 tests):
  • PartialOrd: <, >, <=, >= operators
  • Ord: Total ordering, BTreeMap/BTreeSet support
  • Hash: HashMap/HashSet key support
• Phase 3.3 Display & Borrow Traits (22 tests):
  • Display: User-friendly formatting, consistency with std::Vec
  • Borrow/BorrowMut: Generic function support, HashMap lookup compatibility
  • Slice operation interoperability
• Sub-second execution

Tier 2: Property-Based Tests (60 properties)

• Length invariant after push operations
• Capacity bound (capacity >= len) maintained
• Push/pop symmetry (inverse operations)
• Index access correctness
• Out-of-bounds safety
• Exponential growth factor verification
• Behavioral equivalence with std::Vec
• Empty vector invariants
• Mutable access correctness
• Repeated operations integrity
• Clear operation preserves capacity
• Insert/remove maintain order
• Insert-then-remove inverse operations
• Clear-then-reuse functionality
• Phase 3.1 Deref/AsRef Properties (15 properties):
  • Deref/AsRef equivalence with as_slice
  • Slice method correctness vs std::Vec
  • Generic function interoperability
  • DerefMut mutation operations
• Phase 3.2 Comparison/Hash Properties (10 properties):
  • PartialOrd/Ord matches std::Vec behavior
  • Ordering transitivity and antisymmetry
  • Hash consistency with Eq
  • HashMap/BTreeMap operations correctness
  • Sorting and lexicographic ordering
• Phase 3.3 Display/Borrow Properties (7 properties):
  • Display format consistency with std::Vec Debug output
  • Borrow equivalence with AsRef/AsMut
  • Display respects element Display implementation
  • Slice operation correctness through Borrow

Tier 2: Integration Tests (26 scenarios)

• Basic Integration Tests:
  • Basic vector operations workflow
  • Capacity management and preallocation
  • Stack semantics (LIFO behavior)
  • Integration with standard Rust types (String, complex structs)
  • Real-world buffer usage patterns
  • Interleaved push/pop operations
  • Out-of-bounds access safety
  • Thread safety (Send + Sync)
  • Arc integration for shared ownership
• Advanced Scenario-Based Tests:
  • User records management system
  • Stack-based expression evaluation
  • Batch processing with pre-allocation
  • Undo/Redo system implementation
  • Graph adjacency list data structures
  • Ring buffer patterns
  • Large dataset processing (10,000 elements)
  • Type safety with various element types
  • Thread safety compilation checks
  • Memory efficiency validation (24-byte overhead)
  • Edge case handling
  • std::Vec behavioral equivalence

Tier 3: Formal Verification (3 Kani proofs)

• Capacity invariant proof (capacity >= len for all paths)
• Push/pop correctness proof (mathematical verification)
• Bounds checking verification (no buffer overflows)

Documentation Tests (21 tests)

• All public API examples verified
• 100% rustdoc coverage for public items
• Comprehensive examples in module documentation

Performance Characteristics

Benchmarks demonstrate competitive performance with std::Vec:

• Push (sequential): ~10 ns/operation average
• Pop: O(1) constant time
• Get (random access): O(1) with cache efficiency
• Growth pattern: ~14 reallocations for 10,000 elements (log₂ n)
• Memory efficiency: 24-byte overhead per vector

Chaos Engineering & Fuzz Testing

certeza includes chaos engineering and fuzz testing capabilities adapted from renacer v0.4.1 (Sprint 29).

Chaos Engineering

Test system resilience under adverse conditions:

use certeza::chaos::{ChaosConfig, ChaosResult};
use std::time::Duration;

// Gentle preset for development (512MB, 80% CPU, 120s timeout)
let gentle = ChaosConfig::gentle();

// Aggressive preset for CI/CD (64MB, 25% CPU, 10s timeout, signals)
let aggressive = ChaosConfig::aggressive();

// Custom configuration using renacer builder pattern
let custom = ChaosConfig::new()
    .with_memory_limit(128 * 1024 * 1024)  // 128MB
    .with_cpu_limit(0.5)                   // 50% CPU
    .with_timeout(Duration::from_secs(30))
    .with_signal_injection(true)
    .build();

Chaos Features (renacer pattern):

• chaos-basic: Core chaos configuration and error types
• chaos-network: Network failure simulation (planned)
• chaos-byzantine: Byzantine fault injection (planned)
• chaos-full: All chaos features combined

Commands:

# Run chaos engineering tests (Tier 2)
make chaos-test

# Enable specific chaos features
cargo test --features chaos-basic
cargo test --features chaos-full

Fuzz Testing

Automated testing with libFuzzer to discover edge cases and crashes:

# Run fuzz tests for 60 seconds
make fuzz

# Extended fuzzing session
cargo +nightly fuzz run fuzz_target_1 -- -max_total_time=300

The fuzz target tests TruenoVec operations:

• Push/pop operations
• Random access
• Iterator operations
• Invariant verification

Integration: Chaos tests run in Tier 2 (ON-COMMIT) for fast feedback.

PMAT Compliance

This project is fully compliant with the Pragmatic AI Labs Multi-Language Agent Toolkit (PMAT) standards, enforcing EXTREME TDD:

Quality Standards

• Coverage: ≥85% line coverage (minimum), 95% (target)
• Complexity: ≤10 cyclomatic complexity per function
• SATD: Zero tolerance for TODO/FIXME/HACK comments
• Mutation Testing: ≥85% mutation score
• Documentation: ≥90% rustdoc coverage

Makefile Commands

# Development workflow
make tier1              # Quick checks (sub-second)
make tier2              # Full test suite (1-5 min)
make tier3              # Mutation testing (hours)

# Testing
make test               # Run all tests
make test-quick         # Run unit tests only
make test-property      # Run property-based tests
make coverage           # Generate coverage report
make chaos-test         # Chaos engineering tests (renacer)
make fuzz               # Fuzz testing (60s)

# Code quality
make clippy             # Run clippy linter
make clippy-strict      # Run strict clippy
make fmt                # Format code
make fmt-check          # Check formatting

# Analysis
make complexity         # Analyze complexity with PMAT
make tdg                # Technical debt grading
make security           # Security audit

# Documentation
make docs               # Generate documentation
make validate-docs      # Validate docs with PMAT

# Setup
make install-tools      # Install required tooling
make install-hooks      # Install PMAT git hooks

Testing Framework

Running Tests

# Tier 1: Quick checks (unit tests)
make tier1
cargo test --lib

# Tier 2: Full test suite (unit + property + integration + doc tests)
make tier2
cargo test --all

# Integration tests
cargo test --test integration_tests

# Benchmarks
cargo test --benches

# Property-based tests with custom case count
PROPTEST_CASES=1000 cargo test property_

Mutation Testing

Run mutation testing to verify test suite quality:

make mutation
# or
cargo mutants --no-times

Target: >85% mutation score

Coverage Analysis

Generate coverage report:

make coverage
# or
cargo llvm-cov --all-features --workspace

Target: 95%+ line coverage, 90%+ branch coverage

Risk-Based Verification

Not all code requires the same verification intensity:

Risk Level	Components	Verification Approach
Very High	unsafe blocks, memory allocators, crypto	Full framework: Property + Coverage + Mutation (90%) + Formal
High	Core algorithms, data structures, parsers	Property + Coverage + Mutation (85-90%)
Medium	Business logic, API handlers	Property + Coverage + Mutation (80%)
Low	Simple accessors, config	Unit tests + Coverage (90%)

Resource Allocation: Spend 40% of verification time on the 5-10% highest-risk code.

Architecture

Testing Pyramid

┌─────────────────┐
│  Formal (Kani)  │  ~1-5% code (invariant proofs)
├─────────────────┤
│   Integration   │  ~10% tests (system properties)
├─────────────────┤
│  Property-Based │  ~30% tests (algorithmic correctness)
├─────────────────┤
│   Unit Tests    │  ~60% tests (basic functionality)
└─────────────────┘

Key Design Principles

• Sustainable Workflows: Tiered feedback loops prevent burnout
• Risk-Based Resource Allocation: Focus on high-risk components
• Human-Centered Analysis: Mutation analysis as learning exercise
• Economic Realism: Acknowledge costs and diminishing returns

Documentation

• Main Specification - Complete framework specification (v1.1, ~14K words)
• Improvements v1.1 - Philosophy shift from "theoretical maximum" to "asymptotic effectiveness"
• CLAUDE.md - Guidance for Claude Code development

CI/CD

GitHub Actions workflow enforces quality gates:

• Tier 1: Quick checks on every push
• Tier 2: Full test suite + coverage on PR (≥85%)
• Security: Parallel security audit (cargo-audit, cargo-deny)
• Tier 3: Mutation testing on merge to main (≥85% mutation score)

Contributing

Contributions are welcome! Please ensure:

1. All tests pass: make tier2
2. Coverage ≥85%: make coverage
3. Clippy passes: make clippy-strict
4. Code is formatted: cargo fmt
5. No SATD comments (TODO/FIXME/HACK)

License

MIT License - see LICENSE file for details.

References

This project implements research findings from the certeza specification, incorporating:

• Property-based testing methodologies (QuickCheck, Hypothesis, proptest)
• Mutation testing research (Jia & Harman, 2011)
• Toyota Production System principles (Kaizen, Muda elimination)
• Continuous integration best practices (Fowler, Google)
• Software economics (Boehm, McConnell)
• Safety-critical systems standards (DO-178C, IEC 61508)

Acknowledgments

• trueno project (https://github.com/paiml/trueno) - Reference implementation
• PMAT (https://github.com/paiml/paiml-mcp-agent-toolkit) - Test orchestration toolkit
• Pragmatic AI Labs Research Division