Avra Cohn
A grouping.
Avra Cohn, at the Cambridge Computer Laboratory in Mike Gordon's HOL group. Three records, all from the VIPER episode, at increasing distance from it.
The two 1987 and 1988 technical reports are the machine-checked proofs themselves -- the first level, relating VIPER's top-level specification to its major state model, and the second, descending to the block model -- and the corpus holds both in full because Cambridge deposited them openly. The 1989 Journal of Automated Reasoning paper generalises them for a journal audience and is held as a citation only.
Read her for the caveats rather than the results. She is the field's first practitioner and its first sceptic, and the scepticism is not a later recantation: it is already in the 1987 conclusions, warning against 'a false sense of security afforded by an HOL proof' because 'there are many classes of errors not even visible in the models used'. By 1988 it has become a general argument, in a section she asks the reader to read even if the technical sections are skipped -- that 'neither an actual device nor an intention are objects to which logical reasoning can be applied', so 'verification involves two or more models of a device, where the models bear an uncheckable and possibly imperfect relation both to the intended design and to the actual device'.
The same report is candid about the episode's standing: the chips 'had been built and were being advertised' before the second-level work began, and she calls the research 'rather academic' on that ground. A reader who knows VIPER only as the founding success of hardware verification will not have met that sentence.
Nothing in the corpus covers the rest of her career.