#+setupfile: publish.setup
#+title: Vericert

A formally verified high-level synthesis (HLS) tool written in Coq, building on top of [[https://github.com/AbsInt/CompCert][CompCert]].  This ensures the correctness of the C to Verilog translation according to our Verilog semantics and CompCert's C semantics, removing the need to check the resulting hardware for behavioural correctness.

* Features

The project is currently a work in progress, so proofs remain to be finished.  Currently, the following C features are supported, but are not all proven correct yet:

- all int operations,
- non-recursive function calls,
- local arrays and pointers
- control-flow structures such as if-statements, for-loops, etc...

* Content

- [[./proof/toc.html][Vericert Proof]]
- [[./documentation.org][Vericert Documentation]]