Is Lebesgue/Borel non-measurability actually caused by non-uniqueness? In ZFC, every construction of a Lebesgue or Borel non-measurable set uses the axiom of choice. None of them that I've seen use choice to define a unique set, even though it's entirely possible to do so (e.g. under the AoC, if $\kappa = |A|$ is the cardinality of set $A$, then $\kappa$ is unique). So I've been wondering lately whether the strength of the AoC is enough by itself to construct a non-measurable set.
Here's an attempt at a specific question. In the language of set theory (first-order logic with equality extended with the ZFC axioms), is there a formula without parameters that identifies a unique, Lebesgue/Borel non-measurable set?
 A: The other answers are excellent. But since you have adopted such a strong notion of definability, let me augment them with a positive observation. 
The fact is that any particular set can be made definable without parameters in a forcing extension of the universe $V$. Indeed, there is a single definition $\varphi(x)$, such that for any set $A$ at all, there is a forcing extension $V[G]$ in which $A$ is the unique set such that $\varphi(A)$. Furthermore, one can arrange that the forcing extension $V[G]$ agrees with $V$ far beyond the reals, so that it has the same reals, the same sets of reals, the same measurable sets and so on for quite a long way. 
In particular, there is a single definition such that for any non-Lebesgue measurable set $A$ that you favor, there is a forcing extension $V[G]$, an alternative set-theoretic universe, in which $A$ is defined by $\varphi$ and still non-measurable there. 
Let me explain the proof. Fix any set $A$. Let $\kappa$ be the cardinality of the transitive closure $\text{TC}(\{A\})$. Thus, there is binary relation $E$ on $\kappa$ for which $\langle\kappa,E\rangle\cong\langle\text{TC}(\{A\}),{\in}\rangle$. This isomorphism is unique, since it is precisely the Mostowski collapse. Let $E_0\subset\kappa$ be the set of ordinals coding pairs in $E$. In the style of Easton's theorem, let $\mathbb{P}$ be the forcing notion coding the GCH pattern on the regular cardinals above $2^{\aleph_0}$ to first have a block of length exactly $\kappa$ on which the GCH holds, and then an violation of GCH and then a sequence of length $\kappa$ on which the GCH pattern on the regular cardinals matches the elements of $E_0$. In the resulting forcing extension $V[G]$, the cardinal $\kappa$ and the set $E_0$ and hence $E$ and hence $A$ are definable without parameters. Because the forcing is sufficiently closed, it does not adds new reals or sets of reals and it does not affect measurability. So in the extension, the set $A$ is definable by the formula $\varphi$ that expresses the decoding of the GCH pattern to $E_0$ and hence $E$ and hence $A$. This coding idea is due originally to K. McAloon. 
The conclusion is that there is a kind of universal definition $\varphi$, which can serve to define any object at all, if only you apply the definition in the correct set-theoretic universe.
A: There is no simple formula that invariably describes a set of reals which is not Lebesgue measurable. The reason is that the existence of certain large cardinals imply that all simply definable subsets of $\mathbb{R}$ are Lebesgue measurable.
For example, if there are infinitely many Woodin cardinals with a measurable above, then $L(\mathbb{R})$ satisfies the Axiom of Determinacy and hence all sets in $L(\mathbb{R})$ are Lebesgue measurable. Here, $L(\mathbb{R})$ is the smallest transitive model of ZF that contains all the ordinals and all the reals; this universe contains all the projective sets and much more.
It seems that the situation is hopeless, but this is not quite true. There has been a lot of recent research which shows that the existence of definable wellorderings of $\mathbb{R}$ is not incompatible with some of the largest cardinals we know. However, the definition of these wellorderings of $\mathbb{R}$ is necessarily very complex.
A: Concerning Borel measurability, it was already pointed out that there is an explicit formula s(x) such that ZFC proves "The set { x in R: s(x) } is not Borel". 
(This is not true for ZF, as was pointed out elsewhere.) 
Concerning Lebesgue measurability, ZFC neither proves nor refutes the following: 

There is an OD-definition (or: OD(R)-definition) of a subset of the reals which is non-measurable. 

There is a slight fuzziness here, because there are many non-equivalent notions of definability; OD(R)-definability is perhaps the most prominent and useful.
But an explicit formula can be given: 
There is a formula phi(x) in the language of set theory (without parameters) such that ZFC neither proves nor refutes 

"The set { x in R : phi(x) } is non-measurable".

In fact, phi(x) can be of a rather simple form ($\Delta^1_2$, as you remarked above). Here is an abbreviated version of phi: For each real number x, let $x_1$ be the number obtained from x by deleting all even decimal places, $x_2$ by deleting all odd decimal places (do what you want for the countably many reals where this is not well-defined). This defines a measure-preserving Borel map from $\mathbb R$ to $\mathbb R\times \mathbb R$.  Now consider the set M of all reals x for which there is some $\alpha$ such that $x_1\in L_\alpha$, but $x_2\notin L_\alpha$.   ZFC does neither prove nor refute that M is Lebesgue-measurable. 
(I think that the fact that ZFC does not prove that M is measurable is already due to Gödel.) 
A: http://en.wikipedia.org/wiki/Solovay_model

"In particular Krivine (1969) showed there was a model of ZFC
 in which every ordinal-definable set of reals is measurable."

If all subsets of $\mathbb{R}$ are ordinal-definable then there is such a formula.
A: The answer below has been edited in light of other answers and comments.
There are all sorts of models of $ZFC$ in which every set is definable without parameters, including nonmeasurable sets; indeed a recent paper of Hamkins, Linetsky, and Reitz is devoted to such "pointwise definable" models.
Also, as pointed out in Theo Buehler's comment to the question, there certainly exist definable subsets of reals that are $ZFC$-provably not Borel.

However, the situation is completely different for measurability. The classical work of Solovay [using an inacessible] shows that there is a model of $ZFC$ in which every subset of reals in $OD(\Bbb{R})$ is Lebesgue measurable. Recall that $X$ is in $OD(\Bbb{R})$ if $X$ is definable with parameters from $Ord \cup \Bbb{R}$.

As pointed out in Demer's answer, Krivine [without an inaccessible] provided a model of $ZFC$ in which every ordinal definable subset of reals is measurable. Moreover, as shown by Harvey Friedman, here, there is a model of $ZFC$ [which is a generic extension of Solovay's model] in which the following property holds:

(*)  Every equivalence class of sets of reals modulo null sets that is in $OD(\Bbb{R})$
consists of Lebesgue measurable sets.

Note that (*) implies that no non-measurable subset of reals in definable, since if $X$ is any definable subset of reals that is not measurable, then the equivalence class $\[X\]$ of $X$ modulo null sets satisfies the following two properties:
(1) $\[X\]$ definable,
(2) No member of $\[X\]$ is measurable.

So, to sum-up, the answer to the question for Lebesgue measurability is negative, i.e., there is no formula $\phi(x)$ in the language of set theory for which $ZFC$ proves "there is a unique nonmeasurable subset of reals satisfying $\phi$".
However, if $ZFC$ is strengthened to $ZFC+V=L$ then such a formula does exist, as pointed out in Goldstern's answer.

