NB: a lot of the stuff still has much work to be done, but we're transitioning to working in the open :)
I'm currently focused on the language engineering side (though i was part of the early distributed replication effort, when we ported a verified raft code base to haskell, see https://github.com/cartazio/haver-raft . We ultimately didn't use that code base for a variety of reasons relating to how that verified alg was structured, but all the initial commits should be syntactically equivalent to the coq code in verdi raft, and all the follow on commits should be strictly syntactic transformations. https://github.com/uwplse/verdi is the associated coq development )
Anyway, to your question (carter focuses on the smart contract language, not the consensus layer): This is actually a semi-normal/expected thing in the case of a network partition. Say one node gets cut off, transitions to a candidate and achieves some high term (but potentially has an out of date log index). When it comes back online/partition ends, it will start spamming the rest of the cluster requesting votes.
What protects the rest from this or other faults is a combo of signed RPC's and extra logic (i.e. lazy votes). With sigs, chatter from someone who you don't have the key for (or invalid msgs generally) just get dropped + authorship is verified (Follower can't pretend to be some other node). With lazy votes the portion of the cluster in a good state basically chills (stays in same state, doesn't vote) until the Followers hit an election timeout (AE clears the lazy vote).
Of course you can still DoS the NIC or Haskell server, but the important thing to note is that this isn't meant for a public-facing deployment. It's designed for an internal network -or- inter-corp via leased lines/secured pipes setup. That's the whole point of Juno really... for enterprise applications bitcoin-class tech gives you more features than you need (at the cost of performance).
Tangaroa was a great first step, but we have internal fixes for a number of cases it didn't cover, issues caused by incomplete implementations and (I think) some novel ideas to give back... but I'm still finishing the paper on the enhanced/new (not sure what the line for that is) protocol and its implementation so it didn't make the cut for this release.
Significantly, this means it doesn't do a full BFT (which is ultimately application-specific), meaning it is possible to DOS with correct-but-spurious messages.
We are investigating ways to lazily verify SM results, which would necessarily be application specific. This opens the way for an application to code DOS resistance.