verus-lang/verus
View on GitHub ↗ ★ 3,536 Rust
Verified Rust for low-level systems code
14 mentions on Hacker News by 12 people: 1 story, 13 comments · first 2024-05-04 · latest 2026-09-18
20082026
-
I'm interested in how to integrate formal verification with existing software libraries. For example, https://github.com/verus-lang/verus integrates proof with macro in Rust. What's the plan for Bend?
comment by txhwind · 2026-09-18 · in Bend – a language that blocks AI mistakes via proof and runs on GPUs -
…specs is probably the main skill a programmer in the future will need to get work done. Verus ( https://github.com/verus-lang/verus ) is a good start for the rust ecosystem, but it's essentially a standalone language today (with custom…
comment by gz09 · 2026-07-27 · in We have proof automation now -
It's https://github.com/verus-lang/verus It's not my own project, but it's doing basically the same thing you are doing which is why it is relevant.
comment by Eridrus · 2026-07-04 · in Show HN: Salt – a systems language with Z3 theorem proving in the compiler -
…Verus, I think, are trying to enable exactly what the author is discussing. Perhaps worth a look: https://github.com/verus-lang/verus
comment by twoWhlsGud · 2026-07-03 · in Local Reasoning for Global Properties -
How does this differ from https://github.com/verus-lang/verus
comment by Trung0246 · 2026-05-28 · in Creusot helps you prove your Rust code is correct -
…more optimistic about the verus approach, but I freely admit that's my builder bias speaking. [1] https://github.com/verus-lang/verus
comment by dgacmu · 2026-05-09 · in Can LLMs model real-world systems in TLA+? -
https://github.com/verus-lang/verus
comment by esafak · 2026-04-23 · in Verus is a tool for verifying the correctness of code written in Rust -
…the proof. But it's getting easier by the year and the LLMs are getting more useful as part of it. https://github.com/verus-lang/verus (1) You would have to state the consistency and conditional liveness properties directly, of course, as…
comment by dgacmu · 2026-01-17 · in Lies, Damned Lies and Proofs: Formal Methods Are Not Slopless -
…blocks create unverifiable boundaries Few of the tools can verify unsafe code is free of UB, e.g. https://github.com/verus-lang/verus . Also, since unsafe code should be small and well-encapsulated, this is less of a problem. > the trait…
comment by afdbcreid · 2025-10-05 · in A comparison of Ada and Rust, using solutions to the Advent of Code -
https://github.com/verus-lang/verus is similar tool for Rust (developed by previous heavy users of Dafny).
comment by mmoskal · 2025-06-03 · in Teaching Program Verification in Dafny at Amazon (2023) -
Related: Verus (verified Rust): https://github.com/verus-lang/verus It's aimed more at full systems verification (been used to build verified filesystems, kubernetes controllers etc...).
comment by lsuresh · 2025-03-17 · in Coq-of-rust: Formal verification tool for Rust -
Perhaps verus would be helpful to the op: https://github.com/verus-lang/verus
comment by meling · 2025-02-04 · in No-Panic Rust: A Nice Technique for Systems Programming -
…to intrinsic methods as pushed by type system advancements and projects like Verus [1]. [1] https://github.com/verus-lang/verus
comment by synchronousq · 2025-01-10 · in Formal Methods: Just Good Engineering Practice? (2024)