1) The code that users write in Reflex is the code that actually runs. This means that any guarantee about a Reflex program is a guarantee about the real life i

1) The code that users write in Reflex is the code that actually runs. This means that any guarantee about a Reflex program is a guarantee about the real life implementation of that program. 2) Reflex does not use testing to verify a user's code. Instead, Reflex automatically produces fully machine checkable proofs that user-provided code satisfies user-provided specifications. Machine checkable proofs (in a proof assistant) provide the strongest possible guarantee about one's code.