We present VeriROS, a compact pipeline that issues machine-checkable \emph{admission certificates} for ROS2 waypoint missions and ties those certificates to lightweight runtime evidence. At design time a \emph{Formal Gate} encodes conservative per-leg Worst-Case Execution Time (WCET) estimates and Processor Demand Criterion (PDC) feasibility windows into quantifier-free linear real arithmetic (QF_LRA) constraints; an SMT solver (Z3) then decides feasibility and yields either a certificate with minimum slack margins or an UNSAT core with repair hints. At runtime missions execute under Earliest Deadline First (EDF) with safety fences while a ROS2 monitor evaluates STL robustness and empirical counters to validate, degrade, or revoke certificates. We describe an anonymized prototype and artifact bundle and outline an evaluation plan; we close with open questions on certificate semantics, compositional PTA contracts, and scalability.