\begin{abstract_eng}
Checking desirable specifications of software are important.
If it checks actual implementations, much better.

In this papaer, We propose two verification methods using meta computations which save original implementations.
On the hand method verify specification by enumerate possible states on programs.
We checked red-black tree specification using our meta computation library named Akasha, which override program executions exhaustively.

On the other hand method veriy programs with proofs.
Proposition and proofs have isomorphic relation to typed $\lambda$ calculus by Curry-Howard Isomorphism.
We define the CbC type system with subtype for proving CbC itself.
Agda proves properties of translated CbC programs using proposed subtype definition.
\end{abstract_eng}