Proof techniques for string algorithms?
There is some work on developing an algebraic or grammar-based view of string algorithms, for example

Robert Giegerich, Carsten Meyer, Peter Steffen:
A discipline of dynamic programming over sequence data. Sci. Comput. Program. 51(3): 215-263 (2004)

Robert Giegerich, Hélène Touzet:
Modeling Dynamic Programming Problems over Sequences and Trees with Inverse Coupled Rewrite Systems. Algorithms 7(1): 62-144 (2014)

These approaches deal with string problems that are solved by dynamic programming such as the computation of edit distance or local alignments or comparison of RNA secondary structures. These problems are more difficult in terms of the running time of the best algorithms than the exact pattern matching problem that is solved by Boyer-Moore. 

A more conceptual or programmer-friendly approach for exact pattern matching would be to use the right data structures such as suffix arrays or suffix trees. Many pattern matching algorithms become simpler when these data structures are used as a black box or augmented in some relatively easy way.