
Future Work in Rust Co-Assurance
22 Jan 2025
Explore the latest advancements in Rust-based toolchains for hardware/software co-assurance.

Proving Theorems for Rust’s Dancing Links in ACL2
22 Jan 2025
Explore how 160 theorems, including correctness proofs for CDLLs, validate Rust's Dancing Links implementation using ACL2’s automated verification tools.

Machine-Generated Code That Works
22 Jan 2025
Discover how RAR Rust source is translated into ACL2 with Plexi, ensuring readable, high-assurance machine-generated code for robust formal reasoning.

Simplifying Circular Data Structures with Rust’s RAR Subset
22 Jan 2025
Learn how Knuth’s Dancing Links optimization works in Rust’s RAR subset with array-based circular doubly-linked lists for efficient high-assurance systems.

The Algorithm That Makes Data Dance—and Solve Complex Problems Fast
21 Jan 2025
Discover how Rust and ACL2 optimize Dancing Links for exact cover problems like Sudoku, leveraging memory safety and efficient list manipulation.

The Case for Rust Programming as a Game-Changer for High-Level Synthesis
21 Jan 2025
Discover how Rust and RAR enable memory-safe, high-assurance hardware/software co-design, with applications from cryptography to autonomous systems.

Scaling Hardware/Software Co-Assurance with Restricted Algorithmic C
21 Jan 2025
Explore how Restricted Algorithmic C and ACL2 enable scalable hardware/software co-assurance with formal verification for critical system designs.

RRR—Rust, RAR, and RAC: The Trifecta for Co-Design Excellence
21 Jan 2025
Restricted Algorithmic Rust (RAR), a subset of Rust enables high-assurance designs by integrating with RAC, leveraging Rust’s safety features for co-design.