This tool is built on composition of MicroTESK tool and AstraVer versions of Frama-C and Why3 tools. The main purpose is deductive verification of the machine code by high-level language function contract specification.


This instruction uses RISC-V as example of target processor.

  1. First, install MicroTesk (version from branch mir) tool using instruction [[]] . Pay attention for setting up $MICROTESK_HOME environment variable and installing cvc4 1.6 smt-solver;
  2. Download or clone RISC-V nml model from this repository [[]]. Then compile and generate it using MicroTESK (see instruction above);
  3. Add cvc4 to your $PATH;
  4. Next, install AstraVer toolset using instruction [[]] . Following this instruction you will also install opam than would be used for installing other dependences;
  5. Install grep:
    sudo apt-get install grep
  6. Install readelf:
    sudo apt-get install binutils
  7. Install Yojson :
    opam install Yojson
  8. Install ocaml-containers :
    opam install containters
  9. Optional install gcc for riscv form this repository:;
  10. Next download source code of MicroVer modules:
    git clone
  11. Use make for compiling source code;
  12. Use make install for installing machine code specific Why3 modules, theories and drivers.


  • Use script for verification of the machine code.
    Script usage is .\ model_id file_name.elf file_name.c func_name where:
    model_id is riscv
    file_name.elf - address of executable file that contains target machine code
    file_name.c - C file that contains C code + ACSL specification of the verification object
    func_name - name of the target function.
  • Use script for reusing results of the previous run.
    Script usage is .\ model_id func_name where:
    model_id is riscv
    func_name - name of the target function


Tests are placed into the "microver/tests" directory. File test.c contains some common functions, that can be used for running the system. File riscv.elf compiled from the test.c using gcc for RISC-V. For example you can run this:

for verification on abs function:
./ riscv tests/riscv.elf tests/test.c abs_1

for verification on function with loop:
./ riscv tests/riscv.elf tests/test.c x2


  1. The script creates a build dirrectory called "build_<func_name>". This dirrectory contains:
  2. <func_name>.bin - function machine code
  3. <func_name>.s - disassembled function
  4. <func_name>.bin.json - function CFG
  5. <func_name>.bin.smt2 - old version of smt-lib machine code representation
  6. <func_name>.bin.bb_<x>.smt2 - smt-lib representation of function basic blocks
  7. _current_machine.json - information about target architecture
  8. Theory.mlw - WhyML representation of function specification
  9. WP_parameter_<func_name>.smt2 - smt-lib representation of function specification
  10. fun_info.json - information for merging representations
  11. session.json - information about stack and positions of the local variables in machine code.
  12. <func_name>_merged - targets for solving, verdicts and counterexamples if possible.

Updated by Pavel Putro 9 months ago ยท 5 revisions