In this talk, we focus on two different aspects of verification of boolean predicates over distributed networks. Given a network configuration, the proof-labeling scheme (PLS) model defines a distributed proof in the form of a label that is given to each node, and all nodes locally verify that the network configuration satisfies the desired boolean predicate by exchanging labels with their neighbors. The complexity measure of the scheme, a.k.a. the proof size, is defined to be the maximum size of a label. 1. Space-time tradeoffs for distributed verification, joint work with Rafail Ostrovsky and Will Rosenbaum. In this work, we introduce the notion of a t-PLS, which allows the verification procedure to run for super-constant time. Our work analyzes the tradeoffs of t-PLS between time, label size, message length, and computation space. We construct a universal t-PLS and prove that it uses the same amount of total communication as a known one-round universal PLS, and t factor smaller labels. In addition, we provide a general technique to prove lower bounds for space-time tradeoffs of t-PLS. We use this technique to show an optimal tradeoff for testing that a network is acyclic (cycle free). Our optimal t-PLS for acyclicity uses proof size, message size and computation space O( ( log n)/t). 2. Approximate proof-labeling schemes, joint work with Keren Censor-Hillel and Ami Paz. In this work we extend the PLS model by defining the approximate PLS (APLS) model. In this new model, the predicates for verification are of the form f(G)\le f'(G), where f, f': F → N for a family of configurations F and the set of natural numbers N. Informally, the predicates considered in this model are a comparison between two values of the configuration. As in the PLS model, nodes exchange labels in order to locally verify the predicate, and all must accept if the network satisfies the predicate. The soundness condition is relaxed with an approximation ration alpha, so that only if f(G) > alpha*f'(G) some node must reject. We show that in the APLS model, the proof size can be much smaller than the proof size of the same predicate in the PLS model. Moreover, we prove that there is a tradeoff between the approximation ratio and the proof size.