The following pipeline is a proof of concept for verifying Calyx -- a hardware design language -- verification tools using a Kleene Algebra framework (aided by the already existing HardKAT project). It's a common occurrence among developers that while attempting to implement more robust formal methods to verify their domain specific languages -- specifically those of the form of symbolic execution algorithms -- it tends to be difficult to reason about. The main issues we seek to tackle in this project are:
- Ameliorate the issue of depending on various approximations and heuristics in symbolic execution algorithms, which can lead to less precise results.
- Help developers understand non-carefully implemented algorithms, which might produce non-rigorous results.
(Specify later)
- Install Rust and set up a development environment.
- Set up the Calyx compiler infrastructure
- Set up a subset of the Calyx symbolic repo