What is JDefProg and How it works?

JDefProg is a set of tools that "extends" Java in a transparent way. Using a set of annotations let the developers declare constraints on the code such "this parameter should be not null" or "after this method is called this condition has to be true". One of the components of JDefProg (the Annotations Processor) check the code and signal errors directly in your favorite IDE. Then the code to enforce this constraints is generated automatically and inserted into the compiled class files. It can ben done in two ways: weawing the physical class file (so modifying them permanently) or modifying the classes at load time.

Is a tutorial available?

Yes, just follow the link. You can also just download the latest release: it contains the tutorial. The download page is here