Yes, of course, there is much research on mathematical rigor in quantum field theory. Of course, I don't know what "reasonable", "essentially different", and "realistic" mean to you, but I would say that there are "reasonable" approaches and that some of them do address "realistic" field theories. As an aside, "rigor" for its own sake is far from the primary goal of mathematical physics, as has been discussed many times here and on our sister sites. See for example http://theoreticalphysics.stackexchange.com/questions/107/the-role-of-rigor.

But, in any case, you mention QED, and more generally "realistic" quantum field theory almost certainly means Yang–Mills Theory + matter, as this is what appears in the Standard Model. Here there are deep open questions, like those related to the mass gap. But some parts are by now understood. One part in particular is the *perturbative* path-integral approach to Lagrangian field theory, where the deepest part of the story is that of *renormalization theory*. Kevin Costello's book does a good job, I think, of explaining to mathematicians what renormalization theory is, setting it within a language of homological algebra.

But you bring up Wightman's axioms and AQFT, suggesting that you are less interested in making rigorous physics-as-it-is-practiced, and more interested in axiomatizing its general structure. There is, of course, no consensus yet as to the correct axiomatization — almost all proposals have no nontrivial examples — but many structures seem to be common. There is a more flexible version of AQFT, called *factorization algebra* and detailed in Costello's book with Owen Gwilliam that I think goes a long way towards providing a basic framework. Certainly all physical theories will have more common structure than just being a factorization algebra; but it is very common that we write down an axiom system and then the examples that appear "in nature" are quite special.

I have yet to be convinced that the "Schrodinger" picture is a fundamentally correct one. This is the picture that underscores, for example, geometric quantization, and also the Atiyah–Kontsevich–Segal–etc picture of QFT (originally TQFT, but by now more general). Certainly this version of QFT is an interesting mathematical structure to study, but it arises from the "Heisenberg" picture underpinning factorization algebras only because *sometimes* certain algebraic objects have unique, or at least canonical, irreducible projective representations.

Finally, I want to make one more comment concerning the success of perturbative and some nonperturbative QFT. Namely, almost every QFT that has been written down has been described in "path integral" formalism in some sense or another. Certainly this is true of the perturbative field theories in Kevin's book. But probably "having a path-integral description" *is not* fundamental to the notion of QFT. In a related way, "having a classical limit" *is not* fundamental. I highly recommend Dijkgraaf's Les Houches notes; this point is made in Section 2.2.

**Edit:** The OP has clarified the question to ask about how *nonlinear* quantum field theory can lead to the *linear* algebra of Hilbert Spaces. I think this is part of a standard confusion with the picture as developed of quantization, and what are "quantum spaces". The short answer is that a decent notion of "quantum space" *is* a Hilbert space with some extra structure (e.g. a "spectral triple" of Connes et al). For the long answer, I will restrict to (nonlinear) quantum mechanics, which is the nonlinear quantum sigma model in one dimension.

The most basic form of quantum mechanics, after Feynman and well-tuned to be portable to qft, comes from the following picture. You are given a classical configuration space, which is an abstract manifold with some geometry (a metric to define "mass", a 1-form to define "external magnetic potential", a function to define "external electric potential", etc.). This geometry in particular determines for you an "action functional", which is a function on the paths in this manifold. Now you define a "quantum algebra of observables" as follows. There is a bijection between quantum observables and classical observables, where "classical observables" are functions on the tangent bundle to your space, aka the phase space – so observables are functions of position and velocity. But the quantum algebra has a much richer algebraic structure than the commutative algebra of functions. Namely, given two functions $f_1$ and $f_2$, their product depends on three numbers $(t_1, t_2;t_3)$, and is:
$$ (f_1\star_{(t_1,t_2;t_3)} f_2)(x,v) = \int_{\text{paths }\gamma\text{ s.t. } (\gamma,\dot\gamma)(t_3) = (x,v)} f(\gamma(t_1),\dot\gamma(t_1)) \ f(\gamma(t_2),\dot\gamma(t_2))\ \exp(\text{action}(\gamma)) $$
The associativity of this algebra is somewhat subtle, and depends on the times. You should really think of this as "$f_1$ inserted at time $t_1$ multiplied by $f_2$ inserted at time $t_2$, measured at time $t_3$". There is a straightforward way to evolve a function inserted at some time $t_1$ to a *different* function inserted at any other time $t_3$: namely multiply $1$ at an arbitrary time $t_2$.

Now you can do the following. Since we can evolve functions, $t_3$ isn't much data – let's just decide $t_3 = (t_1 + t_2)/2$, say. Now let's just consider those situations when $t_2 = t_1 + \epsilon$ for very small epsilon. Dividing by $\epsilon$ and taking a limit, you get a usual associative noncommutative algebra.

There is a general notion in mathematics that a "space" is the same data as its (commutative) algebra of functions. Similarly, you can *define* a "noncommutative space" to be the same data as a noncommutative algebra of functions. Since we're doing integrals, the functions we're working with are the types of functions that appear in measure theory and functional analysis, rather than in geometry. Just knowing the algebra of measurable functions on a manifold only tells that manifold as a measure space, and all measure spaces are isomorphic, so you should also remember some data of the smooth structure and metric and so on. Similarly, the algebra you most naively get out of this construction doesn't know a lot; the extra data is that of a "spectral triple".

More precisely, algebras like to have representations, and the algebras of functional analysis like to be represented on Hilbert spaces. For QM (but not for higher-dimensional qft), this Hilbert space is essentially unique (similarly to the way that "the" measure space is essentially unique). The extra structure is what makes it "curved". In the case at hand, this essentially-unique Hilbert space arises in many ways: for example, the action picks out a symplectic form on the tangent bundle to your configuration space, identifying it with the cotangent bundle, and you can choose a way to identify functions on the cotangent bundle with differential operators, and then that algebra of differential operators can be naturally identified with the algebra we have constructed; in this way, the algebra acts on "wave functions" on your configuration space.

Is this a linear space? Not really. I've already mentioned one way that thinking of it as linear is wrong (it forgets the geometry). Another is that the representation is really projective, so the actual space of states is more like the space of lines-through-the-origin in the Hilbert space than the space of points. Really, this linear/nonlinear dichotomy is about like saying of your manifold "Manifold, I would rather you be linear, so I'm going to allow some linear combinations of your points".

I hope that helps clarify some things, and in particular the Schrodinger/Heisenberg dichotomy I alluded to earlier.