That's normal for programming language formal verification, from what I've seen. The question is always "how simplified is it", and if it's simplified to the point of uselessness. There's usually something to be learned (and often bugs to be fixed) from even the most-simplified version, but AFAICT "full" language verification is basically never done (except on toy[1] languages).
edit: [1]: "toy" implying "not intended for broad use", not any kind of "pointless" or "just for fun", to be clear. maybe there's a better term I should be using. so basically all "this language is designed to be formally verified and it does something interesting" languages fall into this category, because it's really not expected to be generally usable - it exists to demonstrate something, and at best become a feature of another language eventually.
Usually these inform tools that can be used to detect rule violations.
For example, the rust constant evaluator can execute almost all Rust at run-time except for FFI. This allows you to write `cargo miri test` in your project, and run your unit tests in the constant evaluator.
The constant evaluator executes the program based on rules given by models like this, and if you perform an action that violates one of the rules, they report an error.
For example, this program mutates a variable while a shared borrow (which excludes mutation) is alive via a raw pointer
fn main() {
let mut a = 13;
let b = &a;
let c = b as *const _ as *mut _;
unsafe { *c = 42; }
println!("b = {}", b);
}
The playground has a `Tools` button, that allows you to run the program under `miri` (the constant evaluator). When doing so, it prints:
error[E0080]: constant evaluation error: borrow being
accessed (Alias(None)) does not exist on the borrow stack
--> src/main.rs:5:14
|
5 | unsafe { *c = 42; }
| ^^^^^^^ borrow being accessed
(Alias(None)) does not exist on the borrow stack
error: aborting due to previous error
The error messages of the constant evaluator aren't great yet, but that basically tells you that it couldn't find a suitable mutable borrow to mutate the variable, so the access is undefined behavior.
edit: [1]: "toy" implying "not intended for broad use", not any kind of "pointless" or "just for fun", to be clear. maybe there's a better term I should be using. so basically all "this language is designed to be formally verified and it does something interesting" languages fall into this category, because it's really not expected to be generally usable - it exists to demonstrate something, and at best become a feature of another language eventually.