At 01:50 PM 11/7/1999 -0800, Ka-Ping Yee wrote:
>point during his talk he mentioned that there exists an A1-level
>(mathematically-proven) operating system out there, which surprised
>me because i thought that EROS was the only one; he cited SCOMP.
As far as I know, SCOMP is the only A1 system. SCOMP is a Honeywell minicomputer OS.
KeyKOS, with some unwritten user mode code, had the requirements for a B3 (which are the same functional requirements as A1), but failed on the assurance (how sure are we that the code actually implements the specs). They didn't really approve of systems written in assembler.
Since that user mode code has never been written, neither KeyKOS or EROS can pass B3 or A1 (or almost any level for that matter). This is good as it keeps them from being subject to export restrictions.