Verified Rust for low-level systems code

Original Article ↗ Hacker News Discussion ↗

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.