Some key design points:

• All such standard libraries will be enabled/disabled with a single switch, --use-stdlibs, which will be on by default but off by default in integration tests, to ensure that the language itself does not become dependent on these libraries.
• They will be pre-verified and built to one or more .doo files, which --use-stdlibs:true will add as implicit --library arguments.
• They will also be pre-compiled and added to the various runtimes. Users will be discouraged from directly referring to any thing in the runtime artifacts, as they are intended to only support Dafny code.