Hi, Here's what I'm doing to run seL4 on an Ariane processor (64 bit) with 16 MB RAM (and some internal BRAM from the FPGA). So far I've only tried the CAmkES adder example. This is the memory layout: 0x80000000: 256K BRAM for OpenSBI 0x80200000: 256K BRAM for ELF-Loader 0x84000000: 16M external RAM for seL4 & servers The BRAM sizes could be reduced to 128kB and 64kB. By default, the final image created by the build system includes the CPIO archive with the DTB and the root server. I modified it to not link the generated archive.o file. Instead, I read the CPIO archive from a memory-mapped flash. This allows me to place the ELF-Loader in a BRAM instead of the SRAM and gives more freedom over the memory layout. https://github.com/seL4-drone-project/seL4_tools/tree/seL4-drone-project There are 4 options in elfloader-tool/CMakeLists.txt * ElfloaderExistingArchive * ElfloaderRelocateArchive * ElfloaderArchiveStart * ElfloaderArchiveEnd Note that there's an option to copy the flash memory to the RAM. This is only there as a workaround for a bug in my FPGA design. shoehorn.py will still complain, but you can disable it by setting IMAGE_START_ADDR. The value doesn't matter because it's not used for RISC-V builds. I set it to 0x80200000. These are the memories in the DTS: memory@80000000 { device_type = "memory"; reg = <0x0 0x80000000 0x0 0x00040000>; }; memory@80200000 { device_type = "memory"; reg = <0x0 0x80200000 0x0 0x00040000>; }; memory@84000000 { device_type = "memory"; reg = <0x0 0x84000000 0x0 0x01000000>; }; hardware_gen.py in the seL4 repository adds an offset for the reserved bootloader section to the first memory, which causes an assertion to fail (start < end) in seL4, so I don't include it in the generated header file: https://github.com/seL4-drone-project/seL4/commit/3a7966ca919157be43e8e1d291... capdl-loader reports 10MB of untyped memory. It probably won't get you to 2MB, but maybe it helps.