Python3, 340 bytes

import re
def P(e,c):
 K=[]
 if'var'==e[0]:K+=[e[1]in c]
 if'abs'==e[0]:K+=['['!=str(e[1])[0]and e[1]not in c and P(e[2],c+[e[1]])]
 if'app'==e[0]:K+=[P(e[1],c)and P(e[2],c)]
 return any(K)
def f(s):
 try:return s[0]=='('and P(eval(re.sub('\s|\w+|\(|\)',lambda x:{' ':',','(':'[',')':']'}.get(V:=x.group(),f'"{V}"'),s)),[])
 except:return 0

Try it online!

Curry (PAKCS), 116 bytes

p"(var "a x|elem a x=0
p"(app "(a++' ':b)x=a#x+b#x
p"(abs "(a++' ':b)x|all(>'@')a=b#(a:x)
(#)(k++n++")")=p k n
(#[])

Try it online!

g returns 0 if there is a match and fails to find a match if there is none.

Explanation

This looks and sort of works like a Haskell answer might. However Curry's pattern matches are way more powerful than Haskell's because it has a trick up it's sleeve. As well as a functional programming language Curry is a logical language. It has non-determinism.

In Haskell a pattern either matches or it doesn't. In Curry a pattern can match a string multiple ways and it will follow through each to find the one you meant. So

p("(app "++a++' ':b++")")

Will cold potentially match many things. For example

p"(app (var x) (var y))"

can break that apart at any space in the string. Curry will match all of them and attempt to run them. All the bad ones will fail later down the line.

Tiny Lisp, 318

(d C(q((E L)(i(e L())0(i(e E(h L))1(C E(t L)))))))(d H(q((le li)(i(e()li)(e le 0)(H(s le 1)(t li))))))(d I(q((L X)(i(e(q abs)(h L))(i(H 3 L)(i(C(h(t L))X)0(I(h(t(t L)))(c(h(t L))X)))0)(i(e(q var)(h L))(i(H 2 L)(i(C(h(t L))X)1 0)0)(i(e(q app)(h L))(i(H 3 L)(i(I(h(t L))X)(I(h(t(t L)))X)0)0)0))))))(d V(q(()(L)(I L()))))

This defines a macro V (for verify) which can be applied to a list, and will check whether it is of the proper form as defined in the question.

This can't do any checks on a lexical level, as Tiny Lisp has no string input (and not even a string type). Therefore it is running out of competition

Here are some test cases:

------examples-from-question-----
((V (abs x (abs y (var x))))  ––→  1)
((V (app (abs x (var x)) (var x)))  ––→  0)
((V (abs x (abs x (var x))))  ––→  0)
----examples-from-TIO----
((V (var x))  ––→  0)
((V (abs vv (var vv)))  ––→  1)
((V (abs xy (var fg)))  ––→  0)
((V (abs x (abs y (var x))))  ––→  1)
((V (app (abs x (var x)) (var x)))  ––→  0)
((V (abs x (app (var x) (var x))))  ––→  1)
((V (app (abs x (app (var x) (var x))) (abs y (app (var y) (var y)))))  ––→  1)
((V (abs x (abs x (var x))))  ––→  0)
((V (abs x (abs y (abs y (var x)))))  ––→  0)
((V (abs (var)))  ––→  0)
---reject---------
((V uuuuuuuuu)  ––→  0)
((V (mmm hummus))  ––→  0)
((V (abs x (var y)))  ––→  0)
((V (abs x (abs x (var x))))  ––→  0)
((V (app (abs x (var x)) (var x)))  ––→  0)
((V (abs (var k) (var (vark k))))  ––→  0)
((V (abs x (abs y (abs y (var x)))))  ––→  0)
((V (abs x (var x)))  ––→  1)
--------accept--------
((V (abs x (var x)))  ––→  1)
((V (abs x (abs y (var x))))  ––→  1)
((V (abs xx (app (var xx) (var xx))))  ––→  1)
((V (app (abs ab (app (var ab) (var ab))) (abs ab (app (var ab) (var ab)))))  ––→  1)

The last "reject" case (with the missing space) is accepted, as we are parsing this as a tiny lisp list, not as a lambda. The test cases with unbalanced parentheses can't even be run.

Here is the code formatted, and with some comments (I've extended the reference implementation of Tiny Lisp to include Python-style line comments). (The comments all start with #! because that can be handled by my automated whitespace-and-comment-remover made for Ceylon.)

#! tinylisp.py

#! Parse a lambda for correctness. 
#! Question: https://codegolf.stackexchange.com/q/233453/2338
#! My answer: https://codegolf.stackexchange.com/a/233925/2338

#! checks whether some element is contained in a list.
(d C #! for "contains"
   (q ((E L) #! E = the element to be checked
             #! L = the list in which the element is searched
       (i (e L ())
          0
          (i (e E (h L))
             1
             (C E (t L))
          )
       )
      )
   )
)

#! checks whether a list has a specified length.
#! len = expected length
#! list = list to check
(d H #! for has-length
   (q ((le li) #! le = the asserted length
               #! li = the list to check
       (i (e () li)
          (e le 0)
          (H (s le 1) (t li))
       )
      )
   )
)

#! This is the main working force here.
#! I (for "is-valid") checks (recursively) whether a lambda expression is valid
#! in a given context of defined variable names.
(d I
   (q ((L X)
       #! L = candidate for a lambda function,
       #! X (context) = list of defined variable names
       (i (e (q abs) (h L))
          (i (H 3 L)
             (i (C (h (t L)) X)
                0
                (I (h (t (t L))) (c (h (t L)) X)))
             0)
          (i (e (q var) (h L))
             (i (H 2 L) 
                (i (C (h (t L)) X)
                   1
                   0)
                0
             )
             (i (e (q app) (h L))
                (i (H 3 L)
                   (i (I (h (t L)) X)
                      (I (h (t (t L))) X)
                      0)
                   0)
                0
             )
          )
       )
      )
   )
)

#! V (for "verify") is the entry point to call from the outside.
#! `(V (...))` returns 1 when it's a valid lambda expression, 0 when it is not.
(d V
   (q (()
       (L)
       (I L ())
      )
   )
)

Scala, 293 bytes

The function that does all the work:

def f(s:Any,c:Set[Any]=Set()):Option[Any]=s match{case
s"(var $v)$r"=>Option.when(c(v))(r)case
s"(abs $v $r"=>if(!c(v)&v.matches("[a-z]+"))f(r,c+v).collect{case s")$r"=>r}else None case
s"(app $o"=>f(o,c).collect{case s" $r"=>f(r,c)}.flatten.collect{case s")$r"=>r}case
_=>None}

This one simply turns an Option into a Boolean.

f(_)==Some("")

Try it in Scastie!

Ungolfed:

//sexpr is the string to parse, ctx is the context (a Set[String] in reality)
//If valid, it will return a Some containing the rest of the string, otherwise a None
def f(sexpr: Any, ctx: Set[Any] = Set()): Option[Any] = sexpr match {
  case s"(var $varName)$rest" =>
    //Check if varName is defined, and only then return the rest
    Option.when(ctx.contains(varName))(rest)
  case s"(abs $varName $rest" =>
    //Make sure varName isn't already defined and that it's a valid name
    if (!ctx.contains(varName) && varName.matches("[a-z]+"))
      //If so, parse the rest, adding varName to the context
      f(rest, ctx + varName)
        .collect { case s")$rest" => rest } //Ensure there's a matching `)`
    else None //If the name is invalid, so is the expression
  case s"(app $first" =>
    //Try parsing the first argument
    f(first, c)
      //Ensure there's a space after it and parse the rest
      .collect { case s" $rest" => f(rest, ctx) }
      .flatten //Turn the Option[Option[String]] into an Option[String]
      .collect { case s")$rest" => rest } //Ensure there's a matching `)`
  case _ => None //If it's not a var, abs, or app, it's invalid
}

Perl 5 -p, 86 bytes

Who said this can’t be solved with a regex? ☺

$_=reverse=~/^(\)(((\w+) (?=([^)]|(?1))* \4 ))rav|(?1) ((?!(?3))\w+ sb|(?1) pp)a)\()$/

Try it online!

Outputs 1 for acceptance or the empty string for rejection. To get around restrictions on lookbehind, I reverse the input and use lookahead instead.

Raku (Perl 6) -p, 123 bytes

my %v;my$r=rx["(abs "(\w+)<!{%v{$0}++}>\s<~~>{--%v{$0}}")"|"(app "<~~>\s<~~>")"|"(var "(\w+)<?{%v{$0}}>")"];$_=so m/^^$r$$/

Try it online!

First time golfing in Raku (this seemed like an apt challenge to give it a spin), so there's probably room for improvement. It's a simple parse of the text, using the %v hash to keep track of existing variables.