Formal Methods

175 readers

2 users here now

founded 2 years ago

MODERATORS

[email protected]

Verus: Verified Rust for low-level systems code (github.com)

submitted 11 months ago by [email protected] to c/[email protected]

0 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).

no comments (yet)

sorted by: hot top controversial new old

there doesn't seem to be anything here