Overview¶ Development of KeY itself¶ Infrastructure¶ Coding Conventions Formatting Conventions Gradle Logging Documentation Dependencies¶ KeY uses the Docking Frames library to organize its UI. Important topics¶ GUI extensions Event listeners Proof loading / saving How to write new taclets SMT solver integration¶ Adding an SMT solver SMT Translation Counter example generation External projects¶ KeY as a library