An obligation is something a proof leaves to be shown or trusted elsewhere, named rather than assumed away. A realization obligation is the trusted claim that native code realizes a logical model: that pinned libc's FILE, buffering and dispatch behave as Stdio.v's protocol and Libio.v's memory view say.
Readiness obligations of the runtimeruntime Fil-CThe runtime is what Fil-C does around one thread's program, natively libpizlo.so with FUGC: where a new object goes, what free does, and what the collector may change while the program waits at a safepoint. The model does not define it; it states it as one page of axioms, Module Type Runtime (Runtime), each with a native test in tests/c/prog/axiom-*.c. module type: freed_bounds, ready_kept and safepoint_ready, about the runtime's own bookkeeping, with no native test; InterpRuntime proves them.
Caller obligations: a premise of an external callexternal call nanofilAn external call is a call to a symbol the module does not define, in practice libc. The core model sends only free to the runtime and is stuck at every other. A contract is Campaign 4's trusted description of one external function: its ABI, the caller's premises, the roots it may write, what it may release or allocate, its observations and its endings.'s contract. A failed one is a ContractViolation, not a promise that native libc traps (libc-contracts.md, Traps).
Realization obligations: Stdio.v's stream_accounting proves the protocol consistent, not that native stdio follows it; native coverage of each contract stays trusted.
Proof obligations of campaign.md: soundness of checkingsoundness of checking nanofilSoundness of checking is the validator's theorem: every run of every valid checked module avoids unchecked, so the checks the validator demands, and those it lets a pass remove or reuse, are enough, and a check that fails is the run's whole story. It does not say a check never fails: a module that reads past an array is valid and traps., transformation correctness and implementation correctness, kept apart; Campaign 4 gives each pass and --checks mode a refinement obligation, against opt:refines/2opt.plrefines+Before, +AftersemidetAfter is an outcome the original program allows, given that the original's outcome was Before, both from interp:run/5 on the same inputs: restated as trace inclusion.