What is a formal definition of a Fermionic quantum field? I could not locate a definition of Fermionic quantum field (like for an electron!) in even Kevin Costello's book, http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.382.4961&rep=rep1&type=pdf 
Can anyone help define this thing? And any such definition also has to make sense when the spacetime is a super-manifold. 
(Beyond how physics books define it as a plane-wave expansion with anti-commuting operator coefficients - there its very unclear as to how the spinorial structure is getting encoded or what exactly is the algebraic structure of this operator space from which these operators are coming - and how they can be defined to act on the Hilbert space of the QFT when this Hilbert space is defined in the "right way" as : the dual of an implicit vector space whose basis is assumed to be in bijective correspondence with the space of all possible classical configurations/values of all the classical fields - which need not all be Fermionic - in the underlying classical Lagrangian) 
 A: Unlike boson fields, the fermion fields do not posses a classical limit. This complicates their construction in a spacetime manifold. The approach developed by DeWitt is to introduce a "superclassical" limit, in which the fermion fields become anticommuting Grassman variables (by taking a Majorana representation the fields can be assumed to be real). This is explained on page 230 of DeWitt's book on Supermanifolds, or more extensively in Chapter 1 of Effective Action Approach to Quantum Field Theory.
A: One can define a Fermionic quantum field $\psi$ by postulating its algebra of anti-commutation relations
$$
  \{ \psi(f), \psi^\dagger(g) \} = (f,g), \qquad \{ \psi(f), \psi(g) \} = 0
$$
where $f,g \in \cal H$ are so called test-functions from a (one particle) Hilbert space. (Similarly, but less cleanly, one can choose a singular basis of Dirac delta distributions $f = \delta_x$, $g = \delta_y$ and obtain $\{ \psi(x), \psi^\dagger(y) \} = \delta(x-y)$.)
Then, one looks for representations of that algebra of which the Fock space is one but not the only one of the possibilities.
In the common Fock space representation $\psi$ is realized as an operator valued field of a Dirac (bi)spinorial type. Its properties, like spin, can be analyzed within the representation theory assuming Poincare invariance.
(There is no need for using plane-wave expansion, as you find in old physics books, as that approach is very limited.)
