The Algorand PoS consensus protocol assumes that honest nodes use so-called "ephemeral keys" (see Section 5.2 of the white paper). This implies they are supposed to "forget" part of their past state. A malicious node could choose not to forget their past state, thus making double-spend a possibility (assuming an adversary with majority of stake).

Therefore, the formal proof of security provided in the Algorand white paper does not resolve the nothing-at-stake problem, which is inherent to all PoS systems.