Verified Rust for low-level systems code

Original Article ↗ Hacker News Discussion ↗

Formal verification for low-level Rust is gaining traction, with tools like Verus using SMT solvers to prove properties such as memory safety and liveness of complex systems (e.g., Kubernetes controllers) that are hard to cover with tests alone. Commenters compare Verus to alternatives like Kani, Dafny, Coq, Lean, and SPARK, noting trade-offs between automation, expressiveness, required annotations, and accessibility for non-experts. The thread also branches into zero-knowledge proofs and their current niche but growing role in areas like blockchains and privacy-preserving cloud or data-processing workflows, where high computational overhead remains a key barrier.

SMT, SAT, and TLA+

  • SMT solvers search for counterexamples to logical constraints or prove none exist, giving program-level correctness guarantees under a spec.
  • They build on SAT via CDCL(T): a SAT core plus theory solvers (arrays, arithmetic, etc.), learning from conflicts to prune search.
  • TLA+ can both brute-force finite state spaces and use SMT backends like Apalache; encoding language constructs soundly into SMT is subtle and tool-specific.

Verus, Rust, and Other Tools

  • Verus extends Rust with “ghost” code and specifications, verified via SMT. It currently wraps whole modules in a proc macro and uses a custom fork of rust-analyzer for IDE support; some wish for lighter attribute-based syntax like Creusot.
  • Comparison to Kani: Kani is a bounded model checker good at bug-finding with few annotations; Verus (like Dafny, F*, VCC) aims at full correctness proofs with many annotations.
  • Suggestions for incremental adoption in plain Rust: use debug_assert or contracts crates, possibly checked by tools like MIRAI or Prusti.

Verifying vs Proving, and Accessibility

  • Most commenters treat “verifying” and “proving” as synonymous; some distinguish “verification” as including spec-writing and “proof” as the logical derivation step.
  • Several note that formal verification for real code is still hard: tools are brittle, proofs often 5–20× the size of the code, and reasoning about unbounded loops/recursion is challenging.
  • Hardware verification is seen as more mature and economically justified; software lags due to lower perceived cost of bugs.
  • Recommended learning paths include Hoare logic, Software Foundations (Coq), Dafny, Why3, Coq/Lean courses, and high-level blogs on correctness.

Use Cases and Experience

  • Verus has been used to write formally verified Kubernetes controllers, proving liveness properties (“eventually reconcile to desired state”) under failures and concurrent edits—behaviors that are essentially untestable exhaustively.
  • Verification is contrasted with unit tests and deterministic simulation: tests/sample executions vs guarantees over all executions.

Zero-Knowledge Proofs Digression

  • ZKPs are explained as proving a statement (e.g., correctness, knowledge of a secret) without revealing underlying data.
  • One camp views ZKPs as currently niche and expensive, with unclear “killer apps” outside crypto.
  • Others argue they are already useful in blockchains (privacy, rollups, succinct verification) and may enable secure cloud computation, safe use of proprietary binaries, or privacy-preserving analysis of sensitive datasets.
  • A long subthread debates whether ZKP-based cloud use can ever be economically preferable to in-house racks; opinions sharply diverge, with no consensus.