Introduction

VeriFast is a tool for modular formal verification of the absence of undefined behavior in Rust¹ programs that use unsafe blocks and the soundness of Rust modules that use unsafe blocks. It works by symbolically executing each function separately, using a separation logic representation of memory, starting from a symbolic state that represents an arbitrary program state that satisfies the function's precondition, and checking that each state at which the function returns satisfies the function's postcondition. By using the callee's precondition and postcondition instead of its body when symbolically executing a function call, and by using the user-specified loop invariant when symbolically executing a loop so as to be able to symbolically execute the loop body only once, and by using symbols to represent possibly infinitely many program states using a finite number of symbolic states, VeriFast covers all (usually infinitely many) possible executions of a function using a finite (and usually small) number of symbolic executions, allowing the verification of (small) programs to usually complete in a matter of seconds.

For functions not declared as unsafe, VeriFast derives a precondition and postcondition from the function's parameter types and return type using the separation logic interpretation of Rust's types defined by RustBelt; for functions declared as unsafe, the user has to provide a precondition and postcondition by inserting specially marked comments called annotations into the source code. Similarly, for each loop a loop invariant has to be provided in an annotation. To be able to express these conditions (called assertions), the user may generally also have to insert annotations defining mathematical recursive datatypes called inductive datatypes, mathematical recursive functions over these datatypes called fixpoint functions, recursive named separation logic assertions called predicates, and type predicates defining a custom interpretation for some of the struct types defined by the current module (as well as some less common constructs such as VeriFast named function types, lemma function types, predicate families, and predicate family instances).

In order for symbolic execution to succeed, the user may furthermore have to insert annotations containing ghost commands such as open and close commands for unfolding and folding predicates and calls of lemma functions, possibly recursive functions defined inside annotations that are checked by VeriFast to terminate and to not have side-effects and that serve as possibly inductive proofs about fixpoint functions and predicates.

This reference defines the syntax of the various kinds of annotations, and describes VeriFast's symbolic execution algorithm and the various checks that VeriFast performs.

Soundness of VeriFast

We aim for VeriFast to be sound, i.e. that if VeriFast reports "0 errors found", then indeed each function not marked as unsafe in the crate under verification is semantically well-typed, which for parameterless non-unsafe functions like main implies that no execution of the function has undefined behavior. However, in contrast to some other tools such as RefinedRust, VeriFast itself has not been formally verified, so unknown bugs are almost certainly present in the tool that may cause the tool to report "0 errors found" incorrectly in some cases. There may also be known unsoundnesses; these should all be recorded as issues with label unsoundness. Also, when using command-line flags like -disable_overflow_check, -ignore_ref_creation, -allow_assume, and -ignore_unwind_paths, the soundness property can only be expected to hold under the assumption that the program does not perform arithmetic overflow, complies with the pointer aliasing rules, does not violate any of the assume ghost commands present in the program, and does not violate semantic well-typedness due to unwinding, respectively. Finally, note that since VeriFast for Rust uses the rustc frontend, which assumes a particular compilation target architecture, VeriFast for Rust's result will only hold for the current target architecture.

The state of VeriFast

VeriFast has been developed by Bart Jacobs, Jan Smans, and Frank Piessens at KU Leuven, Department of Computer Science, DistriNet research group since 2008, with many contributions from contributors inside and outside DistriNet. VeriFast for Rust has been developed by Nima Rahimi Foroushaani and Bart Jacobs at DistriNet since 2022. The lead developer and main maintainer is Bart Jacobs, an associate professor at DistriNet, who combines these activities with his usual research, education, and service duties. The largest verification performed so far with VeriFast for Rust, the verification of certain properties of certain functions of the Rust standard library's LinkedList data structure, was performed in December 2024. Its support for the Rust language is as of yet very incomplete², so that for any new nontrivial use case, it is to be expected, for now, that the tool will have to be extended. Bart Jacobs is eager to support anyone interested in using VeriFast. However, despite his best intentions, he may get distracted by other occupations; in that case, please do not hesitate to remind him early and often---your continued showing of interest will only delight him and you may rest assured that, given sufficient prodding, your issue will be resolved eventually.

The state of this reference

This reference is under construction; much material is still missing. Please bear with us! But if there are particular parts you're particularly eager to see, it always helps to let us know.

Further resources

A tutorial is being prepared. In the meantime, the VeriFast Tutorial for C is a good resource for familiarizing yourself with VeriFast's concepts. Rust versions of the examples and exercises of the VeriFast Tutorial are available; see the command lines used to verify them in verify.mysh (where they are listed in the order in which they appear in the Tutorial). (Note: the solutions found there can be transformed into starting points for exercises by stripping the VeriFast annotations using bin/vfstrip: e.g. vfstrip < account.rs > account_stripped.rs.)

Further examples of VeriFast for Rust proofs are in tests/rust; the command lines are in tests/rust/testsuite.mysh.

Symbolic execution states

A symbolic execution state consists of the following components:

• A symbolic store, mapping each local variable name in scope whose address is not taken to a term representing its current value, and each local variable in scope whose address is taken to a term representing a pointer to the variable.
• A symbolic heap, a multiset of heap chunks representing the resources owned by the code being verified. Note: "symbolic heap" and "heap chunk" are slightly misleading names, because ownership of non-heap resources, such as global variables or stack-allocated variables whose address is taken¹, is also represented as "heap chunks"; more accurate names would have been "symbolic multiset of owned resources" and "chunk of resource".
• A path condition, a set of formulae (terms of type bool) encoding the assumptions made about the symbols used on the current symbolic execution path.

These components are shown in the Locals pane, the Heap chunks pane, and the Assumptions pane of the VeriFast IDE, respectively.

A heap chunk consists of the following components:

• The chunk's coefficient: a term representing a real number. In case of an application of a built-in predicate representing a region of memory, the coefficient is always greater than zero and not greater than one. If the coefficient equals one, it's a full chunk denoting read/write access; otherwise, it's a fractional chunk denoting read-only access. In case of a user-defined predicate, the meaning is given by distributing the multiplication by the coefficient over the separating conjunctions in the predicate's body. If a chunk's coefficient is the literal term 1, it is not shown in the VeriFast IDE.
• The chunk's predicate: a term representing a predicate value. When processing a predicate definition, VeriFast allocates a fresh predicate symbol to represent the predicate; also, each predicate constructor is associated with a function symbol mapping a predicate constructor argument list to a predicate value.
• The chunk's type arguments, a list of types with which to instantiate the predicate's type parameters.
• The chunk's arguments, a list of terms with which to instantiate the predicate's parameters.
• Optionally, the chunk's size. This is only potentially present when verifying a lemma function whose precondition's first separating conjunct is a predicate assertion. In that context, chunks derived from the first chunk produced by the lemma function's precondition through N open operations have size -N. This component is used to verify termination of lemma functions defined by induction on the derivation of the precondition's first chunk.

A predicate is either built-in or user-defined. All built-in predicates are declared in the prelude, in bin/rust/prelude.rsspec, or are automatically generated by VeriFast when it processes certain declarations. The most important ones are the following:

• pred points_to_<T>(p: *T, v: option<T>): a chunk points_to_::<T>(p, v) denotes ownership of a variable of type T pointed to by properly aligned pointer p. If v is some(V), the variable is initialized and holds value V; otherwise, it is uninitialized. Since the points-to chunk for a variable is consumed when the variable is deallocated, ownership of a points-to chunk implies that the pointer is non-dangling.
• pred points_to<T>(p: *T, v: T): equivalent to points_to_::<T>(p, some(v)).
• pred array_<T>(p: *T, n: i32, vs: list<option<T>>): a chunk array_::<T>(p, n, vs) denotes ownership of an array of n components of type T, pointed to by properly aligned pointer p. List vs of length n holds each component's value, if it is initialized, or none if it is not.
• pred array<T>(p: *T, n: i32, vs: list<T>): denotes ownership of a fully initialized array.
• When processing a definition of a struct S with fields F1: T1 through Fn: Tn, VeriFast introduces field predicates pred S_F1_(p: *S, v: option<T1>) = points_to_::<T1>(&(*p).F1, v) and pred S_F1(p: *S, v: T1) = points_to::<T>(&(*p).F1, v) through S_Fn_ and S_Fn, as well as a padding predicate pred struct_S_padding(p: *S).

Annotations

This chapter defines the syntax and the semantics of the various contructs that may appear inside VeriFast annotations.

• Keywords
• Types
• Expressions
• Assertions
• Function specifications
• Function body annotations
  • Ghost commands
  • Block annotations
  • Call annotations
• Ghost declarations

Keywords

In annotations, these words, in addition to Rust's keywords, are recognized as keywords and cannot be used as identifiers:

_ above abstract_type activating action and_fresh_handle
and_handle any assert assume_correct below box_class by close
consuming_box_pred consuming_handle_pred copred create_box
create_fresh_handle create_handle decreases dispose_box
dup_lem_ptr_chunk emp ens extends fix fix_auto fn_type
forall_ handle handle_pred import_module inductive inv leak
lem lem_auto lem_type let_lft merge_fractions
nonghost_callers_only on_unwind_ens open perform_action permbased pred
pred_ctor pred_fam pred_fam_inst preserved_by produce_fn_ptr_chunk
produce_lem_ptr_chunk producing_box_pred producing_fresh_handle_pred
producing_handle_pred req require_module split_fraction terminates
truncating type_pred_decl type_pred_def typedef typeid
unloadable_module

These are the additional operators recognized inside annotations:

&*& |-> |-?-> @

Types

Inside annotations, the syntax of types is extended as follows:

^Syntax
Type :
      ... | *_ | any | PureFunctionType | PredicateType | real

PureFunctionType :
      fix ( ( ParamType , )^* ParamType^? )

ParamType :
      (IDENTIFIER :)^? Type

PredicateType :
      pred ( ((( ParamType , ) ParamType )^? ; )^? ( ParamType , ) ParamType^? )

In addition to (some subset of) Rust's types, VeriFast supports the following types:

• Type *_ (pointer-to-anything) is a pointer type implicitly convertible to any other pointer type. It is analogous to C's void *.
• Type any is the union of all inductive types that themselves contain any only in positive positions.
• The pure function type fix(T1, ..., Tn, U) is the type of mathematical functions taking N arguments, of types T1 through Tn, and returning a value of type U.
• The predicate type pred(T1, ..., Tn) is the type of separation logic predicates taking N arguments, of types T1 through Tn. The type pred(T1, ..., Tn; U1, ..., Um) is the type of precise separation logic predicates taking N input arguments and M output arguments.
• Type real is the type of real numbers. (It is mostly used for chunk coefficients and for reasoning about floating-point numbers.)

In pure function types and predicate types, parameter names may optionally be written for documentation purposes; they are ignored by VeriFast.

Note, furthermore:

• VeriFast does not distinguish between *const T and *mut T and supports the syntax *T. That is, VeriFast treats the type expressions *const T, *mut T, and *T identically.
• When used as the type of a ghost variable (e.g. a pure function parameter or return value, a predicate parameter, a lemma parameter, or a ghost cell) or as the type of an expression in an annotation, all integer types are interpreted as the mathematical type ℤ of all integers. Also, inside annotations arithmetic operations on integers are always interpreted as operations on ℤ and never wrap around.

Expressions

^Syntax
Expression : ... | Lifetime | typeid ( Type )

The syntax of expressions in annotations is the same as in Rust code, with two additional supported forms:

• A lifetime parameter in scope may be used as an expression. This denotes the RustBelt lifetime_t value corresponding to that lifetime parameter.
• The expression typeid(T) denotes the typeid of type T.

Also, certain Rust expressions are interpreted differently in annotations than in Rust code:

• Array expressions are interpreted as list<T> values. For example, [10, 20, 30] is interpreted as cons(10, cons(20, cons(30, nil))).
• Arithmetic expressions on integer types are interpreted as operations on the mathematical set ℤ of all integers; they produce their mathematical result and never wrap around.

Note that match expressions may be used to perform case analysis on values of VeriFast inductive types.

Assertions

^Syntax
Assertion :
      PointsToAssertion
   | PredicateAssertion
   | TypePredicateAssertion
   | BooleanAssertion
   | PatternMatchingEqualityAssertion
   | ConditionalAssertion
   | MatchAssertion
   | Assertion &*& Assertion

PointsToAssertion : ( [ VFPattern ] )^? Expression ( |-> | |-?-> ) VFPattern

VFPattern : _ | ? ( IDENTIFIER | _ ) | Expression

PredicateAssertion : ( [ VFPattern ] )^? Expression VFPatternList ^? VFPatternList

VFPatternList : ( (( VFPattern , )^* VFPattern )^? )

TypePredicateAssertion : < Type > . IDENTIFIER VFPatternList

BooleanAssertion : Expression

PatternMatchingEqualityAssertion : Expression == VFPattern

ConditionalAssertion : if Expression { Assertion } else { Assertion }

MatchAssertion : match Scrutinee { ( MatchAssertionArm ,^? )^* }

MatchAssertionArm : Pattern => Assertion

Function specifications

VeriFast accepts the following specification clauses between a function's header and its body:

^Syntax
SpecificationClause :
      /*@ req Assertion ; @*/
   | /*@ ens Assertion ; @*/
   | /*@ on_unwind_ens Assertion ; @*/
   | /*@ assume_correct @*/

Note that VeriFast also support single-line annotations of the form //@ ...annotation.... Such an annotation is entirely equivalent to /*@ ...annotation... @*/.

Notice that the requires clause, the ensures clause, and the unwind ensures clause must be in separate annotations.

Function body annotations

Ghost commands

VeriFast accepts the following ghost commands as annotations in positions where statements are allowed in Rust code.

^Syntax
GhostCommandAnnotation : /*@ GhostCommand @*/

GhostCommand :
      open PredicateAssertion ;
   | close PredicateAssertion ;
   | let IDENTIFIER = Expression ;
   | if Expression { GhostCommand ^* } ( else { GhostCommand ^* } )^?
   | match Scrutinee { MatchGhostCommandArm ^* }
   | assert Assertion ;
   | leak Assertion ;
   | produce_lem_ptr_chunk TypePath ( (( Expression , )^* Expression )^? ) ( (( IDENTIFIER , ) IDENTIFIER )^? ) { GhostCommand ^* } ( ; | { GhostCommand ^* } )
   | produce_fun_ptr_chunk TypePath ( Expression ) ( (( Expression , )^* Expression )^? ) ( (( IDENTIFIER , ) IDENTIFIER )^? ) { GhostCommand ^* }
   | { GhostDeclaration ^* GhostCommand ^* }
   | return Expression ^? ;
   | Expression ;

A return ghost command may only appear in a lemma body, not in a ghost command annotation.

Block annotations

Additionally, a Rust block may start with one of the following VeriFast annotations:

• a loop invariant of the form /*@ inv Assertion ; @*/
• a loop specification of the form /*@ req Assertion ; ens Assertion ; @*/. Notice that here, the requires clause and the ensures clause must be in the same annotation, whereas in the case of function specifications they must be in separate annotations.
• a batch of ghost declarations of the form /*@ GhostDeclaration ^* @*/ The declarations supported in such batches are predicate definitions, lemma definitions, and local lifetime variable definitions (using let_lft).

Call annotations

Furthermore, a ghost generic argument list annotation may be inserted between the function name and the argument list of a Rust function call, like so: foo/*@::<'a, T>@*/. This is necessary in cases where it is important to pass a particular lifetime as a generic argument to a function. If, for a function call, no ghost generic argument list is provided, VeriFast uses 'static as the argument for each of the function's lifetime parameters.

Ghost declarations

A ghost declarations annotation may appear anywhere a Rust item may appear, except that only a few kinds of ghost declarations are supported inside function bodies (see Block annotations).

^Syntax
GhostDeclarationsAnnotation : /*@ GhostDeclaration ^* @*/

GhostDeclaration :
      pub GhostDeclaration
   | inductive IDENTIFIER GenericParams ^? = |^? InductiveConstructor ( | InductiveConstructor )^* ;
   | fix IDENTIFIER GenericParams ^? ( Params ) ( -> Type )^? ( { Expression } | ; )
   | pred IDENTIFIER GenericParams ^? ( ( Params ; )^? Params ) ( = Assertion )^? ;
   | pred_ctor IDENTIFIER GenericParams ^? ( Params ) ( ( Params ; )^? Params ) = Assertion ;
   | pred GenericParams ^? < Type > . IDENTIFIER ( ( ParamNames ; )^? ParamNames ) = Assertion ;
   | lem IDENTIFIER GenericParams ^? ( Params ) ( -> Type )^? LemmaRest
   | fn_type IDENTIFIER GenericParams ^? ( Params ) = unsafe fn ( Params ) ( -> Type )^? ; req Assertion ; ens Assertion ; on_unwind_ens Assertion ;
   | lem_type IDENTIFIER GenericParams ^? ( Params ) = lem ( Params ) ( -> Type )^? ; req Assertion ; ens Assertion ;
   | let_lft Lifetime = Expression ;
   | abstract_type IDENTIFIER ;

InductiveConstructor : IDENTIFIER ( ( ( ParamType , )^* ParamType ) )^?

LemmaRest :
      LemmaSpecification { GhostCommand ^* }
   | ; LemmaSpecification

LemmaSpecification : nonghost_callers_only^? req Assertion ; ens Assertion ;

Params : (( Param , )^* Param )^?

Param : IDENTIFIER : Type

ParamNames : (( IDENTIFIER , )^* IDENTIFIER )^?

Verifying compliance with Rust's pointer aliasing rules

Breaking Rust's pointer aliasing rules or mutating immutable bytes is undefined behavior. VeriFast currently verifies (only) the latter.

In particular, it verifies that the memory pointed to by a shared reference, except for the memory inside an UnsafeCell, is not mutated while the shared reference is active. First of all, shared reference creation is treated like the creation of a new pointer value, with the same address but a different provenance from the original pointer. Points-to resources for the original pointer cannot be used for accesses through the new shared reference.

VeriFast requires, at creation of a shared reference, that the user transfer a fraction greater than 0 and less than 1 of the points-to resources for the original place to the new shared reference. These resources are transferred back to the original reference when the shared reference is ended (and only then); from that point on, the shared reference is no longer usable.

Specifically, a shared reference creation expression &E is treated like a call of function create_ref in aliasing.rsspec, which is part of the VeriFast for Rust prelude. This function requires that a shared reference value has been precreated using lemma precreate_ref declared in the same file. Furthermore, it requires that the new reference has been initialized.

Memory inside an UnsafeCell is exempted from this process; the points-to resources for that memory are never transferred. This means that a shared reference to an UnsafeCell does not directly provide access to the memory behind the UnsafeCell. To access the memory, the developer has to call UnsafeCell::get. VeriFast treats calls of this method like calls of logical function ref_origin (also declared in aliasing.rsspec). Therefore, if a struct S has a field f of type UnsafeCell<T> inside, it is important for <S>.share(k, t, l) to (directly or indirectly, e.g. via a nonatomic borrow), assert points-to resources for ref_origin(&(*l).f). See, for example, cell.rs and mutex.rs.

Verifying non-unsafe functions

RustBelt

A core value proposition of Rust is that well-typed programs have no undefined behavior, under certain conditions on the use of unsafe blocks. The RustBelt project has developed a mathematically precise proposal for what those conditions are. In this proposal, a semantics is defined for Rust's types and typing judgments in separation logic, providing a definition of whether a function is semantically well-typed that talks only about the function's behavior, not about its precise syntactic structure, and is therefore applicable to functions containing unsafe blocks. They have proven the soundness of Rust's type checker with respect to this semantics, implying that if a function that does not contain unsafe blocks is syntactically well-typed, then it is semantically well-typed. Therefore, if a program consists of modules that use unsafe blocks and client code that does not, it suffices to establish that these modules are semantically well-typed to be able to conclude that the program as a whole is semantically well-typed and therefore has no undefined behavior.¹

In order to be able to express the semantics of mutable references and shared references, as well as the semantics of many of the uses of interior mutability in the Rust standard library, the RustBelt authors have proposed the lifetime logic, which defines separation logic concepts such as lifetime tokens, full borrows, fractured borrows, thread tokens, and nonatomic borrows.

An excellent resource for learning more about the RustBelt proposal and the advanced separation logic Iris that underlies it is Ralf Jung's thesis.

RustBelt and the lifetime logic in VeriFast

An axiomatisation of the lifetime logic into VeriFast's logic and some further RustBelt-related definitions and axioms can be found in the following files:

• bin/rust/rust_belt/lifetime_logic.rsspec
• bin/rust/rust_belt/general.rsspec

Semantic well-typedness of functions in VeriFast

If a crate under verification defines a function not marked as unsafe, VeriFast generates a specification for that function that expresses the function's semantic well-typedness. If the function is annotated with an explicit specification as well, VeriFast first verifies that the explicit specification implies² the generated one, and then verifies the function body against the explicit specification; otherwise, VeriFast verifies the function body against the generated specification.

For a function fn f<'a, 'b : 'a, T, U>(x1: T1, ..., xN: TN) -> U, the generated specification is as follows:

req thread_token(?_t) &*&
    [?_q_a]lifetime_token('a) &*&
    [?_q_b]lifetime_token('b) &*& 
    lifetime_inclusion('a, 'b) == true &*&
    <T1>.own(_t, x1) &*&
    ...
    <TN>.own(_t, xN);
ens thread_token(_t) &*&
    [_q_a]lifetime_token('a) &*&
    [_q_b]lifetime_token('b) &*&
    <U>.own(_t, result);
on_unwind_ens
    thread_token(_t) &*&
    [_q_a]lifetime_token('a) &*&
    [_q_b]lifetime_token('b);

Drop functions

If the crate under verification implements Drop for a struct S<'a> with fields f1 : T1 through fN : TN, VeriFast generates the following specification for drop(&mut self):

req thread_token(?_t) &*&
    [?_q_a]lifetime_token('a) &*&
    <S>.full_borrow_content(_t, self);
ens thread_token(_t) &*&
    [_q_a]lifetime_token('a) &*&
    <T1>.full_borrow_content(_t, &(*self).f1) &*&
    ...
    <TN>.full_borrow_content(_t, &(*self).fN);
on_unwind_ens
    thread_token(_t) &*&
    [_q_a]lifetime_token('a) &*&
    <T1>.full_borrow_content(_t, &(*self).f1) &*&
    ...
    <TN>.full_borrow_content(_t, &(*self).fN);

Semantics of types in VeriFast

For simple types T such as bool and the integer types, we simply have <T>.own(t, x) = true. Here are some more interesting cases:

• <&'a mut T>.own(t, l) = full_borrow('a, <T>.full_borrow_content(t, l))
• <&'a T>.own(t, l) = <T>.share('a, t, l)

For any type T, we have <T>.full_borrow_content(t, l) = *l |-> ?x &*& <T>.own(t, x).

For simple types T such as bool and the integer types, we simply have <T>.share(k, t, l) = frac_borrow(k, <T>.full_borrow_content(t, l)).

If the crate under verification defines a struct S, it can define a custom semantics for type S by defining the <S>.own and <S>.share predicates.³ If it does so, it must also prove a number of proof obligations about these predicates.

Proof obligations for own

If a crate defines a struct S as well as a custom definition of <S>.own, and the struct's field types are not trivially droppable and the struct does not implement the Drop trait, then the crate must prove the following lemma:

lem S_drop()
    req S_own(?t, ?s);
    ens <T1>.own(t, s.f1) &*& ... &*& <Tn>.own(t, s.fn);

where the fields of S are f1 through fn and their types are T1 through Tn.

If a crate defines a struct S as well as a custom definition of <S>.own, and S is Send, and the own predicate mentions the thread id, then the crate must prove the following lemma:

lem S_send(t1: thread_id_t)
    req S_own(?t, ?s);
    ens S_own(t1, s);

Proof obligations for share

If a crate defines a struct S as well as a custom definition of <S>.share, then the crate must prove the following two lemmas:

lem S_share_full(k: lifetime_t, t: thread_id_t, l: *S)
    req atomic_mask(MaskTop) &*& [?q]lifetime_token(k) &*& full_borrow(k, S_full_borrow_content(t, l)) &*& ref_origin(l) == l;
    ens atomic_mask(MaskTop) &*& [q]lifetime_token(k) &*& [_]S_share(k, t, l);

lem S_share_mono(k: lifetime_t, k1: lifetime_t, t: thread_id_t, l: *S)
    req lifetime_inclusion(k1, k) == true &*& [_]S_share(k, t, l);
    ens [_]S_share(k1, t, l);

Additionally, if S is Sync and the share predicate mentions the thread id, then the crate must prove the following lemma:

lem S_sync(t1: thread_id_t)
    req [_]S_share(?k, ?t, ?l);
    ens [_]S_share(k, t1, l);

Generic structs

If struct S is generic in type parameters T1 through Tm, each of the above lemmas must also be generic in the same parameters. Furthermore, they may additionally require and ensure type_interp::<Ti>(), for each i. Furthermore, if a type parameter is Send or Sync, an is_Send(typeid(Ti)) == true or is_Sync(typeid(Ti)) == true conjunct may be added to the precondition. For example:

lem Pair_send<A, B>(t1: thread_id_t)
    req type_interp::<A>() &*& type_interp::<B>() &*& Pair_own::<A, B>(?t, ?pair) &*& is_Send(typeid(A)) && is_Send(typeid(B));
    ens type_interp::<A>() &*& type_interp::<B>() &*& Pair_own::<A, B>(t1, pair);
{
    open Pair_own::<A, B>(t, pair);
    Send::send::<A>(t, t1, pair.fst);
    Send::send::<B>(t, t1, pair.snd);
    close Pair_own::<A, B>(t1, pair);
}