As recently demonstrated by the AlphaDev algorithm, reinforcement learning can be used to generate assembly code that is more performant than a human implementation. However, there are no guarantees for the correctness of the generated code. Programs for simple tasks such as sorting short sequences of integers can be exhaustively tested, but this is not possible for more complex tasks. We describe how Dafny can be used to reason about the state of a machine during the execution of assembly code. This allows Dafny to verify that a given assembly program adheres to input-output constraints. The verification can be done automatically, without the need of human intervention. Therefore, Dafny can be integrated into the reinforcement learning process, and guide the agent to find efficient and verified solutions for complex tasks.