The typical way ODE and PDE numerical methods are tested is using something like the method of manufactured solutions; a more extensive report on validating large physics codes can be found here.
For an ODE solver, the basic idea for testing a method for solving
\begin{equation}
\dot{u}(t) = f(u(t))
\end{equation}
would be to pick a solution, say $u(t) = e^{-t}$, and then calculate what the source term $f$ should be using a symbolic algebra system. For this example, $f(u) = -e^{-t} = -u$. You can also calculate initial conditions and boundary conditions by direct substitution. Here, $u(0) = 1$.
There are GPL- and BSD-licensed symbolic manipulation programs out there that will take care of the algebra for you. In Python, for instance, there Sage and Sympy can each do symbolic manipulation.
Even though you say you'd prefer not to, testing explicitly for things like symmetry or energy conservation (to within a tolerance) is something also done in practice.
Alternative approaches exist, but they're typically impractical. For instance, you could use a computer assisted proof system like HOL Light or Coq to reason about your program, but the computer assisted proof would take an impractically long time to execute. The Flyspeck project aims to do a computer-assisted proof of Kepler's conjecture, and the computation is estimated to take roughly 2.5 years, which is longer in serial than some "hero" computations in high-performance computing. You could also use something like interval arithmetic to ensure that your results lie within a given range, but things like dependency effects would likely make the output intervals very large relative to the precision you want, and you could suffer from a lack of infrastructure (i.e., there aren't many libraries that do interval arithmetic, and these libraries don't necessarily implement enough of what an average nonspecialist might need to do, like, say, solve systems of nonlinear equations).
I gather from your remark about Cryptol that you might want to do some sort of computer-assisted proof. Based on the above, I wouldn't recommend it, but if it could be done efficiently, that would be a very interesting contribution to the numerical methods literature.