Testing Infrastructure

Overview

Bitcoin Commons uses BLVM Specification Lock, property-based testing, fuzzing, integration tests, runtime assertions, and MIRI. Proof scope: proof limitations.

Testing Strategy

Layered Verification

Formal Verification: Z3 proofs via BLVM Specification Lock on spec-locked consensus code
Property-Based Testing (Proptest): Randomized invariant checks
Fuzzing (libFuzzer): Random input exploration
Integration Tests: End-to-end scenarios
Unit Tests: Per-function tests
Runtime Assertions: Optional invariant checks (feature-gated)
MIRI: Undefined-behavior detection on selected tests

Test Types

Unit Tests

Unit tests verify individual functions in isolation:

Location: tests/ directory, #[test] functions
Coverage: Public functions
Examples: Transaction validation, block validation, script execution

Property-Based Tests

Property-based tests verify mathematical invariants:

Location: tests/consensus_property_tests.rs and other property test files
Coverage: Mathematical invariants
Tool: Proptest

Integration Tests

Integration tests verify end-to-end correctness:

Location: tests/integration/ directory
Coverage: Multi-component scenarios
Examples: BIP compliance, historical replay, mempool mining

Fuzzing

Coverage-guided fuzzing uses libFuzzer via cargo-fuzz on unstructured byte inputs. It complements spec-lock, unit tests, and property tests; it does not replace them.

Harness names and crate wiring live in each repo’s fuzz/Cargo.toml ([[bin]] entries). Implementation sources are under fuzz/fuzz_targets/. Do not treat prose (here or in READMEs) as an inventory; it goes stale.

Crate	Location
blvm-consensus	blvm-consensus/fuzz
blvm-protocol	blvm-protocol/fuzz
blvm-node	blvm-node/fuzz
blvm-sdk	blvm-sdk/fuzz

Local monorepo checkouts often use [patch.crates-io] in fuzz/Cargo.toml so fuzz crates resolve path dependencies; continuous integration may build fuzz targets against crates.io instead (see comments in each repo’s fuzz/Cargo.toml, for example blvm-consensus/fuzz and blvm-protocol/fuzz).

Quick start (consensus)

cd blvm-consensus/fuzz
./init_corpus.sh # optional: seed corpora
cargo +nightly fuzz run <target_name>

Pick <target_name> from fuzz/Cargo.toml. The fuzz/ directory also contains scripts (e.g. campaign runners, corpus helpers, sanitizer build helpers), use what matches your workflow.

CI

Fuzz jobs are defined in the relevant repository’s GitHub Actions. Matrix steps and timeouts may not exercise every harness on every run; read the workflow for actual behavior.

Formal Verification (spec-lock)

Formal verification uses blvm-spec-lock / BLVM Specification Lock in blvm-consensus:

Location: src/, tests/
Command: cargo spec-lock verify (same command as CI; self-hosted runners in production workflows)
Inventory: verification policy
Tool: blvm-spec-lock

See also: UTXO Commitments

Runtime Assertions

Runtime assertions catch violations during execution:

Coverage: Critical paths with runtime assertions
Production: Available via feature flag

MIRI Integration

MIRI detects undefined behavior:

CI Integration: Automated undefined behavior detection
Coverage: Property tests and critical unit tests
Tool: MIRI interpreter

Coverage Statistics

Overall Coverage

Verification Technique	Status
Formal Proofs (spec-lock)	✅ Z3 proofs on spec-locked code (self-hosted CI)
Property Tests	✅ Broad invariant coverage
Runtime Assertions	✅ Feature-gated on selected paths
Fuzz Targets	✅ Critical validation surfaces
MIRI Integration	✅ UB checks on selected tests
Mathematical Specs	✅ Orange Paper + docs

Coverage by Consensus Area

Economic rules, PoW, transactions, blocks, scripts, reorg, crypto, mempool, SegWit, and serialization are covered by unit, property, integration, and fuzz tests, with BLVM Specification Lock on critical spec-locked paths. Details: verification policy.

Running Tests

Run All Tests

cd blvm-consensus
cargo test

Run Specific Test Type

# Unit tests
cargo test --lib

# Property tests
cargo test --test consensus_property_tests

# Integration tests
cargo test --test integration

# Fuzz (example; target name from fuzz/Cargo.toml)
cd fuzz && cargo +nightly fuzz run <target_name>

Run with MIRI

cargo +nightly miri test

Run Spec-Lock Verification

Mirror CI per Formal Verification:

export SPEC_LOCK_STRICT=1
export SPEC_LOCK_Z3_TIMEOUT_SECS=120
cargo spec-lock check-drift --crate-path . --spec-path ../blvm-spec/PROTOCOL.md ../blvm-spec/ARCHITECTURE.md --scoped-unparseables
cargo spec-lock verify --crate-path . --spec-path ../blvm-spec/PROTOCOL.md ../blvm-spec/ARCHITECTURE.md --timeout 120 --json-out spec_lock_verify.json

Filter to one function: cargo spec-lock verify --name <function> …. There is no --tier or --proof flag.

Coverage Goals

Target Coverage

Ongoing expansion of spec-lock coverage, property tests, fuzz corpora, runtime assertions, and integration scenarios. Status: verification policy, proof limitations.

Test Organization

Directory Structure

blvm-consensus/
├── src/ # Source; spec-lock on marked functions
├── tests/
│ ├── consensus_property_tests.rs # Main property tests
│ ├── integration/ # Integration tests
│ ├── unit/ # Unit tests
│ ├── fuzzing/ # Fuzzing helpers
│ └── verification/ # Verification tests
└── fuzz/
 └── fuzz_targets/ # Fuzz targets

Edge Case Coverage

Beyond Proof Bounds

Edge cases beyond blvm-spec-lock proof bounds are covered by:

Property-Based Testing: Random inputs of various sizes
Mainnet Block Tests: Real Bitcoin mainnet blocks
Integration Tests: Realistic scenarios
Fuzz Testing: Random generation

Unit Tests: Required for merge
Property Tests: Required for merge
Integration Tests: Required for merge
Fuzz Tests: Run on schedule
Differential Tests: blvm-bench integration suite (self-hosted workflow currently paused; see Differential Testing)
BLVM Specification Lock: Required merge gate where #[spec_locked] is enabled (check-drift then verify on self-hosted runners; see Formal Verification)
MIRI: Run on property tests and critical unit tests

Test Metrics

Property Test Functions: Multiple functions across all files
Runtime Assertions: Multiple assertions (assert! and debug_assert!)
Fuzz Targets: Multiple fuzz targets

Components

The testing infrastructure includes:

Unit tests for all public functions
Property-based tests for mathematical invariants
Integration tests for end-to-end scenarios
Fuzz tests for edge case discovery
blvm-spec-lock proofs for formal verification
Runtime assertions for execution-time checks
MIRI integration for undefined behavior detection
Differential tests (see Differential Testing)

Source

test scripts guide (test data helpers); verification policy (verification workflows)
consensus_property_tests.rs
mod.rs
Formal Verification
tests/
proof limitations
differential_tests.rs (consensus stub)
blvm-bench integration tests, full-chain differential testing
verification policy
blvm-consensus/tests/, blvm-consensus/fuzz/, blvm-consensus/src/ (blvm-consensus/fuzz/blvm-consensus/src/`)

BLVM Documentation