Yes, the code example you've given is exactly in the direction we're thinking. (Edit: thought it can't be verified yet.) We haven't documented the algorithm be

Yes, the code example you've given is exactly in the direction we're thinking. (Edit: thought it can't be verified yet.) We haven't documented the algorithm because it's not the unique part of what we're doing. It works in a very simple-minded way, analysing possible states. The interesting part is the insight that function interfaces are the boundary along which verification should take place. Applying this idea consistently we escape the combinatorial explosion which tends to plague efforts in this area, because every function can be verified by itself. Notably, Dafny recognised this point before us, and the earliest clear statement we can find regarding it is in Dijkstra's "Notes on Structured Programming", in his chapter "On a Program Model". You may find that illuminating read. I'm no expert on Clang/GCC and the new annotation syntax for C and C++, but from what I've seen it's not general enough for what we're trying to achieve in Xr0. The safety semantics which are expressed in annotations in Xr0 (see [0] for an example) get very detailed. [0]: https://xr0.dev/learn#initialisation-of-memory-and-the-clump https://xr0.dev/learn#initialisation-of-memory-and-the-clump