The Details
This framework provides a set of tools for modeling and verifying properties of complex systems. It leverages modern formal verification techniques to ensure that system behaviors align with their specifications, particularly in safety-critical domains like avionics and automotive.
The Features
- Automated Property Checking: Quickly verify system invariants and safety properties.
- Support for Industrial Standards: Designed with DO-178C and other safety certifications in mind.
- Modular Design: Easily integrate with existing development workflows and tools like Simulink.
- High Integrity: Built using functional programming principles to minimize implementation errors.
The Future
Ongoing work includes deeper integration with Rust-based runtime verification and improved support for VHDL-level property checking.