Ironclad is a partially formally verified real-time kernel, with a small
footprint, for general-purpose and embedded OSes, written in SPARK and Ada.

Some of the supported features are:

- A familiar POSIX-compatible interface.
- True simultaneous multitasking.
- Resiliency and small footprint.
- Partial gold-level formal verification.
- Advanced cryptography and a security-centered architecture, including MAC.
- Hard real-time scheduling and real-time oriented features.
- Support for severals architectures and boards.

For more information about the project, some autogenerated documentation, bug
reporting, and development guides, check https://ironclad.nongnu.org

-- Building and testing --

The tools needed are:

- autoconf and automake when not using a tarball.
- perl for some checks, not for compilation.
- gprbuild for compilation, along with a compatible Ada compiler and assembler.
- GNU Info for building the documentation.
- gnatprove for formal verification, if desired.
- highlight for syntax highlighting when building the HTML documentation.

For building the project's binaries, a standard configure-make-make install is
enough, like the following:

./configure --target=x86_64-limine-elf # Or whatever other target.
make
make check # If desired, will need gnatprove and perl.
make install

Several flags are provided in configure for customizing kernel settings, one
can check them with ./configure --help.

The target has to always been specified, the vendor is used as the board to
compile for, the OS field is a placeholder and not used, autoconf just wants
it to be there.

Documentation will be generated and installed with the main executable in the
info format, additional formats can be built with `make html` or `make dvi`.

-- Contributing --

Thanks for considering contributing to Ironclad, it means a lot.

Please check <https://ironclad.nongnu.org/development.html> for information
on how to get started, and how to submit patches to the project.
========================================================================

Copyright (C) 2023 streaksu

Permission is granted to copy, distribute and/or modify this document
under the terms of the GNU Free Documentation License, Version 1.3 or
any later version published by the Free Software Foundation; with no
Invariant Sections, with no Front-Cover Texts, and with no Back-Cover
Texts.  A copy of the license is included in the "GNU Free
Documentation License" file as part of this distribution.