Programming Language | Implemented in Rust | Formulated in SMT
Rusmart is a Rust to Satisfiability Modulo Theories (SMT) formulae transpiler that is implemented mostly via Rust procedural macros.
Rusmart is also a programming language that empathizes on the modeling of program semantics, in particular:
- the operational semantics of a Rusmart program is represented by Rust code which is concretely executable, while
- the denotational semantics of the program is seamlessly transpiled into SMT which can be symbolically reasoned.
Formal verification provides the utmost correctness assurance to programs while satisfiability modulo theories (SMT) solvers (e.g., Z3 and CVC5) are at the core of most push-button style formal verification tools.
Unfortunately, software verification requires scaffolding to
- Transpile code to SMT:
C - Transpile specification (i.e., correctness properties) to SMT:
S - Prove
S => C
While (automated) theorem proving is an independent line of research and has seen tremendous progress in recent years, the transpilers are still limiting factors to the adoption of formal verification.
Rusmart aims to remove the scaffolding transpilers by seamlessly blending operational and denotational semantics of a program.
Rusmart is based on the insight that: most if not all sorts of SMT formulae can be constructed in Rust. Therefore, we can develop both code and specification in a subset of Rust (i.e., the fragments that we know how to transpile), use glue macros to tie them together, and leave the proving work to SMT solvers.
In this repository, you can find examples that elaborate this insight. These examples showcase how to develop complex SMT formulae with Rust syntax in Rusmart, including:
- Generic type system (including native SMT types such as
SetandArray) - Expressions allowed (including quantified expressions to replace loops)
- Declarative constructs in imperative programs (e.g., uninterpreted function, axiomatization)
The Rusmart book aims to be a comprehensive documentation about both
- the Rusmart language features from a user perspective (e.g., type system, native expressions, etc.), and
- the internal design and implementation details of the Rusmart transpiler which lift a subset of Rust into SMT formulae.
With mdBook installed, the Rusmart book can be built and viewed locally via:
make docsHowever, as Rusmart is still under active development, changes, even major refactorings, are constantly pushed to the codebase. Therefore, expect the book to be incomplete for a foreseeable amount of time.