Verification Overview

Neutron Rust code can be verified with formal tools — tools that mathematically prove your code is correct, not just test it with sample inputs. These are third-party Rust tools that work on Neutron code; the in-repo verification suite (Lean 4 model proofs, Quint protocol specs, Verus annotations) is covered on its own pages.

For the relationship between Lean, Quint, simulation, and application SDKs, see the modeling architecture. It distinguishes existing components from proposed application integrations.

Why Verification?

Testing checks a few inputs and hopes for the best. Verification proves correctness for a defined class of inputs.

| | Testing | Verification | |---|---|---| | Coverage | Sample inputs | All inputs within the tool's scope (bounded for Kani, unbounded for Verus) | | Guarantee | "No bugs found" | "No bugs can exist" within that scope | | Edge cases | Must think of them | Covered by the proof's scope | | Confidence | Probabilistic | Mathematical, modulo the tool's assumptions |

Tools

Kani and Shuttle are external tools you add to your own project — the Neutron repo does not currently ship proof harnesses or cargo dependencies for either.

Kani — Logic Verification

Bounded model checker for Rust. Checks that your functions can't panic, overflow, or violate assertions — across all possible inputs up to a bound.

#[kani::proof]
fn check_transfer() {
    let balance: u64 = kani::any();
    let amount: u64 = kani::any();
    kani::assume(amount <= balance);
    let result = balance - amount;
    assert!(result <= balance); // Kani proves this for ALL valid inputs
}

Shuttle — Concurrency Verification

Deterministic concurrency testing. Finds race conditions, deadlocks, and ordering bugs by systematically exploring all possible thread interleavings.

#[test]
fn check_no_deadlock() {
    shuttle::check_random(|| {
        // Shuttle explores all possible orderings
        let lock_a = Arc::new(Mutex::new(0));
        let lock_b = Arc::new(Mutex::new(0));
        // ... your concurrent code here
    }, 1000);
}

Verus — Full Correctness Proofs

Deductive verification for Rust. Unlike Kani's bounded checking, Verus proves correctness for all inputs without bounds — mathematical proof, not brute force. Currently requires a compiler fork; will be integrated when it becomes a standard cargo dependency.

Zero Runtime Cost

All verification runs at build/dev time only. Nothing ships in your binary. Your production code is identical whether you verified it or not — verification produces confidence, not extra code.

Getting Started

Add to your Cargo.toml:

[dev-dependencies]
kani-verifier = "0.x"
shuttle = "0.x"

Then write proof harnesses alongside your tests and run with cargo kani or cargo test (for Shuttle).