  Static verification relying on an automated theorem prover can be very slow
and brittle: since static verification is undecidable, correct code may not
pass a particular static verifier. In this work we use metaprogramming to
generate code that is correct by construction. A theorem prover is used only to
verify initial "traits": units of code that can be used to compose bigger
programs.
  In our work, meta-programming is done by trait composition, which starting
from correct code, is guaranteed to produce correct code. We do this by
extending conventional traits with pre- and post-conditions for the methods; we
also extend the traditional trait composition (+) operator to check the
compatibility of contracts. In this way, there is no need to re-verify the
produced code.
  We show how our approach can be applied to the standard "power" function
example, where metaprogramming generates optimised, and correct, versions when
the exponent is known in advance.
