16
Verus: Verified Rust for low-level systems code (github.com)
submitted 6 months ago by armchair_progamer@programming.dev to c/formal_methods@programming.dev
1 comments fedilink hide all child comments

Another, very similar verified superset of Rust is Creusot. I'm not sure what the benefits/downsides of each are besides syntax tbh.

This is also similar to Kani which also verifies Rust code. However, Kani is a model checker like TLC (the model checker for TLA+), while Verus and Creusot are SMT solvers like Dafny.

Interestingly, Verus (unlike both Kani and Creusot) has its language server, which is a fork of rust-analyzer (verus-analyzer).

top 1 comments
sorted by: hot top controversial new old
[-] arendjr@programming.dev 2 points 6 months ago

Wow, I really like their macro syntax! That seems very approachable to someone who usually doesn’t formally verify their code :)

this post was submitted on 05 May 2024
16 points (100.0% liked)

Formal Methods

163 readers
1 users here now

founded 1 year ago
MODERATORS
Ategon@programming.dev
synthetic_apriori@programming.dev