Verus seems to be exactly what I have been looking for! I discovered AllConcur[0] on HN a while back, and I wanted to port it to Go, but since it used TLA+ and C, and it was very confusing for me to understand how you can trust the implementation unless you can compile TLA+ to C.

I was talking to Gemini about comparing Verus to TLA+ and it said that TLA+ is usually used (for example) "to prove that a distributed consensus protocol is logically sound" but when I asked if Verus can do that too, it said yes. So Verus can be compiled and integrated with Rust, whereas TLA+ is used more for blueprint development that then guides the implementation in the mind of the implementer.

Seems awesome!

[0]: https://news.ycombinator.com/item?id=12357976

▲

pjmlp 2 hours ago | parent | next [-]

That is my pet peeve against TLA+ advocacy, the disassociation between a theoretical proof of a specific algorithm, data structures, and the actual implementation in production.

I rather push for tooling that allows code generation based on the formal proofs like FStart or Dafny, or is integrated with specific programming languages like SPARK, Frama-C or this Verus.

	▲	igornotarobot 18 minutes ago \| parent [-]
		You can write everything in Lean and generate an implementation. Given that LLMs can now generate Lean proofs, this does not seem to be prohibitively expensive anymore. The real issue with distributed algorithms is that they are hard to reason about, and reasoning about them at the code level does not make the verification problem easier, it makes it harder.

▲

japgolly 5 hours ago | parent | prev [-]

[dead]