Posts by Tags

formal verification

Verification of Distributed System using Verus

less than 1 minute read

Published:

Verus is an open-source tool for formally verifying Rust programs. You write your executable Rust code alongside specifications (preconditions, postconditions, invariants) and optional proof code, and Verus uses automated SMT solvers to prove that the code satisfies those specs for all executions, without adding runtime checks.

rust

Verification of Distributed System using Verus

less than 1 minute read

Published:

Verus is an open-source tool for formally verifying Rust programs. You write your executable Rust code alongside specifications (preconditions, postconditions, invariants) and optional proof code, and Verus uses automated SMT solvers to prove that the code satisfies those specs for all executions, without adding runtime checks.