machine-check
Tool for formal verification for machine-code
Common bug-finding approaches like software testing do not guarantee the absence of bugs. Formal verification can prove the absence of bugs, but the added description and proving complexity means it only tends to be used for critical systems. The current state-of-the-art tools are complex to use and hard to reason around when they fail. Machine-check aims to bring scalable yet intuitive formal verification to non-experts, leveraging the Rust ecosystem for description of digital machines including processors with machine-code programs loaded into memory. Ultimately, this should lead to increased reliability, safety, and security of programs and systems.
- The project's own website: https://github.com/onderjan/machine-check
This project was funded through the NGI0 Core Fund, a fund established by NLnet with financial support from the European Commission's Next Generation Internet programme, under the aegis of DG Communications Networks, Content and Technology under grant agreement No 101092990.
