Write the model and the implementation. Everything between them is generated, and every guard and state change is checked against what the code actually did.
$ npx quint-refinements new my-check
created my-check
$ cd my-check && cargo run
✓ counter.incrementRun refined 1 obligations
# edit model.qnt, then
$ npx quint-refinements compile
$ cargo run
✗ bank.withdrawRun:withdraw next:
assign state diverged at state.balance
expected Int(6), observed Int(14)You own two files. The compiler owns the two between them.
Ordinary Quint. Mark the runs your code must follow with /// @conformance.
quint-refinements compile writes the scenario file and a Rust trait with one method per action.
Implement the trait for your real type. cargo run passes, or prints the exact divergence.
module bank {
type BankState = { balance: int }
var state: BankState
action init = all {
state' = { balance: 10 },
}
action withdraw(amount) = all {
amount > 0,
state.balance >= amount,
state' = { balance: state.balance - amount },
}
/// @conformance
run withdrawRun = init
.then(withdraw(4))
.then(all {
assert(state.balance == 6),
state' = state,
})
}impl Implementation for Bank {
type Evidence = Snapshot;
fn from_initial_state(initial_state: &RuntimeValue) -> Result<Self, String> { /* ... */ }
fn snapshot(&self) -> Snapshot { /* ... */ }
// Generated from `action withdraw(amount)`. The scenario supplies the 4.
fn withdraw(&mut self, arguments: &[RuntimeValue]) -> Result<(), String> {
let [RuntimeValue::Int(amount)] = arguments else {
return Err(format!("withdraw expects one integer: {arguments:?}"));
};
self.withdraw(*amount)
}
}bank.withdrawRun refined 3 obligations; final balance 6bank.withdrawRun:withdraw next: assign state diverged at state.balance expected Int(6), observed Int(14)Each page builds a complete project that CI compiles and runs, so the code you read is the code that passes.