Formalizing self-propagating behaviour Since reading Ken Thompson's Reflections on Trusting Trust I am trying to formalize the idea of a program which mutates its own behaviour; specifically, a program that would be self-reproducing except that it would reproduce itself with a mutation. With this definition I wish to differentiate this kind of program from self-reproducing programs and will call them programs with self-propagating behaviour (due to the nature of propagating its own mutations). I am familiar with Hoare Logic, LTL, CTL, and CTL*, but am unsure what to use for the formulation since Hoare Logic requires a concrete implementation of a program and I am trying to represent not a program but a kind of program, and am also unsure if/how I could express this idea in LTL, CTL, or CTL*.
I don't have time for an elaborate answer right now, so here is just a quick braindump: Program logic does not restrict to concrete programs. Given e.g. a pair $(A, B)$ of pre/post-conditions, you can think of this pair as defining a set of programs

$$
\{ P \ |\ P\ \text{is a programs such that}\ \models A[P]B \}
$$

Here are a couple other references that might be useful. 


J. Von Neumann, Theory of Self-Reproducing Automata.
F. Cohen, Computer Viruses - Theory and Experiments.
S. Kramer, J. C. Bradfield, A general definition of malware.
G. A. Kavvos, Theories of Computer Viruses: 30 Years Later.
L. M. Adleman, An abstract theory of computer viruses.
G. Jacob, E. Filiol, H. Debar, Formalization of viruses and malware through process algebras.
J. L. England, Statistical physics of self-replication.


As the kind of program you envision is a form of meta-programming, I suggest also to look at this field (which is primarily implementation-driven and lacks substantial theory as of 2017). Here are some references, none of which is likely to be directly relevant, but will eventually lead to research that should be:


M. Berger, L. Tratt, Program Logics for Homogeneous Meta-Programming
S. N. Artemov, L. D. Beklemishev, Provability Logic.
G. Japaridze, D. de Jongh, The logic of provability.
S. Artemov, Explicit Provability And Constructive Semantics.
J. Alt, S. Artemov, Reflective λ-Calculus.