No they can’t be since function evaluate their arguments before they are called.
For true formal verification you likely need to work on the IR level, i.e. write a custom interpreter of sorts. IIRC, the topic arose on this forum before but I can’t find a good thread.
In the meantime you can try Supposition.jl by @Sukera which maybe gets you close enough to what you want 
See also the announcement of Supposition.jl for a brief discussion about formal verification.
Anyways @Sukera is probably one of the best folks around here to discuss formal verification