When I read that, I thought "What a huge TCB versus what's typical." Additionally, there exist verified strategies for parsing that might be applicable to Scala. Depends on if their formalisms can handle the language's grammar or whatever. Additionally, if they write untrusted parts in ML, they can supplant it with stuff like property-based testing or CakeML compiler.
If you're interested in declarative programming, you should also have a look at answer set programming. Here's an ASP version of the problem that additionally requires prime factors.
domain(100..999).
digit(0..9).
% Variation w/ prime factors
prime(P) :- domain(P), { domain(F) : F < P, P \ F == 0 } 0.
prod(P1 * P2) :- prime(P1;P2).
% Palindrome
pd(X) :- prod(X), X = 100000*A + 10000*B + 1000*C + 100*C + 10*B + A,
digit(A;B;C).
pdMax(M) :- M = #max { X : pd(X) }.
#show pdMax/1.
Superficially it resembles Prolog, but brings "true" declarativity to the table, i.e., the order of rules and the order of atoms in the body is negligible. Various notions of safety and the prohibition of nested complex terms (e.g. `f(f(x))') guarantee termination. Most importantly though, solutions to an answer set program are not proofs (as in Prolog) but truth-assignments of atoms ("answer sets"). In this specific encoding there's no significant difference though, as we're only computing a single answer set containing an atom "pdMax(X)" with the maximum palindrome X.
Solving answer set programs usually involves heuristics and much work along the lines of SAT solving. Recent solvers such as clasp [1] are surprising efficient though and rival state of the art SAT solvers.
