Rust’s borrow checker and type system rule out memory errors and a lot of API misuse. They do not prove that Nix snippets we emit are safe, that database invariants hold under randomised workloads, or that a path validator rejects every traversal attempt up to a bound. For those classes of bugs we add two complementary tools: proptest for property-based testing at normal cargo test speed, and Kani for bounded proofs on small, dependency-light crates.
What ordinary tests still miss
Integration tests are scenarios: they show one or a few paths work. Properties say “this must hold for every input matching a strategy” (proptest) or “for every input up to this size” (Kani). That is the difference between “we tried a few strings” and “we tried to break the assumption systematically.”
proptest: cheap, fast randomised coverage
We use proptest where we want high throughput and easy co-location with existing unit tests: gRPC validation, controller database invariants on in-memory SQLite, node registration, and similar. It is not a proof; it is a strong statistical search for counterexamples, and it runs in the same CI jobs as the rest of the suite.
Request and manifest validation paths (crates/controller/src/grpc/validation.rs and related).
Database CRUD and consistency checks (crates/controller/src/db.rs test module).
Node agent and registration flows where protobuf and identifiers need round-trip and boundary behaviour.
Kani: exhaustive within bounds, isolated in small crates
Kani model-checks Rust functions with bounded input sizes. Pointing it at the full controller binary is impractical: transitive dependencies (gRPC, TLS, SQLite, …) explode build time. We keep proofs in crates/kcore-sanitize (minimal dependencies) for security-sensitive string and path handling used when generating Nix and touching the filesystem.
Harnesses are gated so normal builds and clippy stay unchanged; CI runs Kani in dedicated jobs with pinned tool versions so results are reproducible across merges.
Why both, not one or the other
proptest scales to large modules and finds real bugs quickly with little setup. Kani upgrades specific pure functions from “we didn’t find a counterexample in N random tries” to “no counterexample exists within these bounds” — the right trade-off for injection and path-safety code where a single missed edge case is unacceptable. Together with TLA+ at the protocol level, they form a layered story: design models, then implementation properties, then proofs on the hottest pure code.
What this means in CI
Property tests run with the normal Rust test matrix. Kani runs under the formal verification workflow alongside TLA+ checks so a regression in any layer fails the same quality gate. For more detail on scope and roadmap, see the docs/formal-methods-and-verification.md document in the kcore repository.
https://kcorehypervisor.com
