Do we still need models of spectra other than the $\infty$-category $\mathrm{Sp}$? This question asked whether $\mathrm{Sp}$ is convenient in the sense of satisfying (in the $\infty$-categorical sense) a list of desired properties of Lewis in his 1991 paper (see there).
The answer given there is yes, provided one interprets Lewis's desiderata in the setting of $\infty$-categories.
Given that $\mathrm{Sp}$ is better behaved than all other existing models of spectra, are them still needed for the purposes of homotopy theory?

Here $\mathrm{Sp}$ means the $(\infty,1)$-category of spectra, not specifically the quasicategory of spectra.
(@Dmitri Pavlov requested clarification on the meaning of $\infty$-category. I meant quasicategory, but only because of ignorance: I don't know constructions of $\mathrm{Sp}$ other than Lurie's, and would be happy if someone could point me to references on this. Regarding the meaning of “$\infty$-category”, I believe the discussion would be more interesting if we do not restrict to quasicategories. (This should be a comment; see the edit summary))
 A: The question used the phrase "still needed." This is a very loaded term, and the answer that you give will depend very strongly on how you interpret it.


*

*If, as Dylan does, we interpret this as asking whether some theorems make it mathematically necessary to use one of these strict models, I suspect that the answer is ultimately no. My reason is a little different from Dylan's. Lima's thesis first introduced categories of spectra in 1958 or 1959. Since then there have been many, many models introduced (even Vogt's lectures from 1969 on Boardman's category give a table comparing 8 different ones, including those developed by Spanier and Whitehead). However, the operating principle is now this: a "model for the category of spectra" is something that is equivalent to Boardman's category of spectra; the core applications are to determining information about maps in the stable homotopy category, or about function spaces between objects. One possible interpretation is this: theorems about stable homotopy theory have already been theorems about the $(\infty,1)$-category of spectra by definition for several decades.

*If we ask, instead, whether some developments would not have happened without these strict models, I suspect that the answer is yes. The most prominent example that I can think of is, in equivariant stable theory, the notion of a strictly commutative G-ring spectrum. These encode strictly more structure than the "homotopical" version of a commutative ring spectrum. Now, in the decade after Hill-Hopkins-Ravenel, we have explanations that go back and explain that this is because the G-equivariant category extends to some kind of G-symmetric monoidal category. However, this doesn't alter the fact that the structure was discovered because the strict notion turned out to encode more information than the homotopical one. 

If you allow me unstable comments: topological commutative monoids, topological abelian groups, the Dold-Thom theorem on infinite symmetric products, and the Dold-Kan correspondence on simplicial abelian groups are all theorems that are about a strictly more rigid structure than the notion of "commutative monoid" from Higher Algebra. These are all tremendously important structures. It's not clear to me that they would have developed if we would have started from ground zero with a coherent version of the category of spaces.
However, we should not overlook the human question: whether the subject is easier to teach, learn, and understand using a concrete model. As of writing, I cannot see any way to answer this other than with a resounding yes. There is a good reason why definitions of spectra like those in Adams or Bousfield-Friedlander are still used by people entering the subject: even with care and attention to their subtleties, they can be learned and understood very quickly. With a strict symmetric monoidal model, you can define algebra and module objects with a couple of diagrams; someone who assumes they exist and have good properties can be working with them very quickly.
Asserting that things are just as easy to do with new models of higher categories overlooks the cost involved in learning how to effectively work with them. (This isn't new. For example, developing fluency with homotopy limits and colimits always took some effort, because they remove one of abstract algebra's most useful tools--dramatic and unapologetic overkill--now that "imposing a relation" has higher consequences.) I have seen groups of intelligent people fluent in this language stumped for some time trying to translate a basic fact of category theory into new terms. We cannot demand that those interested in stable theory must learn higher category theory. This is not yet material that can be easily black-boxed. (I say all of this as someone who, at least in recent years, has been converted.)
Not least, part of the problem is that it is difficult to appreciate the development of higher category theory before you have some familiarity with the problems that it solves (e.g. up to and including the old "permuting two circles" problem in stable theory). There are not really a lot of references yet that tell the story of why coherent category theory is a good idea in homotopy theory. This is just one of a series of expository problems that can be squarely laid at the feet of people in my generation and older, and it will hopefully get better as time goes on.
A: At the risk of starting some kind of (un?)civil war, let me expand on my comments.
First and foremost, let's address the interpretation of the question. The OP asks "do we need a model category of spectra". If we interpret need to mean "without a model category of spectra we are unable to prove our favorite theorems and make our favorite computations" I think the answer is straightforward: no we do not need it. As I said in the comments:


*

*Computations are largely done in the homotopy category, unless they use the existence of certain spectral sequences and extra structure that might act on them. However, to the best of my knowledge, all such spectral sequences together with whatever extra structure you like, can be constructed in the land of $\infty$-categories without mentioning any of the fancy model categories of spectra.

*I know of no homotopically meaningful result about spectra that requires one of the model categories of spectra. 


So it is cheating to say: "$\infty$-categories can't prove that such and such is a strict, point-set symmetric monoidal widget" because you can't even ask that question in the land of $\infty$-categories. The real question is: have we ever actually needed to know there is some strict, point-set model for these things? I have asked many people to give me an example. I have never heard of one. I am not arguing that model categories for every concept are never used. One usually needs, at some point, some model category presenting spaces and/or one presenting $\infty$-categories when setting up the foundations. I am just saying that, once those foundations have been built, we do not need to go and find model categories for everything else in the world.

Now, as often happens in these discussions, the conversation has turned to a different question entirely: Are there things that are easier to prove with model categories of spectra than with the $\infty$-category of spectra?
This is the sort of question addressed by Dmitri above.
For the most part, I think this is very subjective: we all have different backgrounds and tastes, and whatever is easiest for us personally is what we should use.
However, I want to point out a subtlety in the discussion of this question. Let me take as our example the same as Dmitri's: constructing the Eilenberg-MacLane spectrum associated to a dga. Here is what Dmitri says:

Yes, the Eilenberg–MacLane functor from the category of differential-graded rings to the category of symmetric ring spectra in simplicial sets is constructed immediately using the lax monoidal structure of the Dold–Kan functor, whereas the analogous construction in the quasicategorical world is far more involved.

But there is a fundamental mismatch between the two tasks. Implicit in the phrase "the Eilenberg-MacLane functor" is the idea that there is a somehow 'unique' one that satisfies some properties we want it to satisfy. (Otherwise both parties would have an easy time constructing a symmetric monoidal functor from dgas to spectra: just send everything to zero.)
So the model category theorist, in answering this question, gets to: (i) choose a model for what 'dgas' are, (ii) choose a model for what 'spectra' are, and (iii) choose a specific model for what they mean by 'Eilenberg-MacLane' spectra. Then they show their construction is some type of monoidal and hopefully that it produces familiar homotopy types when applied on familiar dgas. (By the way: if we're allowed to pick whatever model is convenient, why not just take $\mathrm{H}\mathbb{Z}$-modules and the right adjoint to smashing with $\mathrm{H}\mathbb{Z}$?)
But now, the burden is on the model category theorist to:


*

*Check that this particular construction can be appropriately derived.

*Check that this particular construction agrees with the other particular construction produced by some other model category theorist.

*Check that this particular construction has all of my favorite properties. And, if it doesn't, that it is equivalent through some zig-zag of Quillen equivalences to some other construction which does.

*In verifying (3), one must re-verify (1) and (2) for these new properties. 


For and example of (4): the Dold-Kan functor is not lax symmetric monoidal, but we would still like to know that a cdga gets mapped to an $\mathbb{E}_{\infty}$-algebra. (And, more generally, that a chain complex with an $\mathbb{E}_{\infty}$-structure gets mapped to an $\mathbb{E}_{\infty}$-ring). It is not really clear how to immediately deduce that with the set-up you give... and, if you did write down some explicit $\mathbb{E}_{\infty}$-algebra structure, you would then need to verify that everyone else that writes down an $\mathbb{E}_{\infty}$-algebra structure on some EM-functor equivalent to yours actually produced an equivalent gadget... and so on and so forth forever.
This becomes a very large enterprise. People writing down $n$-different explicit constructions in $n$-different model categories, comparing them, then realizing there is more structure on those constructions, and comparing those, etc. etc.
In the land of $\infty$-categories, you have to work harder to setup the theory but you prove stronger theorems. The functor $D(\mathbb{Z})_{\ge 0} \to \mathsf{Sp}$ producing Eilenberg-MacLane objects can be produced directly from universal properties of the left and right hand side as symmetric monoidal $\infty$-categories. It is then automatically characterized up to a contractible space of choices by various conditions, which provides automatic natural zig-zags of weak equivalences between whatever constructions you make with model categories that satisfy some list of conditions. Moreover, it automatically produces souped-up functors from algebras over any operad in $D(\mathbb{Z})_{\ge 0}$ to algebras over that same operad in $\mathsf{Sp}$. Finally, no computational strength is lost: all of your favorite spectral sequences and filtrations etc. arise from the fact that this functor preserves (homotopy) colimits and is easy to compute on free things.
Let me point out, also, that even having a characterization of this functor via universal properties helps you to check stuff like (4) above. It turns out that the space of ways to promote the plain-old EM-functor to an ($\infty$-)symmetric monoidal functor is contractible. So if some model category theorist goes and promotes their EM-functor to a lax symmetric monoidal one in two different ways, then they automatically know they agree up to some natural zig-zag of weak equivalences.

All of the above was about a specific example, but it is part of a larger point.


*

*The $\infty$-categorical setup allows us to characterize highly structured objects/categories/functors via universal properties and produce them via general existence results. You usually can't even state those universal properties with model categories.

*Computations with objects/categories/functors immediately follow from the characterization because eventually whatever you're doing is probably a bar construction and then, voila, you have a spectral sequence.

*It is often possible to promote constructions like this to even more highly structures constructions with minimal extra work.

*Comparison with any other specific construction, be they model categorical or $\infty$-categorical, is immediate from the universal characterization. Moreover, just the existence of a universal characterization of promoted versions of a construction produces non-obvious comparison results for constructions with model categories.

A: The original question has been answered in the sense that there are people who are confident to prove every statement about spectra they care about without recourse to models or model categories of spectra. (That they might argue with statements only known due to specific manipulations of simplices in the model of quasi-categories is a different question as this question is only about models of spectra and not about the use of models or model categories in general.) More precisely, Dylan has expressed this sentiment in the following sentence. 

I know of no homotopically meaningful statement about spectra that can’t be proven without using model categories of spectra.

I do not see the main purpose of spectra in making homotopically meaningful statements about them. Although I regret that my own work has often been rather far removed from it, I see it as one of the main purposes of spectra to facilitate computations of geometric interest. The things we start with a often not constructed in a particularly homotopical fashion. 
Example 1) The Pontryagin-Thom construction. Here we identify bordism groups of manifolds with the homotopy groups of a Thom spectrum and then use e.g. its homology and the Adams spectral sequence to actually compute these groups. The Adams spectral sequence of course works completely in the homotopy category of spectra, but how do I prove the Pontryagin-Thom theorem if I only know that spectra are the free presentable stable infinity-category on one object? If I am given a problem about topological spaces (even manifolds) it seems to very useful for me that I can use a sequence of pointed topological spaces with suspension maps between them to get a spectrum. 
Another nice thing about models is that you can perform very concrete geometric operations on your geometrically given objects, then check (e.g.) some cofibrancy and see that they coincide with homotopy invariant constructions. As a simple example: Say you are given a concrete topological space with a $G$-action and want to compute the $G$-homotopy orbits (or rather the quotient in the $\infty$-category of spaces). Then I can check in my model sometimes that the action is free and just perform a usual quotient, of which (e.g.) the homology groups are usually much easier to compute than of the homotopy orbits. A recent more sophisticated example of this philosophy is the following:
Example 2) For a topological group $G$, let's denote by $C_n(G)$ the space of commuting $n$-tuples of elements in $G$. In a recent paper, Gritschacher and Hausmann compute the homotopy groups of $C_n(O)$ by identifying the $C_2$-equivariant homotopy type of $C_n(U)$ with $\Omega^{\infty}(k\mathbb{R}\wedge (S^{\sigma})^{\times n})$. They check cofibrancy conditions, write down homeomorphism etc. -- i.e. they argue in a very non-$\infty$-categorical way. But how should one even start calculating the homotopy groups of a very concrete space without arguing first in models to translate it into something that can be described in a purely homotopical fashion?
I want to add that Gritschacher and Hausmann also provide a proof of real Bott periodicity in this fashion (essentially filling in details into a very short sketch of Suslin). Here the case is different as the K-theory spectrum of the symmetrical monoidal category of finite-dimensional real vector spaces has already an $\infty$-categorical sound to it. Is there a proof of real (or complex) Bott periodicity in a purely $\infty$-categorical style starting from the description of K-theory as above? 
Example 3) I think, similar points as above apply to the (equivariant) analysis of the homotopy groups of symmetric powers of spaces. See e.g. Schwede's article

It goes without saying that the $\infty$-categorical paradigm is extremely important and useful, especially for proving anything that can be formulated in purely $\infty$-categorical style - as Dylan said: even if there is a short-cut using models often the $\infty$-categorical argument buys you more. But I see arguing with models of spectra still as important if you start with something that is not given in $\infty$-categorical style, but rather as concrete topological spaces. 
A: 
Given that Sp is better behaved than all other existing models of spectra

No, Sp is not better behaved than other models.
The reason that it seems to be is because all operations in Sp
(e.g., Ω^∞, Σ^∞)
are (by construction) derived.
But if you derive the operations in any other model,
you will get exactly the same properties.

are them still needed for the purposes of homotopy theory?

As stated, the answer is obviously no.
(The underlying (∞,1)-categories are equivalent,
and arguably, this is the only thing that homotopy theory cares about.)
But if “needed” is interpreted in the practical sense,
then one can point out many situations where working
with strict models is much easier than with quasicategorical models,
and because of the various rigidification results
has exactly the same generality as quasicategorical analogues.
This especially concerns all sorts of situations that
in the quasicategorical world involve (co)Cartesian fibrations,
which includes, in particular, the treatment of monoidal categories and operads.
Quasicategories appeared (in HTT) when other models were much less developed
(e.g., the foundational paper by Barwick and Kan on relative categories
has not appeared yet), and today they are just one model out of many,
which has exactly the same foundational status as relative categories, simplicial
categories, etc.
Some models, like complete Segal spaces, have better theoretical properties,
other models, like relative categories, have a much better supply of examples.
In fact, quasicategories are typically constructed out of simplicial categories
or dg categories (typically with a model structure, see Lurie's books for many examples),
and given the fact that the underlying (∞,1)-categories of all these models are
equivalent, one may wonder why one should bother with passing to quasicategories at all.
To summarize, quasicategories are themselves a model:
a quasicategory presents an (∞,1)-category as an (∞,1)-colimit
over Δ^op of (∞,1)-categories given by finite chains of composable morphisms.
Such a presentation is often convenient to work with,
in particular, when doing theoretical computations.
But it is merely a presentation, and as such it will inevitably
become inconvenient at least in some situations (such as
those that require extensive use of (co)Cartesian fibrations).
Why cripple oneself with just one model, when other models
can be much better?
