Nana

o Operations can be implemented directly in C or by generating
  debugger commands which do the checking and logging only if the
  application is run under the debugger. The debugger based calls
  require are very space efficient 0 or 1 bytes per call.
o Support for checking real time constraints.
o Support for assertion invariant checking including
	+ Space and time efficient at least versus <assert.h>
	  For example asserti>=0 uses 53 bytes on a i386 vs
	  an optimised nana call which uses 10 bytes per call.
	+ Checking can be turned on or off at compile or run time.
	+ The action taken when an error is detected can be modified
	  on a global and per/call basis.
o Support for logging printf style debugging including
	+ Logging can be turned on and off at compile or run time.
	+ Logging to files, processes or circular buffers in memory
	  with optional time stamping.
o Support for the quantifiers of predicate calculus forall, exists.
o Support for before and after state saving and checking x, x'.