What/Why?
Creusot is a verification framework for Rust, at the contrary of Serval, it operates at the language level, instead of assembly directly.
The problem we have with Serval are twofold:
- It is hard to use, we've spend a few semester project on that, I looked it up myself and still we don't know how to use it properly yet.
- It requires finite interface, which constraint our design, especially regarding resources reclamation.
Creusot might lift both of those constraints, at the cost of:
- Including the Rust compiler in the TCB.
- Requiring more code annotation.
How?
Just try to play with creusot a bit.
What/Why?
Creusot is a verification framework for Rust, at the contrary of Serval, it operates at the language level, instead of assembly directly.
The problem we have with Serval are twofold:
Creusot might lift both of those constraints, at the cost of:
How?
Just try to play with creusot a bit.