Yep. You can see the source here for example.
The issue with NonlinearVariationalFormulation is that it hides a lot of the actual maths that goes on behind the scenes. The symbolic Gateaux derivative computed by derivative(F, u) implicitly constructs a trial function based on the space in which u is defined yielding a bilinear formulation. You can specify it yourself if you need to as the optional third argument (documentation here).
You may get a better idea of what’s going on by taking a look at this. Or moving to dolfinx which houses the latest developments of dolfin (old dolfin is now very old). dolfinx is far less implicit. In (subjective) order of increasing complexity the following dolfinx demos solve nonlinear problems: