This thesis introduces a formal approach to deriving VLSI circuits
by the use of correctness-preserving transformations. Both the
specification and the implementation are descibed by the relation
based language Ruby. In order to prove the transformation rules a
proof tool called RubyZF has been constructed. It contains a
semantical embedding of Ruby in Zermelo-Fraenkel set theory (ZF)
implemented in the Isabelle theorem prover. A small subset of
Ruby, called Pure Ruby, is embedded as a conservative extension of
ZF and characterised by an inductive definition. Many useful
structures used in connection with VLSI design are defined in
terms of Pure Ruby and their properties proved. The design process
is illustrated by several non-trivial examples of standard VLSI
problems.