We present a framework for the development of certified static analyses using the Coq proof assistant. Several challenges will be addressed in this talk: How do we scale up the development of certified analyses to real languages (like bytecode Java)? Rather than formalise a single analysis, can we propose a family of analyses, parameterised by a precision/efficiency factor? We will propose some solutions to these questions through the example of an inter-procedural abstract interpreter for the Java bytecode language.