Comment by pas

The proof can be done on the whole code (in memory, incremental, etc), and then the modules emitted as dynamically loadable objects.