I think a formalism for AMMs might go a long way toward making formal software development more straightforward. All the formalisms I am aware of pair some logic with some programming language, or worse a logic with an abstract model of a language, but implicitly or explicitly portions of architecture get dragged into the formalism as well, e.g. resulting in seL4 having differing levels of proofs for various architectures (arm, amd64, risc-v).

If instead we pair a logic with a parameterized (by cache coherency semantics, hardware protection and isolation levels, register layout, etc.) abstract machine model then it could presumably apply over multiple architectures and languages with derived specializations for each language.