# MechaTez: But du Stage

Ce stage s'intègre au projet MechaTez,
une bibliothèque FreeSpec dédiée à Tezos;
FreeSpec étant une bibliothèque de vérification développée par Thomas durant sa thèse
avec le soutien de Yann.
Le but du stage est d'appliquer Mechatez à
un cas d'utilisation concret
(typiquement, du code _critique_ du protocole économique de `tezos`)
afin d'évaluer sa pertinence dans toute la chaine de vérification d'une "feature"
du protocole.

On essaie donc d'utiliser MechaTez pour accomplir les étapes suivantes:
1. **comprendre** le code d'origine.
2. **spécifier** formellement la fonctionnalité et axiomatiser des hypothèses.
3. (re)**implémenter** le code d'origine en Coq.
4. **extraire** le code en OCaml pour l'intégrer dans la base de code de Tezos.
5. **comparer** le code généré avec le code d'origine.

Par exemple, on envisage de vérifier une librairie de skip-list codée en OCaml et utilisée par les SCORUs.

*contribution possible à *FreeSpec* et *coqffi*
*[mechatez-tm-traces](https://gitlab.com/nomadic-labs/tezos/-/tree/lthms@mechatez-tm-traces)