A sort of meta-comment on modal agents: I dislike the way they are presented mathematically, in terms of logical expressions and formulas. I think it would be simpler to use some model of computation, such as the lambda calculus, and then make the agents programs instead of formulas.

For example: We first define a runtime with an evaluator, (eval exp), and then a macro (prove exp) which hands the expression to a theorem prover, and returns true if and only if the theorem prover determines that the expression will terminate and the resulting value will be true. We can also use the special form (quote exp) to quote an expression, the replacement for declaring that some parts of formulas are implicitly encoded as Gödel numbers.

An agent becomes simply a function (agent my-code opponent-code). During testing against other agents, the runtime provides the agent with its own quoted code and the opponent's quoted code. (It's not strictly necessary to provide the agent's own code to itself, but doing so makes it easier to avoid having to write quines.) The runtime then evaluates both functions, to see who cooperates and who defects. Note that the agent might never terminate--which is an ambiguity that the mathematical presentation doesn't really resolve. One way to resolve this ambiguity is to say that such is undefined behavior, and the runtime may choose cooperate or defect as it wishes.

Some examples of agents in this framework, using a Lisp-like syntax:

;; DefectBot
(define (defect-bot my-code opponent-code)
  #f) ;; False stands for defection, true for cooperation

;; CliqueBot
(define (clique-bot my-code opponent-code)
  (equal? my-code opponent-code))

;; FairBot
(define (fair-bot my-code opponent-code)
  (prove `(,opponent-code ',opponent-code ',my-code)))

;; Payorian FairBot
(define (payorian-fair-bot my-code opponent-code)
  (define (implies X Y)
	(or (not X) Y))
  (prove `(implies (prove `(,my-code ',my-code ',opponent-code))
		           (,opponent-code ',opponent-code ',my-code))))

;; JustBot
(define (just-bot my-code opponent-code)
  (prove
	`(,opponent-code
	    ',opponent-code
		;; Play the opponent against a copy of FairBot's code, not JustBot's code:
		'(λ (my-code opponent-code)
		   (prove `(,opponent-code ',opponent-code ',my-code))))))

Maybe I should vibe-code this so we can have a tournament :)

Maybe any rank-zero modal agent that's unexploitable but cooperates with itself is FairBot (in the sense that its defining formula is equivalent to). Or if not that, what's the condition?

Up to modal depth 1, yes. I poked at this with Claude; at modal depth 1 a rank-0 agent is a Boolean combination of $\Box Q$, $\Box\neg Q$ and $\Box\bot$, and an unexploitable one must be GL-equivalent to one of $\bot$, $\Box\bot$, $\Box Q\wedge\neg\Box\bot$, $\Box Q$, and of these only $\Box Q$ cooperates with itself.

From modal depth 2 on it fails: $X:\ P\leftrightarrow\Box\Box Q$ is rank 0, cooperates with itself by Löb, and is unexploitable (soundness, applied twice), but is not GL-equivalent to $\Box Q$, and PrudentBot tells them apart, cooperating with FairBot and defecting against $X$, since cooperating with $X$ would need $\mathrm{PA}{+}1$ to prove its own consistency. FairBot over $\mathrm{PA}{+}1$ and $\Box^kQ$, $k\ge3$, are further counterexamples.

Maybe any rank-zero modal agent that's unexploitable but cooperates with itself is FairBot

Can you elaborate on what "rank-zero modal" mean? (unexploitable = (C, D) outcome does not happen?)

"If there is a proof that outcome of the game of me and this opponent is (D,C) under 1000 symbols, then I defect, otherwise I run fair bot condition" -- is this non "rank-zero"?