Pitbull

A deductive verifier for Rust, in the lineage of GNATprove for SPARK. Pitbull proves that Rust code in its verifiable subset cannot panic, overflow, or index out of bounds. It is intentionally narrow in scope: it is a soundness-bearing tool, and its first commitment is to tell the truth about what it has and has not proven.

What v0.1 guarantees

For any function annotated #[pitbull::verify] whose body and transitive reachable callees satisfy the Pitbull Verifiable Subset (PSS-1), Pitbull proves the Absence of Runtime Errors (AoRTE):

• No reachable panic!, unwrap, expect, or unreachable! call site
• No integer arithmetic overflow under overflow-checks = true semantics
• No out-of-bounds slice indexing
• No division or modulo by zero
• No construction of invalid primitive values (e.g. bool from arbitrary bits) If Pitbull reports verified, and the verified crate is compiled with the Pitbull-pinned toolchain, and the user has not introduced unsound #[pitbull::trusted] annotations, then the resulting binary will not exhibit any of the failure modes above on any input.

What v0.1 deliberately refuses to handle

PSS-1 forbids the following constructs in any code reachable from a verified entry point. Pitbull rejects them at compile time; this is not a warning:

• unsafe in any form: blocks, fn, trait, impl
• Raw pointers, UnsafeCell, MaybeUninit, transmute, inline assembly
• Heap allocation: Box, Vec, String, all std::collections
• Reference counting: Rc, Arc, Weak
• Interior mutability: Cell, RefCell, OnceCell, atomics
• Concurrency: thread::spawn, Mutex, channels, Send/Sync requirements
• async/await, coroutines, generators
• Trait objects (dyn Trait), function pointers, escaping closures
• Float arithmetic (deferred to v0.3)
• FFI (extern blocks)
• Build scripts, non-allowlisted proc macros, include!-family macros
• Recursion or loops without explicit #[decreases] / #[variant] clauses See docs/PSS-1.md for the normative specification.

Enforcement status (v0.2 scaffold). The core memory-safety rules above are enforced today: unsafe blocks/fn/trait/impl, FFI (extern blocks / #[no_mangle] / #[export_name] / non-Rust ABI), heap & collections, interior mutability, concurrency primitives, trait objects / fn-pointers / closures, floats, as casts, slice bounds, and overflow. A few constructs are specified but not yet fully enforced by the v0.2 scaffold — loop/recursion termination (PB041/PB042) and implicit drop-glue under verify_roots narrowing — each tracked per-rule in docs/PSS-1.md §17.1. The panic of a library method lives inside un-walked core, so it is caught at the call site. As of the prelude flip this boundary is fail-closed by default (verification.strict_library_acceptance): a call into core/std/alloc is accepted only if it is on the explicit trusted-total allow-list (is_trusted_total_library_call — the non-div/rem wrapping_*/checked_*/saturating_* int methods, Ord::min/max, From/TryFrom, the total char/slice/Option/Result methods, …; Ord::clamp and the slice sort family were evicted 2026-07-09, and the wrapping_/overflowing_/saturating_ div/rem forms (wrapping_div, overflowing_rem, saturating_div, the _euclid kin) 2026-07-12 — clamp panics on min > max, sort/sort_unstable panic on a non-total Ord, and the div/rem forms panic on a zero divisor, so all now fail closed); any other stdlib call fails closed as a coverage gap (exit 1), whether or not we have separately enumerated it as panicking. The enumerated panicking families — unwrap/expect; the panicking int methods pow/abs/div_euclid/div_ceil/next_multiple_of/from_str_radix/signed isqrt/the strict_* family/the wrapping_/overflowing_/saturating_ div-rem forms; Iterator::sum/product/step_by; the char radix/encode methods; str/slice range indexing and split_at/swap/copy_from_slice/chunks/as_chunks/… — still produce a precise (PB043) diagnostic, but they are now an optimization over the fail-closed default, not the safety boundary itself: an un-modelled panicking stdlib method can no longer be silently trusted. Operator-form arithmetic (x * y) and element-projection indexing (a[i]) are covered by PB049/PB054 regardless. The residual is now the inverse and far smaller: a genuinely total stdlib method the allow-list does not yet enumerate is conservatively rejected (a false reject, never a false discharge) until it is added — see docs/SAFETY-MANUAL.md §3.6. Contracts are checked at both ends. A #[pitbull::requires("...")] clause is an assumption while proving the annotated function's own body, so Pitbull separately requires every CALL to establish it (PB077) — otherwise safe_div(a,b){a/b} under requires("b > 0") would verify and so would oops(){safe_div(10,0)}, which divides by zero. Call sites whose arguments are constant integers are proved or refuted outright, and so are call sites that forward one of the CALLER's own parameters, or a computed expression over them (fn caller(v: u32) { let t = v + 1; safe_div(10, t) } under requires("v >= 5") on caller now verifies too — a contradictory caller contract is refused, never a vacuous discharge). Anything not yet encodable (a value behind a branch, a bitwise op, a raw SMT-LIB clause, a usize parameter) is reported as a coverage gap and exits non-zero. Postconditions (#[pitbull::ensures], PB076) are proved for the straight-line body shapes the visitor can capture exactly, and stay pending otherwise. Pitbull will not claim to have proven what it has not: an unimplemented rule is a documented gap, never a silent pass.

Why this list looks brutal

It is the same list SPARK started with. The deal SPARK has kept with its users for forty years is: tell us what we are not allowed to do, and in exchange we tell you the truth about what you have done. Pitbull makes the same deal. The constructs we forbid are not forbidden because they are bad — they are forbidden because v0.1 does not have a sound model for them yet. Each rule has a tracked Future plan in docs/PSS-1.md.

Toolchain

Pitbull pins to a specific nightly because it builds against the unstable rustc_public compiler API (exposed via the rustc_private mechanism), which is nightly-only. Use rust-toolchain.toml in your project root:

[toolchain]
channel = "nightly-2026-01-29"
components = ["rustc-dev", "llvm-tools-preview"]

For ISO 26262 / IEC 61508 / DO-178C qualified deployment, the intended path is to run on top of Ferrocene (Rust's qualified toolchain). This is a roadmap goal, not a current capability: the wrapper today builds against the unstable rustc_public API, which ships only on the pinned nightly above, so it does not yet run on a Ferrocene release. A qualification kit is likewise planned but not present in this repository — do not treat the [project] toolchain identifier (pitbull-0.1.0-ferrocene-26.02.0) as evidence of a completed Ferrocene integration; it is a forward-looking pin, not a runtime check that you are on Ferrocene.

Not in scope

Pitbull does not prove timing, side-channel resistance, or non-interference. It does not re-verify the compiler beneath it. It does not detect hardware faults. For those concerns, use the appropriate tool — and combine results, do not substitute.

License

Dual MIT / Apache-2.0.