While the other two answers referred to very interesting connections of topos theory and quantum physics I think the following is going more into the direction the OP was imagining: In non-commutative topology one considers quantales, which are, roughly, an axiomatization of what you get when you replace open sets with projection operators - in particular intersection of open sets becomes composition of operators and does no longer have to be commutative. Here a few approaches to this idea are listed. One short definition is: A quantale is a monoid object in the monoidal category of lattices.
One can define sheaves over quantales (e.g. as done by Miraglia and Solitro in this article, or by Mulvey and Nawaz in this nicely written paper) and the categories of such sheaves would be the analogon to the notion of Grothendieck topos (but: to my knowledge no Giraud type characterization of such categories is known, let alone an elementary one). One can interpret logic in such categories, as e.g. done by Coniglio here for the Miraglia/Solitro setting.
In some ways such categories of sheaves over quantales connect back to actual topos theory as for example seen in the last corollary of the above Mulvey/Nawaz paper and more impressively in this article by Pedro Resende.
Edit: After having looked into the article pointed out by Urs Schreiber I would like to add a comment on what the authors see as drawbacks of quantum logic. They write that, on the logical side, quantum logic is not distributive and thus "difficult to interpret as a logical structure", that no satisfactory implication operator has been found "so that there is no deductive system in quantum logic" and that no satisfactory first order quantum logic has been found.
I cannot judge what would be satisfactory, but Coniglio's interpretation linked to above has an implication operator and first order quantifiers. In any case, deduction systems can be built without implication operators being present inside the language, one just has to devise rules which say when one can infer a formula from a set of hypotheses (this is done in many nonclassical logics). The non-distributivity presents undeniable and annoying technical difficulties, the difficulty to interpret a non-distributive system "as a logical structure" on the other hand may be a matter of reading it in an appropriate way, see the next point.
The authors also see a physical drawback: They see the law of excluded middle $x \vee x^\bot = 1$, valid in quantum logic, as not reflecting the probabilistic spirit of quantum physics, because there it is not the case that either a proposition $x$ or its complement $x^\bot$ are true - they both may have intermediate "degrees of truth". I think an answer to this is that the interpretation of $\vee$ should not be that one of its arguments is true, but rather that its arguments together span the space of all possibilities. Non-distributivity then makes some sense also.
In a similar vein many things in intuitionistic logic make more sense if one interprets it as talking not about the truth of assertions but about whether they are known or provable (and an observer-centered perspective on quantum physics seems very appropriate). So the choice of an underlying logic is the choice of a point of view. Maybe one can see the two topos approaches and the quantale approach as talking about quantum physics from different perspectives - one could even consider creating a bigger formal language containing the connectives from both interpretations and allowing to relate the several points of view (giving a formal semantics for this language might be quite a challenge, though).
Disclaimers: 1. My background in the things discussed above lies in categorical and non-classical logic - my knowledge of quantum physics is quite superficial. 2. Although I jumped to the defense of quantales here, I really like both topos approaches...
I doubt any answer will be satisfactory. My opinion is that we are still very far from a mathematical justification. If we accept the mathematical foundations of quantum mechanics, and if we make the approximation that the nucleus of the atom is just one heavy thing with $N$ positive charges, then the motion of the $N$ electrons is governed by a linear equation (Schrödinger) in ${\mathbb R}^{3N}$. The unknown is a function $\psi(r^1,\ldots,r^N,t)$ with the property (Pauli exclusion) that it has full skew-symmetry. For instance,
$$\psi(r^2,r^1,\ldots,r^N,t)=-\psi(r^1,r^2,\ldots,r^N,t).$$
In practice, we look for steady states $e^{i\omega t}\phi(r^1,r^2,\ldots,r^N)$. Then $\omega$ is the energy level.
Because of the very large space dimension, one cannot perform reliable calculations on computer, when $N$ is larger than a few units. One attempt to simplify the problem has been to postulate that $\phi$ is a Slatter determinant, which means that
$$\phi(r^1,r^2,\ldots,r^N)=\|a_i(r^j)\|_{1\le i,j\le N}.$$
The unknown is then an $N$-tuple of functions $a_i$ over ${\mathbb R}^3$. Of course, we do not expect that steady states be really Slater determinants; after all, the Schrödinger equation does not preserve the class of Slater determinants. Thus there is a price to pay, which is to replace the Schrödinger equation by an other one, obtained by an averaging process (Hartree--Fock model). The drawback is that the new equation is non-linear. Such approximate states have been studied by P.-L. Lions & I. Catto in the 90's.
Update. Suppose $N=2$ only. If we think to $\phi$ as a finite-dimensional object instead of an $L^2$-function, then it is nothing but a skew-symmetric matrix $A$. Approximation à la Slater consists in writing $A\sim XY^T-YX^T$, where $X$ and $Y$ are vectors. In other words, one approximate $A$ by a rank-two skew-symmetric matrix. The approximation must be in terms of the Hilbert-Schmidt norm (also named Frobenius, Schur): this norm is natural because of the requirement $\|\phi\|_{L^2}=N$. If $\pm a_1,\ldots,\pm a_m$ are the pairs of eigenvalues of $A$, with $0\le a_1\le\ldots\le a_m$, then the best Slater approximation $B$ satisfies $\|B\|^2=2a_m^2$, $\|A-B\|^2=2(a_1^2+\cdots+a_{m-1}^2)$. Not that good. Imagine how much worse it can be if $N$ is larger than $2$.
Best Answer
The question is a little unclear --- you want something axiomatic but not rigorous? Anyway, if you don't care about rigor and you like Dirac deltas, I don't think there's any better place to start than Dirac's Principles of Quantum Mechanics. Then if you want to understand the connection to $L^2$ spaces and the spectral theorem, I'd recommend Mathematical Foundations of Quantum Mechanics by von Neumann. The notation is out of date but the exposition is excellent.