Given that this is a reasonably small code base (compared to, say, an OS kernel), an idea would be to use a language that provides strong guarantees about corre

Given that this is a reasonably small code base (compared to, say, an OS kernel), an idea would be to use a language that provides strong guarantees about correctness the implementation. For example, Spark Ada can be used to do that. Alternatively, keeping the implementation in C, a similar level of assurance could be achieved by developing the library along with a specification, and requiring any extensions to pass some kind of correctness proof based on this specification.