kite42

Yea this project is complete vibe-coded crap. A lot of the lighthouses aren't in the correct locations and some or even missing.

All it does is dispatch proof obligations to an SMT solver like Z3. There is nothing special about Verus, it works in the same way other program verification frameworks like Dafny and Frama-C work - except it's for Rust. Most of this article presents nothing unique to Verus and is more of an advertisement for the authors research work and the other work AWS is doing.

Some of this stuff isn't really insightful.

> It’s only awkward if you make it awkward.

Or THEY make it awkward.

> Don’t make your problems other people’s problems.

Well, yea... Also don't attack other people, and don't steal from other people, ...

> Help others succeed, and they’ll help you succeed in the long term.

Hard no. Many will take advantage of your time and advice, and never return the favor. Choose wisely who you help succeed.

> Don’t let your expenses rise as fast as your income.

Once again, very generic. Don't spend more than you make.

On the other hand, some of this stuff is actually never mentioned but useful

> Keep a brag document

> Under-promise and over-deliver.