The project files for the article: "Analysis and Formal Specification of OpenJDK's BitSet". The files contain: The KeY 2.10.0 jar executable, which is the prover used in this verification. A PDF of the article The original version of OpenJDK's BitSet class. Our edited version of the BitSet class, including formal specification and files necessary to load the code into KeY. A folder containing a number of completed proofs for simple methods from the BitSet class, as well as proofs for statements made in the article. Version 9:The README's in the following directories were expanded upon and/or clarified: \ (Main README) \Edited-BitSet \Proofs\Article-Assertions \Proofs\BitSet-Methods\Recorded-proofs Version 8:The BitSet.key file has now been extended with additional proof rules. Some of these proof rules are proven to be correct, with proofs in the proof folder.Using these additional rules, further methods have been proven. These, and recordings of the proofs being carried out, can be found in the proof folder.