Translation of Rust's core and alloc crates to Coq for formal verification

Original Article ↗ Hacker News Discussion ↗

Tool and Verification Approach

  • coq-of-rust automatically translates Rust (core/alloc) into Coq, avoiding earlier tedious and error‑prone manual translation of the standard library.
  • The tool works at Rust’s THIR level rather than MIR; THIR preserves more high-level structure (expressions/loops) but is less compact and stable.
  • Loops are represented via a special primitive in a monad; proofs reason over finite execution traces and currently assume deterministic, non‑concurrent programs.

Trust, Bootstrapping, and Translation Correctness

  • Several comments stress that automatic translation shifts trust to the translator and to rustc’s frontend and type checker.
  • A suggested path is to translate coq-of-rust itself into Coq and prove that this Coq version preserves Rust semantics, then use it to re-translate its own source (a “diverse double-compilation” / translation-validation style argument).
  • There is recognition that rustc itself is unverified and very large; verifying it fully is seen as an enormous task.
  • Skeptics note that translation bugs could invalidate proofs (e.g., translating everything to a no-op), though others argue multiple, richer properties would typically expose such errors.

Handling Pointers, Mutability, and Unsafe Code

  • The current focus is on safe Rust; unsafe blocks are translated on a best-effort basis without full guarantees.
  • Pointers are generally treated as mutable pointers; borrow-checker information is not exploited, simplifying translation but pushing complexity to proof time.
  • Users can provide custom memory models/allocators (e.g., records for a few globals) to avoid heavy separation logic, at least for “simple” memory disciplines.
  • Immutable pointers can become immutable Coq values, making mostly-functional Rust code translate almost one-to-one.

Rust Safety Guarantees and Formalization

  • There is no complete source-level formalization of Rust yet; most formal work has focused on MIR and the unsafe semantics/type system.
  • One line of discussion asks whether verified core libraries plus no unsafe yields “formally verified” Rust programs.
  • Responses emphasize that:
    • Rust safety mainly targets memory safety and data-race freedom (under specific definitions).
    • Safe Rust can still have deadlocks, resource races, logical errors, and issues via OS/hardware behavior.
    • The goal of formalizing/verification of the standard library is to make Rust’s promised safety guarantees hold transitively for all safe code, not to rule out all bugs.

Cost, Scale, and Usefulness of Formal Verification

  • Multiple comments highlight that fully verifying large, real-world programs with interactive provers does not yet scale well; end-to-end verified systems are small compared to modern software.
  • There’s emphasis on cost–benefit: 100% assurance can be vastly more expensive than “99.9999%” assurance plus testing; verification should be targeted at critical components (e.g., unsafe core, kernels, crypto, avionics).
  • Specification writing is compared to writing property tests but harder; this is seen as a major practical blocker. Some advocate mixed strategies (selective formal proofs plus conventional testing and validation).
  • The thread notes that crypto/industry funding and hobby‑aligned philanthropy are currently important drivers for this kind of formal-methods work.