# Verus

23 Hacker News commenters recommended Verus and 4 criticized it, November 2025 to November 2026. It was recommended in 10 of 13 months. It meets the Hacker Approved badge rule.

**Verdict:** Lets Rust programmers prove code correct against specifications kept beside the implementation. Most common caveat: its verus! macro wrapping all code unsettles rust-analyzer and tooling.

## Why people recommend it

- Useful and impressive in practice (3 comments): "Verus is making our verification story extremely compelling" ([source](https://news.ycombinator.com/item?id=49743895)) "I uncovered a few interesting bugs this way." ([source](https://news.ycombinator.com/item?id=49611844)) "Genuinely impressive and massively useful." ([source](https://news.ycombinator.com/item?id=49747994))
- Integrates proofs with the Rust language (3 comments): "it has made me think deeper about the structure and semantics of Rust code" ([source](https://news.ycombinator.com/item?id=47871836)) "I think they found a nice way to integrate proofs with the language." ([source](https://news.ycombinator.com/item?id=50204026)) "It augments Rust with Z3 and is not a pile of unverified slop." ([source](https://news.ycombinator.com/item?id=48756316))
- Verifies the real implementation (2 comments): "couple the implementation and verification so you can't end up with a model that diverges from the actual implementation" ([source](https://news.ycombinator.com/item?id=48070790)) "You can use a refinement style system like Verus in which your spec is a very high level statement of system behavior" ([source](https://news.ycombinator.com/item?id=46658501))
- Works well with AI agents (2 comments): "I let the AI bang on the proof and trust the proof assistant to confirm it." ([source](https://news.ycombinator.com/item?id=47242168)) "agents are good at writing Verus proofs in a Rust code base" ([source](https://news.ycombinator.com/item?id=50086149))

## What people warn about

- Macro wrapping hurts tooling and builds (3 comments): "The macro system looks very nice if it doesn't slow down the normal build." ([source](https://news.ycombinator.com/item?id=49743221)) "a `verus! {}` macro wrapping everything was never gonna be a viable way forward" ([source](https://news.ycombinator.com/item?id=49333897)) "Verus wraps everything in its macro that makes rust-analyzer etc unhappy." ([source](https://news.ycombinator.com/item?id=47875468))
- Standalone language, not Rust-integrated (2 comments): "it's really cool just a tad sad that the rust eco-system didn't allow verus to be more streamlined" ([source](https://news.ycombinator.com/item?id=47872073)) "is a good start for the rust ecosystem, but it's essentially a standalone language today" ([source](https://news.ycombinator.com/item?id=49064650))
- Doesn't match clippy or Kani (2 comments): "seems like it needs more work to do the same thing clippy does" ([source](https://news.ycombinator.com/item?id=47871935)) "it doesn't seem to do the thing I love about Kani" ([source](https://news.ycombinator.com/item?id=46353313))
- Nothing new versus other verifiers (2 comments): "Even Verus itself doesn't really change this." ([source](https://news.ycombinator.com/item?id=49740508)) "There is nothing special about Verus, it works in the same way other program verification frameworks" ([source](https://news.ycombinator.com/item?id=49736104))

## Alternatives hackers recommend

- [SPARK Ada](https://hackerapproved.com/p/spark.md): 63 recommend
- [Dafny](https://hackerapproved.com/p/dafny.md): 24 recommend
- [F*](https://hackerapproved.com/p/f.md): 17 recommend

## Cite as

Hacker Approved, "Verus", https://hackerapproved.com/p/verus/ (counts from 1,795,640 Hacker News comments, November 2025 to November 2026).