The Ruby programming language is typically not seen as a language that can be
formally verified. Our research attempts to bridge this gap by introducing novel
techniques to annotate Ruby programs with type specifications, contracts, and translate
them to statically verifiable components. We introduce a novel tool, RubyCorrect,
which uses these techniques to perform extended static checking (ESC) on Ruby
programs, as well as to generate executable test cases through symbolic execution.
These analyses serve to improve code quality and development productivity. We aim
to show that Ruby programs can benefit from existing static verification tools and
techniques if they are simply made available to Ruby developers.