proofs with Std.Do

Stream: CSLib

[Jesse Alama]

My understanding is that Boole will be the language of choice for CSLib. Is there room for other approaches, too? In particular, is there any interaction between proofs about Boole programs and the forthcoming Std.Do framework?

[Clark Barrett]

Can you provide a pointer to info about Std.Do?

[Henrik Böving]

It's the FRO built do notation verification framework. It was originally developed here: https://github.com/sgraf812/mpl?tab=readme-ov-file#mpl and then merged into core not too long ago, there is some info in that readme about how it works and more ongoing work by Sebastian Graf at the FRO right now.

[Sebastian Graf]

I think the short answer to

In particular, is there any interaction between proofs about Boole programs and the forthcoming Std.Do framework?

Is: We (as in: the authors of Boole and me, as the author of Std.Do) do not yet know enough about each other's approaches.
I would hope that we can assess the question better once Boole is released and I have at least written a proper reference manual entry for Std.Do (it is currently in the "pre-release, use at your own risk" phase). I would be very excited to support CSLib with Std.Do!

[Alexandre Rademaker]

Where can we find the Std.Do reference manual? I would also be curious about reference to understand its implementation.

[Sebastian Graf]

There's no manual entry yet, that's why I need to write one. I think I'll make that a higher priority (higher than "avoiding exponential formula blowup", that is) given that it will be essential to sync up with the CSLib effort ASAP. In the meantime, this blog post gives a rough overview on how to use it: https://markushimmel.de/blog/my-first-verified-imperative-program/. There's also my kitchen sink test file that you can check out: https://github.com/leanprover/lean4/blob/master/tests/lean/run/doLogicTests.lean.

[Sebastian Graf]

There's now a tutorial for mvcgen with a compact section on how to extend and use it with custom monads.

[Eric Wieser]

Any chance of a verso copy?

[Eric Wieser]

Unfortunately it looks like lean has once again fallen victim to the highlight.js new language door being sealed shut, and so we have to contact every service using highlight.js and ask them to consider adding our language separately.

[Sebastian Graf]

Eric Wieser said:

Any chance of a verso copy?

Yes, but I wanted to get the content out before making it pretty and polished.

[Shaowei Lin]

I'm also interested in knowing how Boole and mvcgen will interact with each other. Aeneas and Loom also do something similar, but I hear that Son Ho (Aeneas) is planning to have support for mvcgen soon.

Should we think of all of them as different ways (instances of Monad?) that can generate verification conditions in pure Lean, so we can ignore which tool was used to get the pure VCs? Even so, I think the style of the VCs will vary from tool to tool, so the proofs that we write for the VCs may look quite different.

At BAIF and at Galois, we are trying to do Rust verification in Lean, and trying to build AI tools for the VCs which are generated. We are currently going with the Aeneas-to-mvcgen transpiler, but it would great to know which framework (Boole/mvcgen/Loom) to focus on, or at least what the long-term roadmap would be.

[Sebastian Graf]

Here's my summary as the maintainer of mvcgen:

• Hax builds on Std.Do and uses mvcgen to generate VCs.
• Son Ho of Aeneas is currently looking into using Std.Do in order to use mvcgen to generate VCs. Naïvely I would expect that not to be much more difficult than for Hax, however Aeneas has a sophisticated tactic support for its current VC generation mechanism that would need to be ported.
• Vlad Gladstein of Loom will work on generalizing Std.Do in Q1/26 so that Loom can build on it. We have sketched out how a viable generalization might work.
• Boole did not have a shallow embedding into Lean's do notation last I checked (which was a few months ago). I think it could make use of mvcgen/Std.Do iff they manage to define some kind of semantic translation from Boole into something that can have a WP instance (i.e., a Monad). I don't know enough of Boole and its future plans to judge whether such a translation exists.
• Same for Strata. It depends on the generality of the framework, I suppose.

Concrete answers for your questions:

I'm also interested in knowing how Boole and mvcgen will interact with each other.

Can't say. If anything, Boole is not Rust, so you are probably rather asking about Strata. And I have no idea there, either.

Should we think of all of them as different ways (instances of Monad?) that can generate verification conditions in pure Lean, so we can ignore which tool was used to get the pure VCs?

That would be great, yes. I'm optimistic for shallowly embedded languages (Loom, Aeneas, Hax). I'm not sure if this works out for deeply embedded languages. I hope it will, but I haven't seen examples yet. See "iff" above.

Even so, I think the style of the VCs will vary from tool to tool, so the proofs that we write for the VCs may look quite different.

That sounds likely. The generated VCs depend on the particular shallow embedding (i.e., denotational semantics).

We are currently going with the Aeneas-to-mvcgen transpiler, but it would great to know which framework (Boole/mvcgen/Loom) to focus on, or at least what the long-term roadmap would be.

I'm not sure if either competitor falls in the Rust-to-Lean fragment. The decision should be between Hax and Aeneas and I do not have advice here. It has been discussed before, though; see #Program verification > What is the connection between Aeneas and Hax?

[Bas Spitters]

Loom is similar to SSProve (in Rocq), in that both use the Dijkstra monad framework. We've been using SSProve as a backend for Hax successfully in:

1. Verification of PQ TLS (https://eprint.iacr.org/2025/980)
2. to connect Rust with Jasmin code for cryptographic primitives (Last Yard paper)
3. to verify a cryptographic voting smart contract written in Rust.
   https://hax.cryspen.com/publications/

@Sebastian Graf you looked at the Dijkstra monad framework, and decided to take another route. You documented your rationale somewhere. Could you remind us of it, and contrast it to Loom ?

[Shaowei Lin]

Thanks @Sebastian Graf ! This helps a lot! I'm looking forward to hearing more about how deeply embedded languages like Boole and Strata could build on mvcgen/Std.Do, when their developers are ready to discuss this.

[Shaowei Lin]

Thanks @Bas Spitters for highlighting the similarities between Loom, SSProve and Hax!

[Bas Spitters]

@Shaowei Lin to be sure, Loom is an implementation of the Dijkstra monad framework, the same one we've been using the last five years in SSProve. SSProve supports a relational logic, which is common for security proofs.
I don't think these are currently supported by Loom (I only looked quickly), but I think it could be added.
Hax is partially orthogonal in that it transforms industry rust code into a language friendly for proof assistants (similar to aeneas, in this respect as they share parts of the front-end).